Add a new delegate to allow API tracing

.appveyor.yml

@@ -77,6 +77,10 @@ on_finish:
       echo "Compressing and uploading JUnit HTML report..."
       7z a JUnit.html.zip JUnit.html
       Push-AppveyorArtifact JUnit.html.zip -DeploymentName "JUnit Report"
+  - ps: |
+      echo "Compressing and uploading trace files..."
+      7z a traces.zip .\traces
+      Push-AppveyorArtifact traces.zip -DeploymentName "Traces"
 
 cache:
   - C:\ant

.gitignore

@@ -60,6 +60,7 @@ solvers_maven_conf/*.asc
 /Javadoc
 /Javadoc-z3
 /gh-pages
+/traces
 
 .idea/
 

build/gitlab-ci.yml

@@ -132,6 +132,7 @@ spotbugs:
       - "JUnit.html"
       - "JUnit-coverage/"
       - "junit/coverage.xml"
+      - "traces/"
     when: always
     reports:
       junit: "junit/TESTS-TestSuites.xml"
@@ -143,6 +144,7 @@ spotbugs:
   artifacts:
     paths:
       - "JUnit.html" # no coverage files available
+      - "traces/"
 
 unit-tests:x86_64:jdk-11:
   extends: .unit-tests

scripts/reduceTrace.py

@@ -0,0 +1,128 @@
+#!/usr/bin/env python3
+
+# This file is part of JavaSMT,
+# an API wrapper for a collection of SMT solvers:
+# https://github.com/sosy-lab/java-smt
+#
+# SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
+#
+# SPDX-License-Identifier: Apache-2.0
+
+import re
+import sys
+from collections import defaultdict
+from pathlib import Path
+
+
+# Read a trace file
+def readTrace(path):
+    with open(path) as file:
+        return [line.rstrip() for line in file]
+
+
+# Build a map with line numbers for all variable definitions
+def getLinesForDefinitions(trace):
+    lineNumber = 1
+    lineDefs = dict()
+    for line in trace:
+        if line.find('=') >= 0:
+            leftSide = line[0:(line.find('=') - 1)]
+            name = re.match('var (.*)', leftSide)
+            lineDefs[name.group(1)] = lineNumber
+        lineNumber = lineNumber + 1
+    return lineDefs
+
+
+# Build a dependency graph for the definitions
+# Maps from variables to the places where they are used
+def buildDependencies(lineDefs, trace):
+    lineNumber = 1
+    deps = defaultdict(list)
+    for line in trace:
+        expr = line[(line.find('=') + 2):] if line.find('=') >= 0 else line
+        object = expr[0:expr.find('.')]
+        if object[0].islower():
+            deps[lineDefs[object]].append(lineNumber)
+        # FIXME Parse the expression to get the variables
+        for m in re.finditer('(config|logger|notifier|var[0-9]+)', expr):
+            deps[lineDefs[m.group()]].append(lineNumber)
+        lineNumber += 1
+    return deps
+
+
+# Collect all top-level statements
+# Top-level statements are:
+#  *.addConstraint(*)
+#  *.isUnsat()
+#  *.getModel()
+#  *.asList()
+# FIXME Finish this list
+def usedTopLevel(lineDefs, trace):
+    tl = set()
+    for line in trace:
+        m = re.fullmatch(
+            'var (var[0-9]+) = (var[0-9]+).(isUnsat\\(\\)|getModel\\(\\)|asList\\(\\)|addConstraint\\((var[0-9]+)\\));',
+            line)
+        if m != None:
+            tl.add(lineDefs[m.group(1)])
+    return tl
+
+
+# Calculate the closure of all used definitions, starting with the top-level statements
+def usedClosure(tl, deps):
+    cl = set()
+    st = set(tl)
+    while cl.union(st) != cl:
+        cl = cl.union(st)
+        st = set()
+        for (key, val) in deps.items():
+            if set(val).intersection(cl) != set():
+                st.add(key)
+    return cl
+
+
+# Keep only statements and definitions that are used
+def filterUnused(used, trace):
+    lineNumber = 1
+    reduced = []
+    for line in trace:
+        if line.find('=') == -1 or lineNumber in used:
+            reduced.append(line)
+        lineNumber += 1
+    return reduced
+
+
+# Remove all definitions that are not used (recursively)
+def removeDeadCode(trace):
+    lineDefs = getLinesForDefinitions(trace)
+    deps = buildDependencies(lineDefs, trace)
+    tl = usedTopLevel(lineDefs, trace)
+    cl = usedClosure(tl, deps)
+    return filterUnused(cl, trace)
+
+
+if __name__ == '__main__':
+    arg = sys.argv
+    if not len(sys.argv) == 2:
+        print('Expecting a path to a trace file as argument')
+        exit(-1)
+
+    path = Path(sys.argv[1])
+    if not (path.is_file()):
+        print(f'Could not find file "{path}"')
+        exit(-1)
+
+    # We'll use multiple passes to reduce the size of the trace:
+    # 1. Read the trace
+    # 2. Remove unused code
+    # 3. Remove unnecessary toplevel commands
+    # 4. Loop: Remove aliasing (by duplicating the definitions)
+    # 5.    Loop: Reduce terms
+    # 6. Remove unused prover environments
+
+    # TODO Implement steps 3-6
+    # TODO Check that the reduced trace still crashes
+
+    trace = readTrace(path)
+    for line in removeDeadCode(trace):
+        print(line)

src/org/sosy_lab/java_smt/SolverContextFactory.java

@@ -30,6 +30,7 @@
 import org.sosy_lab.java_smt.delegate.logging.LoggingSolverContext;
 import org.sosy_lab.java_smt.delegate.statistics.StatisticsSolverContext;
 import org.sosy_lab.java_smt.delegate.synchronize.SynchronizedSolverContext;
+import org.sosy_lab.java_smt.delegate.trace.TraceSolverContext;
 import org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaSolverContext;
 import org.sosy_lab.java_smt.solvers.boolector.BoolectorSolverContext;
 import org.sosy_lab.java_smt.solvers.cvc4.CVC4SolverContext;
@@ -95,6 +96,11 @@ public enum Solvers {
   @Option(secure = true, description = "Apply additional checks to catch common user errors.")
   private boolean useDebugMode = false;
 
+  @Option(
+      secure = true,
+      description = "Enable API tracing to record all calls to the JavaSMT library")
+  private boolean trace = false;
+
   @Option(
       secure = true,
       description = "Counts all operations and interactions towards the SMT solver.")
@@ -230,6 +236,9 @@ public SolverContext generateContext(Solvers solverToCreate)
     if (useDebugMode) {
       context = new DebuggingSolverContext(solverToCreate, config, context);
     }
+    if (trace) {
+      context = new TraceSolverContext(solverToCreate, config, context);
+    }
     if (collectStatistics) {
       // statistics need to be the most outer wrapping layer.
       context = new StatisticsSolverContext(context);

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

@@ -205,6 +205,12 @@ public enum FunctionDeclarationKind {
   /** Cast a signed bitvector to a floating-point number. */
   BV_SCASTTO_FP,
 
