diff options
author | ayveejay <41393247+ayveejay@users.noreply.github.com> | 2018-08-01 03:25:51 +0100 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-07-31 19:25:51 -0700 |
commit | ad61299aa24a83f935daedab32440d25006e18bb (patch) | |
tree | 82540951afd070cc43f3e7ea87fc9b8c8e9311b8 /test/system | |
parent | 049bc7acdb7ecc50719175652028a51a8f996502 (diff) |
Improvements and tests for the API around separation logic (#2229)
- Introduces a system that validating that, when not using THEORY_SEP, that it is not possible to
obtain the separation logic heap/nil (validate_exception())
- Introduces a system test demonstrating how to use the separation logic theory, and then how
to use the "getters" to obtain and interrogate the heap/nil expressions (validate_getters())
- Refactors the original getters to avoid duplicate code
- Add a check as part of the getters to ensure that THEORY_SEP is in use
Diffstat (limited to 'test/system')
-rw-r--r-- | test/system/Makefile.am | 3 | ||||
-rw-r--r-- | test/system/sep_log_api.cpp | 313 |
2 files changed, 315 insertions, 1 deletions
diff --git a/test/system/Makefile.am b/test/system/Makefile.am index 1be242e3d..ed52b0232 100644 --- a/test/system/Makefile.am +++ b/test/system/Makefile.am @@ -6,7 +6,8 @@ CPLUSPLUS_TESTS = \ reset_assertions \ two_smt_engines \ smt2_compliance \ - statistics + statistics \ + sep_log_api if CVC4_BUILD_LIBCOMPAT #CPLUSPLUS_TESTS += \ diff --git a/test/system/sep_log_api.cpp b/test/system/sep_log_api.cpp new file mode 100644 index 000000000..354cd37b2 --- /dev/null +++ b/test/system/sep_log_api.cpp @@ -0,0 +1,313 @@ +/******************************************************************************/ +/*! \file sep_log_api.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew V. Jones + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS or file + ** THANKS (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.\endverbatim + ** + ** \brief 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 "expr/expr.h" +#include "smt/smt_engine.h" + +using namespace CVC4; +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) +{ + ExprManager em; + Options opts; + SmtEngine smt(&em); + + /* + * Setup some options for CVC4 -- we explictly want to use a simplistic + * theory (e.g., QF_IDL) + */ + smt.setLogic("QF_IDL"); + smt.setOption("produce-models", SExpr("true")); + smt.setOption("incremental", SExpr("false")); + + /* Our integer type */ + Type integer(em.integerType()); + + /* Our SMT constants */ + Expr x(em.mkVar("x", integer)); + Expr y(em.mkVar("y", integer)); + + /* y > x */ + Expr y_gt_x(em.mkExpr(kind::GT, y, x)); + + /* assert it */ + smt.assertFormula(y_gt_x); + + /* check */ + Result r(smt.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 + { + Expr heap_expr(smt.getSepHeapExpr()); + } + catch (const CVC4::RecoverableModalException& e) + { + caught_on_heap = true; + + /* Check we get the correct exception string */ + if (e.what() != expected) + { + return -1; + } + } + + /* test the nil expression */ + try + { + Expr nil_expr(smt.getSepNilExpr()); + } + catch (const CVC4::RecoverableModalException& 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) +{ + ExprManager em; + Options opts; + SmtEngine smt(&em); + + /* Setup some options for CVC4 */ + smt.setLogic("QF_ALL_SUPPORTED"); + smt.setOption("produce-models", SExpr("true")); + smt.setOption("incremental", SExpr("false")); + + /* Our integer type */ + Type integer(em.integerType()); + + /* A "random" constant */ + Rational val_for_random_constant(Rational(0xDEADBEEF)); + Expr random_constant(em.mkConst(val_for_random_constant)); + + /* Another random constant */ + Rational val_for_expr_nil_val(Rational(0xFBADBEEF)); + Expr expr_nil_val(em.mkConst(val_for_expr_nil_val)); + + /* Our nil term */ + Expr nil(em.mkNullaryOperator(integer, kind::SEP_NIL)); + + /* Our SMT constants */ + Expr x(em.mkVar("x", integer)); + Expr y(em.mkVar("y", integer)); + Expr p1(em.mkVar("p1", integer)); + Expr p2(em.mkVar("p2", integer)); + + /* Constraints on x and y */ + Expr x_equal_const(em.mkExpr(kind::EQUAL, x, random_constant)); + Expr y_gt_x(em.mkExpr(kind::GT, y, x)); + + /* Points-to expressions */ + Expr p1_to_x(em.mkExpr(kind::SEP_PTO, p1, x)); + Expr p2_to_y(em.mkExpr(kind::SEP_PTO, p2, y)); + + /* Heap -- the points-to have to be "starred"! */ + Expr heap(em.mkExpr(kind::SEP_STAR, p1_to_x, p2_to_y)); + + /* Constain "nil" to be something random */ + Expr fix_nil(em.mkExpr(kind::EQUAL, nil, expr_nil_val)); + + /* Add it all to the solver! */ + smt.assertFormula(x_equal_const); + smt.assertFormula(y_gt_x); + smt.assertFormula(heap); + smt.assertFormula(fix_nil); + + /* + * Incremental is disabled due to using separation logic, so don't query + * twice! + */ + Result r(smt.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 */ + Expr heap_expr(smt.getSepHeapExpr()); + Expr nil_expr(smt.getSepNilExpr()); + + /* 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" */ + Rational val_for_p1(smt.getValue(p1).getConst<CVC4::Rational>()); + Rational val_for_p2(smt.getValue(p2).getConst<CVC4::Rational>()); + + /* 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 (Expr child : heap_expr.getChildren()) + { + /* 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 */ + Rational addr( + smt.getValue(child.getChildren().at(0)).getConst<CVC4::Rational>()); + Rational value( + smt.getValue(child.getChildren().at(1)).getConst<CVC4::Rational>()); + + /* 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 != val_for_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 (value <= val_for_random_constant) + { + 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 */ + Rational value_for_nil = + smt.getValue(nil_expr.getChildren().at(1)).getConst<CVC4::Rational>(); + + /* + * The value for nil from the solver should be the value we originally tied + * nil to + */ + if (value_for_nil != val_for_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; +} |