Merge pull request #517 from sosy-lab/feat/improve-separation-logic

Improve separation logic (CVC4 and CVC5)

Author: kfriedberger

src/org/sosy_lab/java_smt/api/SLFormulaManager.java

@@ -2,7 +2,7 @@
 // an API wrapper for a collection of SMT solvers:
 // https://github.com/sosy-lab/java-smt
 //
-// SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+// SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
 //
 // SPDX-License-Identifier: Apache-2.0
 
@@ -15,18 +15,73 @@
  * all formulae for one heap need to use matching types (sorts) for the AdressFormulae and
  * ValueFormulae. The user has to take care of this, otherwise the {@link ProverEnvironment}
  * complains at runtime!
+ *
+ * @see <a href="https://en.wikipedia.org/wiki/Separation_logic">Separation Logic</a>
+ * @see <a href="https://cacm.acm.org/research/separation-logic/">Separation Logic</a>
+ * @see <a
+ *     href="https://www.cs.cmu.edu/afs/cs.cmu.edu/project/fox-19/member/jcr/www15818As2011/cs818A3-11.html">15-818A3
+ *     Introduction to Separation Logic (6 units) Spring 2011</a>
+ * @see <a href="https://www.philipzucker.com/executable-seperation">Modeling Separation Logic with
+ *     Python Dicts and Z3</a>
  */
 @SuppressWarnings("MethodTypeParameterName")
 public interface SLFormulaManager {
 
+  /**
+   * Creates a formula representing the "separating conjunction" (*) of two Boolean formulas. In
+   * separation logic, the separating conjunction asserts that the two formulas describe disjoint
+   * parts of the heap. It is similar to the logical AND operator, but with the additional
+   * constraint that the memory regions described by the two formulas do not overlap.
+   *
+   * @return a Boolean formula representing the separating conjunction of {@code f1} and {@code f2}.
+   */
   BooleanFormula makeStar(BooleanFormula f1, BooleanFormula f2);
 
+  /**
+   * Creates a formula representing a "points-to" relation in the heap. The "points-to" relation
+   * asserts that a pointer points to a specific value in memory.
+   *
+   * @param <AF> the type of the address formula.
+   * @param <VF> the type of the value formula.
+   * @param ptr the pointer formula.
+   * @param to the value formula.
+   * @return a Boolean formula representing the "points-to" relation.
+   */
   <AF extends Formula, VF extends Formula> BooleanFormula makePointsTo(AF ptr, VF to);
 
+  /**
+   * Creates a formula representing the "magic wand" (-*) operator in separation logic. The "magic
+   * wand" operator asserts that if the first formula holds, then the second formula can be added to
+   * the heap without conflict. It is a form of implication (=&gt;) that takes into account the
+   * disjointness of memory regions.
+   *
+   * @return a Boolean formula representing the "magic wand" of {@code f1} and {@code f2}.
+   */
   BooleanFormula makeMagicWand(BooleanFormula f1, BooleanFormula f2);
 
+  /**
+   * Creates a formula representing an empty heap. The empty heap formula asserts that no memory is
+   * allocated for the given address and value types.
+   *
+   * @param <AF> the type of the address formula.
+   * @param <VF> the type of the value formula.
+   * @param <AT> the type of the address formula type.
+   * @param <VT> the type of the value formula type.
+   * @param pAddressType the type of the address formula.
+   * @param pValueType the type of the value formula.
+   * @return a Boolean formula representing an empty heap.
+   */
   <AF extends Formula, VF extends Formula, AT extends FormulaType<AF>, VT extends FormulaType<VF>>
-      BooleanFormula makeEmptyHeap(AT pAdressType, VT pValueType);
+      BooleanFormula makeEmptyHeap(AT pAddressType, VT pValueType);
 
+  /**
+   * Creates a formula representing the "nil" element for a given address type. The "nil" element is
+   * used to represent a null pointer or an unallocated memory address.
+   *
+   * @param <AF> the type of the address formula.
+   * @param <AT> the type of the address formula type.
+   * @param pAdressType the type of the address formula.
+   * @return a formula representing the "nil" element for the given address type.
+   */
   <AF extends Formula, AT extends FormulaType<AF>> AF makeNilElement(AT pAdressType);
 }

src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java

