From ad61299aa24a83f935daedab32440d25006e18bb Mon Sep 17 00:00:00 2001 From: ayveejay <41393247+ayveejay@users.noreply.github.com> Date: Wed, 1 Aug 2018 03:25:51 +0100 Subject: [PATCH] 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 --- src/smt/smt_engine.cpp | 32 ++-- src/smt/smt_engine.h | 11 +- test/system/Makefile.am | 3 +- test/system/sep_log_api.cpp | 313 ++++++++++++++++++++++++++++++++++++ 4 files changed, 338 insertions(+), 21 deletions(-) create mode 100644 test/system/sep_log_api.cpp diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 801711a13..cfafd63c4 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -5258,36 +5258,32 @@ Model* SmtEngine::getModel() { return m; } -Expr SmtEngine::getHeapExpr() +std::pair SmtEngine::getSepHeapAndNilExpr(void) { - NodeManagerScope nms(d_nodeManager); - Expr heap; - Expr nil; // we don't actually use this - Model* m = getModel(); - if (m->getHeapModel(heap, nil)) + if (!d_logic.isTheoryEnabled(THEORY_SEP)) { - return heap; + const char* msg = + "Cannot obtain separation logic expressions if not using the " + "separation logic theory."; + throw RecoverableModalException(msg); } - InternalError( - "SmtEngine::getHeapExpr(): failed to obtain heap expression from theory " - "model."); -} - -Expr SmtEngine::getNilExpr() -{ NodeManagerScope nms(d_nodeManager); - Expr heap; // we don't actually use this + Expr heap; Expr nil; Model* m = getModel(); if (m->getHeapModel(heap, nil)) { - return nil; + return std::make_pair(heap, nil); } InternalError( - "SmtEngine::getNilExpr(): failed to obtain nil expression from theory " - "model."); + "SmtEngine::getSepHeapAndNilExpr(): failed to obtain heap/nil " + "expressions from theory model."); } +Expr SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; } + +Expr SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; } + void SmtEngine::checkUnsatCore() { Assert(options::unsatCores(), "cannot check unsat core if unsat cores are turned off"); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 3536c5b1b..e4bd7d77d 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -429,6 +429,13 @@ class CVC4_PUBLIC SmtEngine { const std::vector& formals, Expr func); + /** + * Helper method to obtain both the heap and nil from the solver. Returns a + * std::pair where the first element is the heap expression and the second + * element is the nil expression. + */ + std::pair getSepHeapAndNilExpr(); + public: /** @@ -489,12 +496,12 @@ class CVC4_PUBLIC SmtEngine { /** * When using separation logic, obtain the expression for the heap. */ - Expr getHeapExpr(); + Expr getSepHeapExpr(); /** * When using separation logic, obtain the expression for nil. */ - Expr getNilExpr(); + Expr getSepNilExpr(); /** * Get an aspect of the current SMT execution environment. 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 +#include + +#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()); + Rational val_for_p2(smt.getValue(p2).getConst()); + + /* 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()); + Rational value( + smt.getValue(child.getChildren().at(1)).getConst()); + + /* 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(); + + /* + * 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; +} -- 2.30.2