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