GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/api/sep_log_api.cpp Lines: 83 98 84.7 %
Date: 2021-03-22 Branches: 115 226 50.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sep_log_api.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew V. Jones, Andres Noetzli, Andrew Reynolds
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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.\endverbatim
11
 **
12
 ** \brief Two tests to validate the use of the separation logic API.
13
 **
14
 ** First test validates that we cannot use the API if not using separation
15
 ** logic.
16
 **
17
 ** Second test validates that the expressions returned from the API are
18
 ** correct and can be interrogated.
19
 **
20
 *****************************************************************************/
21
22
#include <iostream>
23
#include <sstream>
24
25
#include "api/cvc4cpp.h"
26
27
using namespace CVC4::api;
28
using namespace std;
29
30
/**
31
 * Test function to validate that we *cannot* obtain the heap/nil expressions
32
 * when *not* using the separation logic theory
33
 */
34
1
int validate_exception(void)
35
{
36
2
  Solver slv;
37
38
  /*
39
   * Setup some options for CVC4 -- we explictly want to use a simplistic
40
   * theory (e.g., QF_IDL)
41
   */
42
1
  slv.setLogic("QF_IDL");
43
1
  slv.setOption("produce-models", "true");
44
1
  slv.setOption("incremental", "false");
45
46
  /* Our integer type */
47
2
  Sort integer = slv.getIntegerSort();
48
49
  /** we intentionally do not set the separation logic heap */
50
51
  /* Our SMT constants */
52
2
  Term x = slv.mkConst(integer, "x");
53
2
  Term y = slv.mkConst(integer, "y");
54
55
  /* y > x */
56
2
  Term y_gt_x(slv.mkTerm(Kind::GT, y, x));
57
58
  /* assert it */
59
1
  slv.assertFormula(y_gt_x);
60
61
  /* check */
62
2
  Result r(slv.checkSat());
63
64
  /* If this is UNSAT, we have an issue; so bail-out */
65
1
  if (!r.isSat())
66
  {
67
    return -1;
68
  }
69
70
  /*
71
   * We now try to obtain our separation logic expressions from the solver --
72
   * we want to validate that we get our expected exceptions.
73
   */
74
1
  bool caught_on_heap(false);
75
1
  bool caught_on_nil(false);
76
77
  /* The exception message we expect to obtain */
78
  std::string expected(
79
      "Cannot obtain separation logic expressions if not using the separation "
80
2
      "logic theory.");
81
82
  /* test the heap expression */
83
  try
84
  {
85
1
    Term heap_expr = slv.getSeparationHeap();
86
  }
87
2
  catch (const CVC4ApiException& e)
88
  {
89
1
    caught_on_heap = true;
90
91
    /* Check we get the correct exception string */
92
1
    if (e.what() != expected)
93
    {
94
      return -1;
95
    }
96
  }
97
98
  /* test the nil expression */
99
  try
100
  {
101
1
    Term nil_expr = slv.getSeparationNilTerm();
102
  }
103
2
  catch (const CVC4ApiException& e)
104
  {
105
1
    caught_on_nil = true;
106
107
    /* Check we get the correct exception string */
108
1
    if (e.what() != expected)
109
    {
110
      return -1;
111
    }
112
  }
113
114
1
  if (!caught_on_heap || !caught_on_nil)
115
  {
116
    return -1;
117
  }
118
119
  /* All tests pass! */
120
1
  return 0;
121
}
122
123
/**
124
 * Test function to demonstrate the use of, and validate the capability, of
125
 * obtaining the heap/nil expressions when using separation logic.
126
 */
127
1
int validate_getters(void)
128
{
129
2
  Solver slv;
130
131
  /* Setup some options for CVC4 */
132
1
  slv.setLogic("QF_ALL_SUPPORTED");
133
1
  slv.setOption("produce-models", "true");
134
1
  slv.setOption("incremental", "false");
135
136
  /* Our integer type */
137
2
  Sort integer = slv.getIntegerSort();
138
139
  /** Declare the separation logic heap types */
140
1
  slv.declareSeparationHeap(integer, integer);
141
142
  /* A "random" constant */
143
2
  Term random_constant = slv.mkInteger(0xDEADBEEF);
144
145
  /* Another random constant */
146
2
  Term expr_nil_val = slv.mkInteger(0xFBADBEEF);
147
148
  /* Our nil term */
149
2
  Term nil = slv.mkSepNil(integer);
150
151
  /* Our SMT constants */
152
2
  Term x = slv.mkConst(integer, "x");
153
2
  Term y = slv.mkConst(integer, "y");
154
2
  Term p1 = slv.mkConst(integer, "p1");
155
2
  Term p2 = slv.mkConst(integer, "p2");
156
157
  /* Constraints on x and y */
158
2
  Term x_equal_const = slv.mkTerm(Kind::EQUAL, x, random_constant);
159
2
  Term y_gt_x = slv.mkTerm(Kind::GT, y, x);
160
161
  /* Points-to expressions */
162
2
  Term p1_to_x = slv.mkTerm(Kind::SEP_PTO, p1, x);
163
2
  Term p2_to_y = slv.mkTerm(Kind::SEP_PTO, p2, y);
164
165
  /* Heap -- the points-to have to be "starred"! */
166
2
  Term heap = slv.mkTerm(Kind::SEP_STAR, p1_to_x, p2_to_y);
167
168
  /* Constain "nil" to be something random */
169
2
  Term fix_nil = slv.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
    return -1;
187
  }
188
189
  /* Obtain our separation logic terms from the solver */
190
2
  Term heap_expr = slv.getSeparationHeap();
191
2
  Term nil_expr = slv.getSeparationNilTerm();
192
193
  /* If the heap is not a separating conjunction, bail-out */
194
1
  if (heap_expr.getKind() != Kind::SEP_STAR)
195
  {
196
    return -1;
197
  }
198
199
  /* If nil is not a direct equality, bail-out */
200
1
  if (nil_expr.getKind() != Kind::EQUAL)
201
  {
202
    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
      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
3
    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
        return -1;
235
      }
236
1
      continue;
237
    }
238
239
    /* If the current address is the value for p2 */
240
2
    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
2
      if (std::stoll(value.toString())
250
1
          <= std::stoll(random_constant.toString()))
251
      {
252
        return -1;
253
      }
254
1
      continue;
255
    }
256
257
    /*
258
     * We should only have two addresses in heap, so if we haven't hit the
259
     * "continue" for p1 or p2, then bail-out
260
     */
261
    return -1;
262
  }
263
264
  /*
265
   * If we complete the loop and we haven't validated both p1 and p2, then we
266
   * have a problem
267
   */
268
1
  if (!checked_p1 || !checked_p2)
269
  {
270
    return -1;
271
  }
272
273
  /* We now get our value for what nil is */
274
2
  Term value_for_nil = slv.getValue(nil_expr[1]);
275
276
  /*
277
   * The value for nil from the solver should be the value we originally tied
278
   * nil to
279
   */
280
1
  if (value_for_nil != expr_nil_val)
281
  {
282
    return -1;
283
  }
284
285
  /* All tests pass! */
286
1
  return 0;
287
}
288
289
1
int main(void)
290
{
291
  /* check that we get an exception when we should */
292
1
  int check_exception(validate_exception());
293
294
1
  if (check_exception)
295
  {
296
    return check_exception;
297
  }
298
299
  /* check the getters */
300
1
  int check_getters(validate_getters());
301
302
1
  if (check_getters)
303
  {
304
    return check_getters;
305
  }
306
307
1
  return 0;
308
3
}