Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	test/api/sep_log_api.cpp	Lines:	83	98	84.7 %
Date:	2021-09-07	Branches:	115	226	50.9 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew V. Jones, Andres Noetzli, Andrew Reynolds
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Two tests to validate the use of the separation logic API.
 *
 * First test validates that we cannot use the API if not using separation
 * logic.
 *
 * Second test validates that the expressions returned from the API are
 * correct and can be interrogated.
 *
 ****************************************************************************/

#include <iostream>
#include <sstream>

#include "api/cpp/cvc5.h"

using namespace cvc5::api;
using namespace std;

/**
 * Test function to validate that we *cannot* obtain the heap/nil expressions
 * when *not* using the separation logic theory
 */
int validate_exception(void)
{
  Solver slv;

  /*
   * Setup some options for cvc5 -- we explictly want to use a simplistic
   * theory (e.g., QF_IDL)
   */
  slv.setLogic("QF_IDL");
  slv.setOption("produce-models", "true");
  slv.setOption("incremental", "false");

  /* Our integer type */
  Sort integer = slv.getIntegerSort();

  /** we intentionally do not set the separation logic heap */

  /* Our SMT constants */
  Term x = slv.mkConst(integer, "x");
  Term y = slv.mkConst(integer, "y");

  /* y > x */
  Term y_gt_x(slv.mkTerm(Kind::GT, y, x));

  /* assert it */
  slv.assertFormula(y_gt_x);

  /* check */
  Result r(slv.checkSat());

  /* If this is UNSAT, we have an issue; so bail-out */
  if (!r.isSat())
  {
    return -1;
  }

  /*
   * We now try to obtain our separation logic expressions from the solver --
   * we want to validate that we get our expected exceptions.
   */
  bool caught_on_heap(false);
  bool caught_on_nil(false);

  /* The exception message we expect to obtain */
  std::string expected(
      "Cannot obtain separation logic expressions if not using the separation "
      "logic theory.");

  /* test the heap expression */
  try
  {
    Term heap_expr = slv.getSeparationHeap();
  }
  catch (const CVC5ApiException& e)
  {
    caught_on_heap = true;

    /* Check we get the correct exception string */
    if (e.what() != expected)
    {
      return -1;
    }
  }

  /* test the nil expression */
  try
  {
    Term nil_expr = slv.getSeparationNilTerm();
  }
  catch (const CVC5ApiException& e)
  {
    caught_on_nil = true;

    /* Check we get the correct exception string */
    if (e.what() != expected)
    {
      return -1;
    }
  }

  if (!caught_on_heap || !caught_on_nil)
  {
    return -1;
  }

  /* All tests pass! */
  return 0;
}

/**
 * Test function to demonstrate the use of, and validate the capability, of
 * obtaining the heap/nil expressions when using separation logic.
 */
int validate_getters(void)
{
  Solver slv;

  /* Setup some options for cvc5 */
  slv.setLogic("QF_ALL");
  slv.setOption("produce-models", "true");
  slv.setOption("incremental", "false");

  /* Our integer type */
  Sort integer = slv.getIntegerSort();

  /** Declare the separation logic heap types */
  slv.declareSeparationHeap(integer, integer);

  /* A "random" constant */
  Term random_constant = slv.mkInteger(0xDEADBEEF);

  /* Another random constant */
  Term expr_nil_val = slv.mkInteger(0xFBADBEEF);

  /* Our nil term */
  Term nil = slv.mkSepNil(integer);

  /* Our SMT constants */
  Term x = slv.mkConst(integer, "x");
  Term y = slv.mkConst(integer, "y");
  Term p1 = slv.mkConst(integer, "p1");
  Term p2 = slv.mkConst(integer, "p2");

  /* Constraints on x and y */
  Term x_equal_const = slv.mkTerm(Kind::EQUAL, x, random_constant);
  Term y_gt_x = slv.mkTerm(Kind::GT, y, x);

  /* Points-to expressions */
  Term p1_to_x = slv.mkTerm(Kind::SEP_PTO, p1, x);
  Term p2_to_y = slv.mkTerm(Kind::SEP_PTO, p2, y);

  /* Heap -- the points-to have to be "starred"! */
  Term heap = slv.mkTerm(Kind::SEP_STAR, p1_to_x, p2_to_y);

  /* Constain "nil" to be something random */
  Term fix_nil = slv.mkTerm(Kind::EQUAL, nil, expr_nil_val);

  /* Add it all to the solver! */
  slv.assertFormula(x_equal_const);
  slv.assertFormula(y_gt_x);
  slv.assertFormula(heap);
  slv.assertFormula(fix_nil);

  /*
   * Incremental is disabled due to using separation logic, so don't query
   * twice!
   */
  Result r(slv.checkSat());

  /* If this is UNSAT, we have an issue; so bail-out */
  if (!r.isSat())
  {
    return -1;
  }

  /* Obtain our separation logic terms from the solver */
  Term heap_expr = slv.getSeparationHeap();
  Term nil_expr = slv.getSeparationNilTerm();

  /* If the heap is not a separating conjunction, bail-out */
  if (heap_expr.getKind() != Kind::SEP_STAR)
  {
    return -1;
  }

  /* If nil is not a direct equality, bail-out */
  if (nil_expr.getKind() != Kind::EQUAL)
  {
    return -1;
  }

  /* Obtain the values for our "pointers" */
  Term val_for_p1 = slv.getValue(p1);
  Term val_for_p2 = slv.getValue(p2);

  /* We need to make sure we find both pointers in the heap */
  bool checked_p1(false);
  bool checked_p2(false);

  /* Walk all the children */
  for (const Term& child : heap_expr)
  {
    /* If we don't have a PTO operator, bail-out */
    if (child.getKind() != Kind::SEP_PTO)
    {
      return -1;
    }

    /* Find both sides of the PTO operator */
    Term addr = slv.getValue(child[0]);
    Term value = slv.getValue(child[1]);

    /* If the current address is the value for p1 */
    if (addr == val_for_p1)
    {
      checked_p1 = true;

      /* If it doesn't match the random constant, we have a problem */
      if (value != random_constant)
      {
        return -1;
      }
      continue;
    }

    /* If the current address is the value for p2 */
    if (addr == val_for_p2)
    {
      checked_p2 = true;

      /*
       * Our earlier constraint was that what p2 points to must be *greater*
       * than the random constant -- if we get a value that is LTE, then
       * something has gone wrong!
       */
      if (std::stoll(value.toString())
          <= std::stoll(random_constant.toString()))
      {
        return -1;
      }
      continue;
    }

    /*
     * We should only have two addresses in heap, so if we haven't hit the
     * "continue" for p1 or p2, then bail-out
     */
    return -1;
  }

  /*
   * If we complete the loop and we haven't validated both p1 and p2, then we
   * have a problem
   */
  if (!checked_p1 || !checked_p2)
  {
    return -1;
  }

  /* We now get our value for what nil is */
  Term value_for_nil = slv.getValue(nil_expr[1]);

  /*
   * The value for nil from the solver should be the value we originally tied
   * nil to
   */
  if (value_for_nil != expr_nil_val)
  {
    return -1;
  }

  /* All tests pass! */
  return 0;
}

int main(void)
{
  /* check that we get an exception when we should */
  int check_exception(validate_exception());

  if (check_exception)
  {
    return check_exception;
  }

  /* check the getters */
  int check_getters(validate_getters());

  if (check_getters)
  {
    return check_getters;
  }

  return 0;
}


Generated by: GCOVR (Version 3.2)

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