Skip to content

Commit bae2a1c

Browse files
kfriedbergerkfriedberger
committed
Separation Logic: add initial test.
1 parent 9bf39bb commit bae2a1c

File tree

1 file changed

+309
-0
lines changed

1 file changed

+309
-0
lines changed

‎src/org/sosy_lab/java_smt/test/SLFormulaManagerTest.java‎

Lines changed: 309 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,309 @@
1+
// This file is part of JavaSMT,
2+
// an API wrapper for a collection of SMT solvers:
3+
// https://github.com/sosy-lab/java-smt
4+
//
5+
// SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
6+
//
7+
// SPDX-License-Identifier: Apache-2.0
8+
9+
package org.sosy_lab.java_smt.test;
10+
11+
import static com.google.common.truth.Truth.assertThat;
12+
import static com.google.common.truth.TruthJUnit.assume;
13+
14+
import com.google.common.collect.ImmutableList;
15+
import com.google.common.collect.ImmutableSet;
16+
import com.google.common.collect.Iterables;
17+
import java.math.BigInteger;
18+
import java.util.ArrayList;
19+
import java.util.List;
20+
import org.junit.Before;
21+
import org.junit.Test;
22+
import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
23+
import org.sosy_lab.java_smt.api.BooleanFormula;
24+
import org.sosy_lab.java_smt.api.FormulaType;
25+
import org.sosy_lab.java_smt.api.Model;
26+
import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
27+
import org.sosy_lab.java_smt.api.ProverEnvironment;
28+
import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
29+
import org.sosy_lab.java_smt.api.SolverException;
30+
31+
public class SLFormulaManagerTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 {
32+
33+
private BooleanFormula makeStarAll(List<BooleanFormula> formulas) {
34+
return formulas.stream().reduce(slmgr::makeStar).orElse(bmgr.makeTrue());
35+
}
36+
37+
protected void requireSepNil() {
38+
assume()
39+
.withMessage("Java bindings for solver %s do not support SEP_NIL", solverToUse())
40+
.that(solverToUse())
41+
.isNotEqualTo(Solvers.CVC4);
42+
}
43+
44+
protected void requireMultipleHeapSorts() {
45+
assume()
46+
.withMessage(
47+
"Java bindings for solver %s do not support multiple heap sorts", solverToUse())
48+
.that(solverToUse())
49+
.isNotEqualTo(Solvers.CVC4);
50+
}
51+
52+
@Before
53+
public void setup() {
54+
requireSeparationLogic();
55+
}
56+
57+
@Test
58+
public void testStackWithoutSL() throws InterruptedException, SolverException {
59+
BooleanFormula noSL = imgr.equal(imgr.makeNumber(1), imgr.makeVariable("x"));
60+
61+
assertThatFormula(noSL).isSatisfiable(ProverOptions.ENABLE_SEPARATION_LOGIC);
62+
}
63+
64+
@Test
65+
public void testMakeEmp() throws InterruptedException, SolverException {
66+
BooleanFormula emptyHeapInt =
67+
slmgr.makeEmptyHeap(FormulaType.IntegerType, FormulaType.IntegerType);
68+
69+
assertThatFormula(emptyHeapInt).isSatisfiable(ProverOptions.ENABLE_SEPARATION_LOGIC);
70+
}
71+
72+
@Test
73+
public void testMakeEmptoP2() throws InterruptedException, SolverException {
74+
requireMultipleHeapSorts();
75+
// Actually, no solver supports multiple heap sorts. However, our bindings for CVC5
76+
// apply non-incremental mode for SL and use distinct solver instances for distinct queries.
77+
78+
BooleanFormula emptyHeapInt =
79+
slmgr.makeEmptyHeap(FormulaType.RationalType, FormulaType.BooleanType);
80+
BooleanFormula emptyHeapRat =
81+
slmgr.makeEmptyHeap(FormulaType.IntegerType, FormulaType.IntegerType);
82+
BooleanFormula query = bmgr.and(emptyHeapInt, emptyHeapRat);
83+
84+
assertThatFormula(query).isSatisfiable(ProverOptions.ENABLE_SEPARATION_LOGIC);
85+
}
86+
87+
@Test
88+
public void testNotNilPtoNil() throws InterruptedException, SolverException {
89+
requireSepNil();
90+
91+
IntegerFormula nil = slmgr.makeNilElement(FormulaType.IntegerType);
92+
BooleanFormula nilPtoNil = slmgr.makePointsTo(nil, nil);
93+
94+
assertThatFormula(nilPtoNil).isUnsatisfiable(ProverOptions.ENABLE_SEPARATION_LOGIC);
95+
}
96+
97+
@Test
98+
public void testNilPtoValue() throws InterruptedException, SolverException {
99+
requireSepNil();
100+
101+
IntegerFormula nil = slmgr.makeNilElement(FormulaType.IntegerType);
102+
IntegerFormula value = imgr.makeNumber(42);
103+
BooleanFormula nilPtoValue = slmgr.makePointsTo(nil, value);
104+
105+
assertThatFormula(nilPtoValue).isUnsatisfiable(ProverOptions.ENABLE_SEPARATION_LOGIC);
106+
}
107+
108+
@Test
109+
public void testXPtoNil() throws InterruptedException, SolverException {
110+
requireSepNil();
111+
112+
IntegerFormula ptr = imgr.makeVariable("p");
113+
IntegerFormula nil = slmgr.makeNilElement(FormulaType.IntegerType);
114+
BooleanFormula ptoNil = slmgr.makePointsTo(ptr, nil);
115+
116+
assertThatFormula(ptoNil).isSatisfiable(ProverOptions.ENABLE_SEPARATION_LOGIC);
117+
}
118+
119+
@Test
120+
public void testXPtoValue() throws InterruptedException, SolverException {
121+
IntegerFormula ptr = imgr.makeVariable("p");
122+
IntegerFormula value = imgr.makeNumber(42);
123+
BooleanFormula ptoValue = slmgr.makePointsTo(ptr, value);
124+
125+
assertThatFormula(ptoValue).isSatisfiable(ProverOptions.ENABLE_SEPARATION_LOGIC);
126+
}
127+
128+
@Test
129+
public void testPPtoNilThenPPtoNil() throws SolverException, InterruptedException {
130+
requireSepNil();
131+
132+
IntegerFormula ptr = imgr.makeVariable("p");
133+
IntegerFormula nil = slmgr.makeNilElement(FormulaType.IntegerType);
134+
BooleanFormula ptoNil = slmgr.makePointsTo(ptr, nil);
135+
136+
assertThatFormula(ptoNil).isSatisfiable(ProverOptions.ENABLE_SEPARATION_LOGIC);
137+
138+
// test repeated non-incremental solving in CVC5
139+
try (ProverEnvironment prover =
140+
context.newProverEnvironment(ProverOptions.ENABLE_SEPARATION_LOGIC)) {
141+
prover.push(ptoNil);
142+
assertThatEnvironment(prover).isSatisfiable();
143+
assertThatEnvironment(prover).isSatisfiable();
144+
prover.pop();
145+
}
146+
}
147+
148+
@Test
149+
public void testPtoNilThenPPto42() throws SolverException, InterruptedException {
150+
requireSepNil();
151+
152+
IntegerFormula ptr = imgr.makeVariable("p");
153+
IntegerFormula nil = slmgr.makeNilElement(FormulaType.IntegerType);
154+
IntegerFormula value = imgr.makeNumber(42);
155+
BooleanFormula ptoNil = slmgr.makePointsTo(ptr, nil);
156+
BooleanFormula ptoValue = slmgr.makePointsTo(ptr, value);
157+
158+
assertThatFormula(ptoNil).isSatisfiable(ProverOptions.ENABLE_SEPARATION_LOGIC);
159+
assertThatFormula(ptoValue).isSatisfiable(ProverOptions.ENABLE_SEPARATION_LOGIC);
160+
161+
// test repeated non-incremental solving in CVC5
162+
try (ProverEnvironment prover =
163+
context.newProverEnvironment(ProverOptions.ENABLE_SEPARATION_LOGIC)) {
164+
prover.push(ptoNil);
165+
assertThatEnvironment(prover).isSatisfiable();
166+
prover.pop();
167+
prover.push(ptoValue);
168+
assertThatEnvironment(prover).isSatisfiable();
169+
prover.pop();
170+
}
171+
}
172+
173+
@Test
174+
public void testPtoAndEmp() throws InterruptedException, SolverException {
175+
IntegerFormula ptr = imgr.makeVariable("p");
176+
IntegerFormula value = imgr.makeNumber(42);
177+
BooleanFormula pto = slmgr.makePointsTo(ptr, value);
178+
BooleanFormula emp = slmgr.makeEmptyHeap(FormulaType.IntegerType, FormulaType.IntegerType);
179+
BooleanFormula combined = slmgr.makeStar(pto, emp);
180+
181+
assertThatFormula(combined).isSatisfiable(ProverOptions.ENABLE_SEPARATION_LOGIC);
182+
}
183+
184+
@Test
185+
public void testStar() throws InterruptedException, SolverException {
186+
IntegerFormula ptr1 = imgr.makeVariable("ptoP1");
187+
IntegerFormula ptr2 = imgr.makeVariable("ptoP2");
188+
IntegerFormula value1 = imgr.makeNumber(42);
189+
IntegerFormula value2 = imgr.makeNumber(43);
190+
191+
BooleanFormula ptoP1V1 = slmgr.makePointsTo(ptr1, value1);
192+
BooleanFormula ptoP1V2 = slmgr.makePointsTo(ptr1, value2);
193+
BooleanFormula ptoP2V1 = slmgr.makePointsTo(ptr2, value1);
194+
BooleanFormula ptoP2V2 = slmgr.makePointsTo(ptr2, value2);
195+
196+
assertThatFormula(slmgr.makeStar(ptoP1V1, ptoP1V1))
197+
.isUnsatisfiable(ProverOptions.ENABLE_SEPARATION_LOGIC);
198+
assertThatFormula(slmgr.makeStar(ptoP1V1, ptoP1V2))
199+
.isUnsatisfiable(ProverOptions.ENABLE_SEPARATION_LOGIC);
200+
assertThatFormula(slmgr.makeStar(ptoP1V1, ptoP2V1))
201+
.isSatisfiable(ProverOptions.ENABLE_SEPARATION_LOGIC);
202+
assertThatFormula(slmgr.makeStar(ptoP1V1, ptoP2V2))
203+
.isSatisfiable(ProverOptions.ENABLE_SEPARATION_LOGIC);
204+
205+
assertThatFormula(
206+
bmgr.implication(
207+
slmgr.makeStar(ptoP1V1, ptoP2V2), imgr.distinct(ImmutableList.of(ptr1, ptr2))))
208+
.isTautological(ProverOptions.ENABLE_SEPARATION_LOGIC);
209+
}
210+
211+
@Test
212+
public void testSimpleTreeValid() throws InterruptedException, SolverException {
213+
requireSepNil();
214+
215+
// lets build a tree:
216+
// - each node consists of two integers: left and right
217+
// - each node pointer points to the left integer, the right integer is at pointer+1
218+
IntegerFormula nil = slmgr.makeNilElement(FormulaType.IntegerType);
219+
IntegerFormula one = imgr.makeNumber(1);
220+
IntegerFormula root = imgr.makeVariable("root");
221+
IntegerFormula left = imgr.makeVariable("left");
222+
IntegerFormula right = imgr.makeVariable("right");
223+
BooleanFormula ptoRootLeft = slmgr.makePointsTo(root, left);
224+
BooleanFormula ptoRootRight = slmgr.makePointsTo(imgr.add(root, one), left);
225+
BooleanFormula ptoLeftNil = slmgr.makePointsTo(left, nil);
226+
BooleanFormula ptoRightNil = slmgr.makePointsTo(right, nil);
227+
228+
// tree: (root -> left) * (root+1 -> right) * (left -> nil) * (right -> nil)
229+
BooleanFormula sepTree =
230+
makeStarAll(ImmutableList.of(ptoRootLeft, ptoRootRight, ptoLeftNil, ptoRightNil));
231+
232+
assertThatFormula(sepTree).isSatisfiable(ProverOptions.ENABLE_SEPARATION_LOGIC);
233+
try (ProverEnvironment prover =
234+
context.newProverEnvironment(
235+
ProverOptions.ENABLE_SEPARATION_LOGIC, ProverOptions.GENERATE_MODELS)) {
236+
prover.push(sepTree);
237+
assertThatEnvironment(prover).isSatisfiable();
238+
try (Model model = prover.getModel()) {
239+
// check that root, left and right are different
240+
BigInteger valRoot = model.evaluate(root);
241+
BigInteger valLeft = model.evaluate(left);
242+
BigInteger valRight = model.evaluate(right);
243+
BigInteger valNil = model.evaluate(nil);
244+
assertThat(ImmutableSet.of(valRoot, valLeft, valRight, valNil)).hasSize(4); // all different
245+
assertThat(valRoot.add(BigInteger.ONE)).isNoneOf(valLeft, valRight, valNil);
246+
}
247+
prover.pop();
248+
}
249+
}
250+
251+
@Test
252+
public void testSimpleTreeInvalid() throws InterruptedException, SolverException {
253+
requireSepNil();
254+
255+
IntegerFormula nil = slmgr.makeNilElement(FormulaType.IntegerType);
256+
IntegerFormula root = imgr.makeVariable("root");
257+
IntegerFormula left = imgr.makeVariable("left");
258+
IntegerFormula right = imgr.makeVariable("right");
259+
BooleanFormula ptoRootLeft = slmgr.makePointsTo(root, left);
260+
BooleanFormula ptoRootRight = slmgr.makePointsTo(imgr.add(root, imgr.makeNumber(1)), right);
261+
BooleanFormula ptoLeftNil = slmgr.makePointsTo(left, nil);
262+
BooleanFormula ptoLeftRight = slmgr.makePointsTo(left, right);
263+
264+
// tree: (root -> left) * (root+1 -> right) * (left -> nil) * (left -> right)
265+
BooleanFormula sepTree =
266+
makeStarAll(ImmutableList.of(ptoRootLeft, ptoRootRight, ptoLeftNil, ptoLeftRight));
267+
268+
// left has two different values -> invalid
269+
assertThatFormula(sepTree).isUnsatisfiable(ProverOptions.ENABLE_SEPARATION_LOGIC);
270+
}
271+
272+
@Test
273+
public void testListValid() throws InterruptedException, SolverException {
274+
requireSepNil();
275+
276+
IntegerFormula nil = slmgr.makeNilElement(FormulaType.IntegerType);
277+
List<IntegerFormula> nodes = new ArrayList<>();
278+
for (int i = 0; i <= 10; i++) {
279+
nodes.add(imgr.makeVariable("n" + i));
280+
}
281+
List<BooleanFormula> ptos = new ArrayList<>();
282+
for (int i = 0; i < nodes.size() - 1; i++) {
283+
ptos.add(slmgr.makePointsTo(nodes.get(i), nodes.get(i + 1)));
284+
}
285+
BooleanFormula ptoLastNil = slmgr.makePointsTo(Iterables.getLast(nodes), nil);
286+
287+
// list: n1 -> n2 -> ... -> nil
288+
BooleanFormula sepTree = slmgr.makeStar(makeStarAll(ptos), ptoLastNil);
289+
assertThatFormula(sepTree).isSatisfiable(ProverOptions.ENABLE_SEPARATION_LOGIC);
290+
}
291+
292+
@Test
293+
public void testListValidCycle() throws InterruptedException, SolverException {
294+
List<IntegerFormula> nodes = new ArrayList<>();
295+
for (int i = 0; i <= 10; i++) {
296+
nodes.add(imgr.makeVariable("n" + i));
297+
}
298+
List<BooleanFormula> ptos = new ArrayList<>();
299+
for (int i = 0; i < nodes.size() - 1; i++) {
300+
ptos.add(slmgr.makePointsTo(nodes.get(i), nodes.get(i + 1)));
301+
}
302+
BooleanFormula ptoLastNil =
303+
slmgr.makePointsTo(Iterables.getLast(nodes), Iterables.getFirst(nodes, null));
304+
305+
// list: (n1 -> n2 -> ... -> n10) * cycle: (n10 -> n1)
306+
BooleanFormula sepTree = slmgr.makeStar(makeStarAll(ptos), ptoLastNil);
307+
assertThatFormula(sepTree).isSatisfiable(ProverOptions.ENABLE_SEPARATION_LOGIC);
308+
}
309+
}

0 commit comments

Comments
 (0)