@@ -29,7 +29,7 @@
 
 public abstract class AbstractProver<T> implements BasicProverEnvironment<T> {
 
-  private final boolean generateModels;
+  protected final boolean generateModels;
   private final boolean generateAllSat;
   protected final boolean generateUnsatCores;
   private final boolean generateUnsatCoresOverAssumptions;

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4Model.java

@@ -73,7 +73,7 @@ private ImmutableList<ValueAssignment> generateModel() {
 
   // TODO this method is highly recursive and should be rewritten with a proper visitor
   private void recursiveAssignmentFinder(ImmutableSet.Builder<ValueAssignment> builder, Expr expr) {
-    if (expr.isConst() || expr.isNull()) {
+    if (expr.getKind() == Kind.SEP_NIL || expr.isConst() || expr.isNull()) {
       // We don't care about consts.
       return;
     } else if (expr.isVariable() && expr.getKind() == Kind.BOUND_VARIABLE) {

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SLFormulaManager.java

@@ -45,6 +45,6 @@ protected Expr makeEmptyHeap(Type pT1, Type pT2) {
 
   @Override
   protected Expr makeNilElement(Type pType) {
-    return exprManager.mkExpr(Kind.SEP_NIL, pType.mkGroundTerm());
+    return exprManager.mkNullaryOperator(pType, Kind.SEP_NIL);
   }
 }

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java

@@ -40,6 +40,7 @@ class CVC4TheoremProver extends AbstractProverWithAllSat<Void>
     implements ProverEnvironment, BasicProverEnvironment<Void> {
 
   private final CVC4FormulaCreator creator;
+  private final int randomSeed;
   SmtEngine smtEngine; // final except for SL theory
   private boolean changedSinceLastSatQuery = false;
 
@@ -50,37 +51,45 @@ class CVC4TheoremProver extends AbstractProverWithAllSat<Void>
    * <p>TODO If the overhead of importing/exporting the expressions is too expensive, we can disable
    * this behavior. This change would cost us the flexibility of setting options per Prover.
    */
-  private final ExprManager exprManager = new ExprManager();
+  private ExprManager exprManager; // final except for SL theory
 
   /** We copy expression between different ExprManagers. The map serves as cache. */
-  private final ExprManagerMapCollection exportMapping = new ExprManagerMapCollection();
+  private ExprManagerMapCollection exportMapping; // final except for SL theory
 
   // CVC4 does not support separation logic in incremental mode.
   private final boolean incremental;
 
   protected CVC4TheoremProver(
       CVC4FormulaCreator pFormulaCreator,
       ShutdownNotifier pShutdownNotifier,
-      int randomSeed,
+      int pRandomSeed,
       Set<ProverOptions> pOptions,
       BooleanFormulaManager pBmgr) {
     super(pOptions, pBmgr, pShutdownNotifier);
 
     creator = pFormulaCreator;
-    smtEngine = new SmtEngine(exprManager);
+    randomSeed = pRandomSeed;
     incremental = !enableSL;
 
-    setOptions(randomSeed, pOptions);
+    createNewEngine();
   }
 
-  private void setOptions(int randomSeed, Set<ProverOptions> pOptions) {
-    smtEngine.setOption("incremental", new SExpr(incremental));
-    if (pOptions.contains(ProverOptions.GENERATE_MODELS)) {
-      smtEngine.setOption("produce-models", new SExpr(true));
+  private void createNewEngine() {
+    if (smtEngine != null) {
+      smtEngine.delete(); // cleanup
+    }
+    if (exportMapping != null) {
+      exportMapping.delete();
     }
-    if (pOptions.contains(ProverOptions.GENERATE_UNSAT_CORE)) {
-      smtEngine.setOption("produce-unsat-cores", new SExpr(true));
+    if (exprManager != null) {
+      exprManager.delete(); // cleanup
     }
+    exprManager = new ExprManager();
+    smtEngine = new SmtEngine(exprManager);
+    exportMapping = new ExprManagerMapCollection();
+    smtEngine.setOption("incremental", new SExpr(incremental));
+    smtEngine.setOption("produce-models", new SExpr(generateModels));
+    smtEngine.setOption("produce-unsat-cores", new SExpr(generateUnsatCores));
     smtEngine.setOption("produce-assertions", new SExpr(true));
     smtEngine.setOption("dump-models", new SExpr(true));
     // smtEngine.setOption("produce-unsat-cores", new SExpr(true));
@@ -93,10 +102,6 @@ private void setOptions(int randomSeed, Set<ProverOptions> pOptions) {
     smtEngine.setOption("full-saturate-quant", new SExpr(true));
   }
 
-  protected void setOptionForIncremental() {
-    smtEngine.setOption("incremental", new SExpr(true));
-  }
-
   /** import an expression from global context into this prover's context. */
   protected Expr importExpr(Expr expr) {
     return expr.exportTo(exprManager, exportMapping);
@@ -172,13 +177,9 @@ protected Evaluator getEvaluatorWithoutChecks() {
   }
 
   private void setChanged() {
-    closeAllEvaluators();
     if (!changedSinceLastSatQuery) {
       changedSinceLastSatQuery = true;
-      if (!incremental) {
-        // create a new clean smtEngine
-        smtEngine = new SmtEngine(exprManager);
-      }
+      closeAllEvaluators();
     }
   }
 
@@ -196,17 +197,20 @@ public boolean isUnsat() throws InterruptedException, SolverException {
     closeAllEvaluators();
     changedSinceLastSatQuery = false;
     if (!incremental) {
-      for (BooleanFormula f : getAssertedFormulas()) {
-        assertFormula(f);
-      }
+      // in non-incremental mode, we need to create a new solver instance for each sat check
+      createNewEngine();
+      getAssertedFormulas().forEach(this::assertFormula);
     }
 
     Result result;
     try (ShutdownHook hook = new ShutdownHook(shutdownNotifier, smtEngine::interrupt)) {
       shutdownNotifier.shutdownIfNecessary();
       result = smtEngine.checkSat();
+    } catch (Exception e) {
+      throw new SolverException("CVC4 failed during satisfiability check", e);
+    } finally {
+      shutdownNotifier.shutdownIfNecessary();
     }
-    shutdownNotifier.shutdownIfNecessary();
     return convertSatResult(result);
   }