Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Aina Niemetz, Andrew V. Jones
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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/c/cvc5.h>
24 : :
25 : 1 : int main(void)
26 : : {
27 : 1 : int res = 0;
28 : : /**
29 : : * Test function to demonstrate the use of, and validate the capability, of
30 : : * obtaining the heap/nil expressions when using separation logic.
31 : : */
32 : 1 : Cvc5TermManager* tm = cvc5_term_manager_new();
33 : 1 : Cvc5* solver = cvc5_new(tm);
34 : :
35 : : /* Setup some options for cvc5 */
36 : 1 : cvc5_set_logic(solver, "ALL");
37 : 1 : cvc5_set_option(solver, "produce-models", "true");
38 : 1 : cvc5_set_option(solver, "incremental", "false");
39 : :
40 : : /* Our integer type */
41 : 1 : Cvc5Sort int_sort = cvc5_get_integer_sort(tm);
42 : :
43 : : /** Declare the separation logic heap types */
44 : 1 : cvc5_declare_sep_heap(solver, int_sort, int_sort);
45 : :
46 : : /* A "random" constant */
47 : 1 : Cvc5Term random_constant = cvc5_mk_integer_int64(tm, 0xDEADBEEF);
48 : :
49 : : /* Another random constant */
50 : 1 : Cvc5Term expr_nil_val = cvc5_mk_integer_int64(tm, 0xFBADBEEF);
51 : :
52 : : /* Our nil term */
53 : 1 : Cvc5Term nil = cvc5_mk_sep_nil(tm, int_sort);
54 : :
55 : : /* Our SMT constants */
56 : 1 : Cvc5Term x = cvc5_mk_const(tm, int_sort, "x");
57 : 1 : Cvc5Term y = cvc5_mk_const(tm, int_sort, "y");
58 : 1 : Cvc5Term p1 = cvc5_mk_const(tm, int_sort, "p1");
59 : 1 : Cvc5Term p2 = cvc5_mk_const(tm, int_sort, "p2");
60 : :
61 : : /* Constraints on x and y */
62 : 1 : Cvc5Term args[2] = {x, random_constant};
63 : 1 : Cvc5Term x_eq_const = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args);
64 : 1 : args[0] = y;
65 : 1 : args[1] = x;
66 : 1 : Cvc5Term y_gt_x = cvc5_mk_term(tm, CVC5_KIND_GT, 2, args);
67 : :
68 : : /* Points-to expressions */
69 : 1 : args[0] = p1;
70 : 1 : args[1] = x;
71 : 1 : Cvc5Term p1_to_x = cvc5_mk_term(tm, CVC5_KIND_SEP_PTO, 2, args);
72 : 1 : args[0] = p2;
73 : 1 : args[1] = y;
74 : 1 : Cvc5Term p2_to_y = cvc5_mk_term(tm, CVC5_KIND_SEP_PTO, 2, args);
75 : :
76 : : /* Heap -- the points-to have to be "starred"! */
77 : 1 : args[0] = p1_to_x;
78 : 1 : args[1] = p2_to_y;
79 : 1 : Cvc5Term heap = cvc5_mk_term(tm, CVC5_KIND_SEP_STAR, 2, args);
80 : :
81 : : /* Constain "nil" to be something random */
82 : 1 : args[0] = nil;
83 : 1 : args[1] = expr_nil_val;
84 : 1 : Cvc5Term fix_nil = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args);
85 : :
86 : : /* Add it all to the solver! */
87 : 1 : cvc5_assert_formula(solver, x_eq_const);
88 : 1 : cvc5_assert_formula(solver, y_gt_x);
89 : 1 : cvc5_assert_formula(solver, heap);
90 : 1 : cvc5_assert_formula(solver, fix_nil);
91 : :
92 : : /*
93 : : * Incremental is disabled due to using separation logic, so don't query
94 : : * twice!
95 : : */
96 : 1 : Cvc5Result r = cvc5_check_sat(solver);
97 : :
98 : : /* If this is UNSAT, we have an issue; so bail-out */
99 [ - + ]: 1 : if (!cvc5_result_is_sat(r))
100 : : {
101 : 0 : res = -1;
102 : : }
103 : : else
104 : : {
105 : : /* Obtain our separation logic terms from the solver */
106 : :
107 : 1 : Cvc5Term heap_expr = cvc5_get_value_sep_heap(solver);
108 : 1 : Cvc5Term nil_expr = cvc5_get_value_sep_nil(solver);
109 : :
110 : : /* If the heap is not a separating conjunction, bail-out */
111 [ - + ]: 1 : if (cvc5_term_get_kind(heap_expr) != CVC5_KIND_SEP_STAR)
112 : : {
113 : 0 : res = -1;
114 : : }
115 : : /* If nil is not a direct equality, bail-out */
116 [ - + ]: 1 : else if (cvc5_term_get_kind(nil_expr) != CVC5_KIND_EQUAL)
117 : : {
118 : 0 : res = -1;
119 : : }
120 : : else
121 : : {
122 : : /* Obtain the values for our "pointers" */
123 : 1 : Cvc5Term val_for_p1 = cvc5_get_value(solver, p1);
124 : 1 : Cvc5Term val_for_p2 = cvc5_get_value(solver, p2);
125 : :
126 : : /* We need to make sure we find both pointers in the heap */
127 : 1 : bool checked_p1 = false;
128 : 1 : bool checked_p2 = false;
129 : :
130 : : /* Walk all the children */
131 [ + + ]: 3 : for (size_t i = 0, n = cvc5_term_get_num_children(heap_expr); i < n; i++)
132 : : {
133 : 2 : Cvc5Term child = cvc5_term_get_child(heap_expr, i);
134 : : /* If we don't have a PTO operator, bail-out */
135 [ - + ]: 2 : if (cvc5_term_get_kind(child) != CVC5_KIND_SEP_PTO)
136 : : {
137 : 0 : res = -1;
138 : 0 : break;
139 : : }
140 : :
141 : : /* Find both sides of the PTO operator */
142 : 2 : Cvc5Term addr = cvc5_get_value(solver, cvc5_term_get_child(child, 0));
143 : 2 : Cvc5Term value = cvc5_get_value(solver, cvc5_term_get_child(child, 1));
144 : :
145 : : /* If the current address is the value for p1 */
146 [ + + ]: 2 : if (cvc5_term_is_equal(addr, val_for_p1))
147 : : {
148 : 1 : checked_p1 = true;
149 : :
150 : : /* If it doesn't match the random constant, we have a problem */
151 [ - + ]: 1 : if (cvc5_term_is_disequal(value, random_constant))
152 : : {
153 : 0 : res = -1;
154 : 0 : break;
155 : : }
156 : 1 : continue;
157 : : }
158 : :
159 : : /* If the current address is the value for p2 */
160 [ + - ]: 1 : if (cvc5_term_is_equal(addr, val_for_p2))
161 : : {
162 : 1 : checked_p2 = true;
163 : :
164 : : /*
165 : : * Our earlier constraint was that what p2 points to must be *greater*
166 : : * than the random constant -- if we get a value that is LTE, then
167 : : * something has gone wrong!
168 : : */
169 : 1 : if (cvc5_term_get_int64_value(value)
170 [ - + ]: 1 : <= cvc5_term_get_int64_value(random_constant))
171 : : {
172 : 0 : res = -1;
173 : 0 : break;
174 : : }
175 : 1 : continue;
176 : : }
177 : :
178 : : /*
179 : : * We should only have two addresses in heap, so if we haven't hit the
180 : : * "continue" for p1 or p2, then bail-out
181 : : */
182 : 0 : res = -1;
183 : 0 : break;
184 : : }
185 : :
186 : : /*
187 : : * If we complete the loop and we haven't validated both p1 and p2, then
188 : : * we have a problem
189 : : */
190 [ + - ]: 1 : if (res == 0)
191 : : {
192 [ + - ][ - + ]: 1 : if (!checked_p1 || !checked_p2)
193 : : {
194 : 0 : res = -1;
195 : : }
196 : : else
197 : : {
198 : : /* We now get our value for what nil is */
199 : : Cvc5Term value_for_nil =
200 : 1 : cvc5_get_value(solver, cvc5_term_get_child(nil_expr, 1));
201 : :
202 : : /*
203 : : * The value for nil from the solver should be the value we originally
204 : : * tied nil to
205 : : */
206 [ - + ]: 1 : if (cvc5_term_is_disequal(value_for_nil, expr_nil_val))
207 : : {
208 : 0 : res = -1;
209 : : }
210 : : }
211 : : }
212 : : }
213 : : }
214 : :
215 : : /* All tests pass! */
216 : 1 : cvc5_delete(solver);
217 : 1 : cvc5_term_manager_delete(tm);
218 : 1 : return res;
219 : : }
|