+  /** Convert an unsigned bitvector to integer. The result is in [0, 2^size - 1]. */
+  UBV_TO_INT,
+
+  /** Convert a signed bitvector to integer. The result is in [-2^(size-1), 2^(size-1) - 1]. */
+  SBV_TO_INT,
+
   // Simple floating point operations
 
   /** Negation of a floating point. */
@@ -304,6 +310,8 @@ public enum FunctionDeclarationKind {
   STR_TO_CODE,
   STR_LT,
   STR_LE,
+
+  RE_NONE,
   RE_PLUS,
   RE_STAR,
   RE_OPTIONAL,
@@ -314,6 +322,13 @@ public enum FunctionDeclarationKind {
   RE_COMPLEMENT,
   RE_DIFFERENCE,
 
+  // Separation logic
+  SEP_EMP,
+  SEP_NIL,
+  SEP_PTO,
+  SEP_STAR,
+  SEP_WAND,
+
   // default case
 
   /**

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

@@ -80,8 +80,8 @@ public interface SLFormulaManager {
    *
    * @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.
+   * @param pAddressType 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);
+  <AF extends Formula, AT extends FormulaType<AF>> AF makeNilElement(AT pAddressType);
 }

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

@@ -207,11 +207,15 @@ public ResultFormulaType sum(List<ParamFormulaType> operands) {
   }
 
   protected TFormulaInfo sumImpl(List<TFormulaInfo> operands) {
-    TFormulaInfo result = makeNumberImpl(0);
-    for (TFormulaInfo operand : operands) {
-      result = add(result, operand);
+    if (operands.isEmpty()) {
+      return makeNumberImpl(0);
+    } else {
+      TFormulaInfo result = operands.get(0);
+      for (TFormulaInfo operand : operands.subList(1, operands.size())) {
+        result = add(result, operand);
+      }
+      return result;
     }
-    return result;
   }
 
   @Override

src/org/sosy_lab/java_smt/delegate/trace/TraceArrayFormulaManager.java

@@ -0,0 +1,100 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+package org.sosy_lab.java_smt.delegate.trace;
+
+import org.sosy_lab.java_smt.api.ArrayFormula;
+import org.sosy_lab.java_smt.api.ArrayFormulaManager;
+import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.Formula;
+import org.sosy_lab.java_smt.api.FormulaType;
+
+@SuppressWarnings("MethodTypeParameterName")
+public class TraceArrayFormulaManager implements ArrayFormulaManager {
+  private final ArrayFormulaManager delegate;
+  private final TraceLogger logger;
+
+  TraceArrayFormulaManager(ArrayFormulaManager pDelegate, TraceLogger pLogger) {
+    delegate = pDelegate;
+    logger = pLogger;
+  }
+
+  @Override
+  public <TI extends Formula, TE extends Formula> TE select(
+      ArrayFormula<TI, TE> pArray, TI pIndex) {
+    return logger.logDef(
+        "mgr.getArrayFormulaManager()",
+        String.format("select(%s, %s)", logger.toVariable(pArray), logger.toVariable(pIndex)),
+        () -> delegate.select(pArray, pIndex));
+  }
+
+  @Override
+  public <TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> store(
+      ArrayFormula<TI, TE> pArray, TI pIndex, TE pValue) {
+    return logger.logDef(
+        "mgr.getArrayFormulaManager()",
+        String.format(
+            "store(%s, %s, %s)",
+            logger.toVariable(pArray), logger.toVariable(pIndex), logger.toVariable(pValue)),
+        () -> delegate.store(pArray, pIndex, pValue));
+  }
+
+  @Override
+  public <
+          TI extends Formula,
+          TE extends Formula,
+          FTI extends FormulaType<TI>,
+          FTE extends FormulaType<TE>>
+      ArrayFormula<TI, TE> makeArray(String pName, FTI pIndexType, FTE pElementType) {
+    return logger.logDef(
+        "mgr.getArrayFormulaManager()",
+        String.format(
+            "makeArray(\"%s\", %s, %s)",
+            pName, logger.printFormulaType(pIndexType), logger.printFormulaType(pElementType)),
+        () -> delegate.makeArray(pName, pIndexType, pElementType));
+  }
+
+  @Override
+  public <
+          TI extends Formula,
+          TE extends Formula,
+          FTI extends FormulaType<TI>,
+          FTE extends FormulaType<TE>>
+      ArrayFormula<TI, TE> makeArray(FTI pIndexType, FTE pElementType, TE defaultElement) {
+    return logger.logDef(
+        "mgr.getArrayFormulaManager()",
+        String.format(
+            "makeArray(%s, %s, %s)",
+            logger.printFormulaType(pIndexType),
+            logger.printFormulaType(pElementType),
+            logger.toVariable(defaultElement)),
+        () -> delegate.makeArray(pIndexType, pElementType, defaultElement));
+  }
+
+  @Override
+  public <TI extends Formula, TE extends Formula> BooleanFormula equivalence(
+      ArrayFormula<TI, TE> pArray1, ArrayFormula<TI, TE> pArray2) {
+    return logger.logDef(
+        "mgr.getArrayFormulaManager()",
+        String.format(
+            "equivalence(%s, %s)", logger.toVariable(pArray1), logger.toVariable(pArray2)),
+        () -> delegate.equivalence(pArray1, pArray2));
+  }
+
+  @Override
+  public <TI extends Formula> FormulaType<TI> getIndexType(ArrayFormula<TI, ?> pArray) {
+    return delegate.getIndexType(pArray);
+  }
+
+  @Override
+  public <TE extends Formula> FormulaType<TE> getElementType(ArrayFormula<?, TE> pArray) {
+    return delegate.getElementType(pArray);
+  }
+}