Package de.uzl.its.swat.symbolic.trace

Class SymbolicTraceHandler

java.lang.Object
de.uzl.its.swat.symbolic.trace.SymbolicTraceHandler
public class SymbolicTraceHandler extends Object
Manages access to the trace of the symbolic execution. This class should be used for all access to the trace package.

  • Constructor Details

    • SymbolicTraceHandler

      public SymbolicTraceHandler()
      Constructs a new SymbolicTraceHandler.

  • Method Details

    • checkAndSetBranch

      public void checkAndSetBranch(boolean result, org.sosy_lab.java_smt.api.BooleanFormula constraint, int iid)
      Checks the result of a branch and adds the corresponding constraint to the symbolic trace.
      Parameters:
      result - Whether the branch was taken (true) or not (false).
      constraint - The constraint of the branch.
      iid - The iid of the branch instruction.

    • addSpecialElement

      public void addSpecialElement(int iid, String inst)
      Adds a special element to the symbolic trace. This is used to catch all unsupported branching behaviour.
      Parameters:
      iid - The iid of the special instruction.
      inst - The instruction of the special instruction.

    • addInput

      public void addInput(String name, Value<?,?> value)
      Adds an input to the symbolic trace.
      Parameters:
      name - The name of the input.
      value - The value of the input.

    • getTraceDTO

      public String getTraceDTO()
      Encodes the symbolic trace as a JSON string.
      Returns:
      The symbolic trace encoded as a JSON string.

    • dumpConstraints

      public void dumpConstraints(org.slf4j.Logger logger)
      Dumps all constraints to the logger. Used for debugging purposes and by the LocalSolver.
      Parameters:
      logger - The logger to dump the constraints to.

    • dumpInputs

      public ArrayList<String> dumpInputs()
      Returns all imputs as an array list of strings. Used for debugging purposes and by the LocalSolver.
      Returns:
      The inputs as an array list of strings.

    • getTraceSize

      public int getTraceSize()
      Returns the size of the symbolic trace.
      Returns:
      The size of the symbolic trace.

    • getBranchConstraints

      public HashMap<Integer,org.sosy_lab.java_smt.api.BooleanFormula> getBranchConstraints()
      Fetches the branch constraints from the symbolic trace.
      Returns:
      The branch constraints from the symbolic trace.

    • getPathConstraints

      public HashMap<Integer,org.sosy_lab.java_smt.api.BooleanFormula> getPathConstraints(int iid) throws IllegalArgumentException
      Fetches all path constraints that are required for a specific branch constraints
      Parameters:
      iid - The id of the branch constraint
      Returns:
      The path constraints
      Throws:
      IllegalArgumentException

    • getInputBounds

      public ArrayList<org.sosy_lab.java_smt.api.BooleanFormula> getInputBounds()
      Fetches the input bounds from the symbolic trace. Each symbolic input has two bounds, the lower and the upper bound of the respective datatype.
      Returns:
      The input bounds from the symbolic trace.