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