Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Two tests to validate the use of the separation logic API.
11 : : *
12 : : * First test validates that we cannot use the API if not using separation
13 : : * logic.
14 : : *
15 : : * Second test validates that the expressions returned from the API are
16 : : * correct and can be interrogated.
17 : : *
18 : : ****************************************************************************/
19 : :
20 : : #include <cvc5/cvc5.h>
21 : :
22 : : using namespace cvc5;
23 : : using namespace std;
24 : :
25 : : /**
26 : : * Test function to validate that we *cannot* obtain the heap/nil expressions
27 : : * when *not* using the separation logic theory
28 : : */
29 : 1 : int validate_exception(void)
30 : : {
31 : 1 : TermManager tm;
32 : 1 : Solver slv(tm);
33 : :
34 : : /*
35 : : * Setup some options for cvc5 -- we explictly want to use a simplistic
36 : : * theory (e.g., QF_IDL)
37 : : */
38 : 1 : slv.setLogic("QF_IDL");
39 : 1 : slv.setOption("produce-models", "true");
40 : 1 : slv.setOption("incremental", "false");
41 : :
42 : : /* Our integer type */
43 : 1 : Sort integer = tm.getIntegerSort();
44 : :
45 : : /** we intentionally do not set the separation logic heap */
46 : :
47 : : /* Our SMT constants */
48 : 1 : Term x = tm.mkConst(integer, "x");
49 : 1 : Term y = tm.mkConst(integer, "y");
50 : :
51 : : /* y > x */
52 : 4 : Term y_gt_x(tm.mkTerm(Kind::GT, {y, x}));
53 : :
54 : : /* assert it */
55 : 1 : slv.assertFormula(y_gt_x);
56 : :
57 : : /* check */
58 : 1 : Result r(slv.checkSat());
59 : :
60 : : /* If this is UNSAT, we have an issue; so bail-out */
61 [ - + ]: 1 : if (!r.isSat())
62 : : {
63 : 0 : return -1;
64 : : }
65 : :
66 : : /*
67 : : * We now try to obtain our separation logic expressions from the solver --
68 : : * we want to validate that we get our expected exceptions.
69 : : */
70 : 1 : bool caught_on_heap(false);
71 : 1 : bool caught_on_nil(false);
72 : :
73 : : /* The exception message we expect to obtain */
74 : : std::string expected(
75 : : "cannot obtain separation logic expressions if not using the separation "
76 : 1 : "logic theory.");
77 : :
78 : : /* test the heap expression */
79 : : try
80 : : {
81 : 1 : Term heap_expr = slv.getValueSepHeap();
82 : 0 : }
83 [ - + ]: 1 : catch (const CVC5ApiException& e)
84 : : {
85 : 1 : caught_on_heap = true;
86 : :
87 : : /* Check we get the correct exception string */
88 [ - + ]: 1 : if (e.what() != expected)
89 : : {
90 : 0 : return -1;
91 : : }
92 [ - + ]: 1 : }
93 : :
94 : : /* test the nil expression */
95 : : try
96 : : {
97 : 1 : Term nil_expr = slv.getValueSepNil();
98 : 0 : }
99 [ - + ]: 1 : catch (const CVC5ApiException& e)
100 : : {
101 : 1 : caught_on_nil = true;
102 : :
103 : : /* Check we get the correct exception string */
104 [ - + ]: 1 : if (e.what() != expected)
105 : : {
106 : 0 : return -1;
107 : : }
108 [ - + ]: 1 : }
109 : :
110 [ + - ][ - + ]: 1 : if (!caught_on_heap || !caught_on_nil)
111 : : {
112 : 0 : return -1;
113 : : }
114 : :
115 : : /* All tests pass! */
116 : 1 : return 0;
117 : 1 : }
118 : :
119 : : /**
120 : : * Test function to demonstrate the use of, and validate the capability, of
121 : : * obtaining the heap/nil expressions when using separation logic.
122 : : */
123 : 1 : int validate_getters(void)
124 : : {
125 : 1 : TermManager tm;
126 : 1 : Solver slv(tm);
127 : :
128 : : /* Setup some options for cvc5 */
129 : 1 : slv.setLogic("QF_ALL");
130 : 1 : slv.setOption("produce-models", "true");
131 : 1 : slv.setOption("incremental", "false");
132 : :
133 : : /* Our integer type */
134 : 1 : Sort integer = tm.getIntegerSort();
135 : :
136 : : /** Declare the separation logic heap types */
137 : 1 : slv.declareSepHeap(integer, integer);
138 : :
139 : : /* A "random" constant */
140 : 1 : Term random_constant = tm.mkInteger(0xDEADBEEF);
141 : :
142 : : /* Another random constant */
143 : 1 : Term expr_nil_val = tm.mkInteger(0xFBADBEEF);
144 : :
145 : : /* Our nil term */
146 : 1 : Term nil = tm.mkSepNil(integer);
147 : :
148 : : /* Our SMT constants */
149 : 1 : Term x = tm.mkConst(integer, "x");
150 : 1 : Term y = tm.mkConst(integer, "y");
151 : 1 : Term p1 = tm.mkConst(integer, "p1");
152 : 1 : Term p2 = tm.mkConst(integer, "p2");
153 : :
154 : : /* Constraints on x and y */
155 : 4 : Term x_equal_const = tm.mkTerm(Kind::EQUAL, {x, random_constant});
156 : 4 : Term y_gt_x = tm.mkTerm(Kind::GT, {y, x});
157 : :
158 : : /* Points-to expressions */
159 : 4 : Term p1_to_x = tm.mkTerm(Kind::SEP_PTO, {p1, x});
160 : 4 : Term p2_to_y = tm.mkTerm(Kind::SEP_PTO, {p2, y});
161 : :
162 : : /* Heap -- the points-to have to be "starred"! */
163 : 4 : Term heap = tm.mkTerm(Kind::SEP_STAR, {p1_to_x, p2_to_y});
164 : :
165 : : /* Constain "nil" to be something random */
166 : 4 : Term fix_nil = tm.mkTerm(Kind::EQUAL, {nil, expr_nil_val});
167 : :
168 : : /* Add it all to the solver! */
169 : 1 : slv.assertFormula(x_equal_const);
170 : 1 : slv.assertFormula(y_gt_x);
171 : 1 : slv.assertFormula(heap);
172 : 1 : slv.assertFormula(fix_nil);
173 : :
174 : : /*
175 : : * Incremental is disabled due to using separation logic, so don't query
176 : : * twice!
177 : : */
178 : 1 : Result r(slv.checkSat());
179 : :
180 : : /* If this is UNSAT, we have an issue; so bail-out */
181 [ - + ]: 1 : if (!r.isSat())
182 : : {
183 : 0 : return -1;
184 : : }
185 : :
186 : : /* Obtain our separation logic terms from the solver */
187 : 1 : Term heap_expr = slv.getValueSepHeap();
188 : 1 : Term nil_expr = slv.getValueSepNil();
189 : :
190 : : /* If the heap is not a separating conjunction, bail-out */
191 [ - + ]: 1 : if (heap_expr.getKind() != Kind::SEP_STAR)
192 : : {
193 : 0 : return -1;
194 : : }
195 : :
196 : : /* If nil is not a direct equality, bail-out */
197 [ - + ]: 1 : if (nil_expr.getKind() != Kind::EQUAL)
198 : : {
199 : 0 : return -1;
200 : : }
201 : :
202 : : /* Obtain the values for our "pointers" */
203 : 1 : Term val_for_p1 = slv.getValue(p1);
204 : 1 : Term val_for_p2 = slv.getValue(p2);
205 : :
206 : : /* We need to make sure we find both pointers in the heap */
207 : 1 : bool checked_p1(false);
208 : 1 : bool checked_p2(false);
209 : :
210 : : /* Walk all the children */
211 [ + + ]: 3 : for (const Term& child : heap_expr)
212 : : {
213 : : /* If we don't have a PTO operator, bail-out */
214 [ - + ]: 2 : if (child.getKind() != Kind::SEP_PTO)
215 : : {
216 : 0 : return -1;
217 : : }
218 : :
219 : : /* Find both sides of the PTO operator */
220 : 2 : Term addr = slv.getValue(child[0]);
221 : 2 : Term value = slv.getValue(child[1]);
222 : :
223 : : /* If the current address is the value for p1 */
224 [ + + ]: 2 : if (addr == val_for_p1)
225 : : {
226 : 1 : checked_p1 = true;
227 : :
228 : : /* If it doesn't match the random constant, we have a problem */
229 [ - + ]: 1 : if (value != random_constant)
230 : : {
231 : 0 : return -1;
232 : : }
233 : 1 : continue;
234 : : }
235 : :
236 : : /* If the current address is the value for p2 */
237 [ + - ]: 1 : if (addr == val_for_p2)
238 : : {
239 : 1 : checked_p2 = true;
240 : :
241 : : /*
242 : : * Our earlier constraint was that what p2 points to must be *greater*
243 : : * than the random constant -- if we get a value that is LTE, then
244 : : * something has gone wrong!
245 : : */
246 [ - + ]: 1 : if (value.getInt64Value() <= random_constant.getInt64Value())
247 : : {
248 : 0 : return -1;
249 : : }
250 : 1 : continue;
251 : : }
252 : :
253 : : /*
254 : : * We should only have two addresses in heap, so if we haven't hit the
255 : : * "continue" for p1 or p2, then bail-out
256 : : */
257 : 0 : return -1;
258 [ - + ][ - + ]: 7 : }
[ - + ][ + - ]
[ + - ]
259 : :
260 : : /*
261 : : * If we complete the loop and we haven't validated both p1 and p2, then we
262 : : * have a problem
263 : : */
264 [ + - ][ - + ]: 1 : if (!checked_p1 || !checked_p2)
265 : : {
266 : 0 : return -1;
267 : : }
268 : :
269 : : /* We now get our value for what nil is */
270 : 1 : Term value_for_nil = slv.getValue(nil_expr[1]);
271 : :
272 : : /*
273 : : * The value for nil from the solver should be the value we originally tied
274 : : * nil to
275 : : */
276 [ - + ]: 1 : if (value_for_nil != expr_nil_val)
277 : : {
278 : 0 : return -1;
279 : : }
280 : :
281 : : /* All tests pass! */
282 : 1 : return 0;
283 : 1 : }
284 : :
285 : 1 : int main(void)
286 : : {
287 : : /* check that we get an exception when we should */
288 : 1 : int check_exception(validate_exception());
289 : :
290 [ - + ]: 1 : if (check_exception)
291 : : {
292 : 0 : return check_exception;
293 : : }
294 : :
295 : : /* check the getters */
296 : 1 : int check_getters(validate_getters());
297 : :
298 [ - + ]: 1 : if (check_getters)
299 : : {
300 : 0 : return check_getters;
301 : : }
302 : :
303 : 1 : return 0;
304 : : }
|
