Split state variables and symbolic variables. Stricter type checking. (…

…#3987) * Split state variables and symbolic variables. Stricter type checking. * Rename variables appropriately. * IWYU. * Refactor the concolic execution model. Push concolic refresh into final state. * Fix up gtests. * Remove flawed test. * Move packet variables out of the execution state. * State variables never used the incarnation count. Remove. * There is no need to look up the declaration in convertPathExpr.
p4lang · Apr 28, 2023 · 06f520f · 06f520f
1 parent 30d953b
commit 06f520f
Show file tree

Hide file tree

Showing 86 changed files with 959 additions and 961 deletions.
diff --git a/backends/p4tools/common/CMakeLists.txt b/backends/p4tools/common/CMakeLists.txt
@@ -43,7 +43,7 @@ set(
   lib/trace_event.cpp
   lib/trace_event_types.cpp
   lib/util.cpp
-  lib/zombie.cpp
+  lib/variables.cpp
 )
 
 add_p4tools_library(p4tools-common ${P4C_TOOLS_COMMON_SOURCES})

diff --git a/backends/p4tools/common/compiler/convert_hs_index.h b/backends/p4tools/common/compiler/convert_hs_index.h
@@ -1,7 +1,7 @@
 #ifndef BACKENDS_P4TOOLS_COMMON_COMPILER_CONVERT_HS_INDEX_H_
 #define BACKENDS_P4TOOLS_COMMON_COMPILER_CONVERT_HS_INDEX_H_
 
-#include <stddef.h>
+#include <cstddef>
 
 #include "ir/ir.h"
 #include "ir/node.h"

diff --git a/backends/p4tools/common/core/solver.h b/backends/p4tools/common/core/solver.h
@@ -4,7 +4,11 @@
 #include <optional>
 #include <vector>
 
-#include "backends/p4tools/common/lib/model.h"
+#include <boost/container/flat_map.hpp>
+#include <boost/container/flat_set.hpp>
+
+#include "ir/ir.h"
+#include "lib/castable.h"
 #include "lib/cstring.h"
 
 namespace P4Tools {
@@ -13,6 +17,19 @@ namespace P4Tools {
 // TODO: This should implement AbstractRepCheckedNode<Constraint>.
 using Constraint = IR::Expression;
 
+/// Comparator to compare SymbolicVariable pointers.
+struct SymbolicVarComp {
+    bool operator()(const IR::SymbolicVariable *s1, const IR::SymbolicVariable *s2) const {
+        return s1->operator<(*s2);
+    }
+};
+
+/// This type maps symbolic variables to their value assigned by the solver.
+using SymbolicMapping = boost::container::flat_map<const IR::SymbolicVariable *,
+                                                   const IR::Expression *, SymbolicVarComp>;
+
+using SymbolicSet = boost::container::flat_set<const IR::SymbolicVariable *, SymbolicVarComp>;
+
 /// Provides a higher-level interface for an SMT solver.
 class AbstractSolver : public ICastable {
  public:
@@ -40,13 +57,13 @@ class AbstractSolver : public ICastable {
     /// @checkSat returned anything other than true, if there was no such previous call, or if the
     /// state in the solver has changed since the last such call (e.g., more assertions have been
     /// made).
-    virtual const Model *getModel() const = 0;
+    [[nodiscard]] virtual const SymbolicMapping &getSymbolicMapping() const = 0;
 
     /// Saves solver state to the given JSON generator.
     virtual void toJSON(JSONGenerator &) const = 0;
 
     /// @returns whether this solver is incremental.
-    virtual bool isInIncrementalMode() const = 0;
+    [[nodiscard]] virtual bool isInIncrementalMode() const = 0;
 
     /// Cast an abstract solver to its specific sub type.
     /// Casts involving "const" have to explicit in this case. This is necessary because abstract

diff --git a/backends/p4tools/common/core/z3_solver.cpp b/backends/p4tools/common/core/z3_solver.cpp
@@ -8,13 +8,11 @@
 #include <iterator>
 #include <list>
 #include <map>
-#include <ostream>
 #include <string>
 #include <utility>
 
 #include <boost/multiprecision/cpp_int.hpp>
 
-#include "backends/p4tools/common/lib/model.h"
 #include "ir/ir.h"
 #include "ir/irutils.h"
 #include "ir/json_loader.h"  // IWYU pragma: keep
@@ -70,8 +68,7 @@ class Z3Translator : public virtual Inspector {
     bool preorder(const IR::BoolLiteral *boolLiteral) override;
 
     /// Translates variables.
-    bool preorder(const IR::Member *member) override;
-    bool preorder(const IR::ConcolicVariable *var) override;
+    bool preorder(const IR::SymbolicVariable *var) override;
 
     // Translations for unary operations.
     bool preorder(const IR::Neg *op) override;
@@ -161,35 +158,21 @@ z3::sort Z3Solver::toSort(const IR::Type *type) {
     BUG("Z3Solver: unimplemented type %1%: %2% ", type->node_type_name(), type);
 }
 
-std::string Z3Solver::generateName(const IR::StateVariable &var) const {
+std::string Z3Solver::generateName(const IR::SymbolicVariable &var) {
     std::ostringstream ostr;
-    generateName(ostr, var);
+    ostr << var;
     return ostr.str();
 }
 
-void Z3Solver::generateName(std::ostringstream &ostr, const IR::StateVariable &var) const {
-    // Recurse into the parent member expression to retrieve the full name of the variable.
-    if (const auto *next = var->expr->to<IR::Member>()) {
-        generateName(ostr, next);
-    } else {
-        const auto *path = var->expr->to<IR::PathExpression>();
-        BUG_CHECK(path, "Z3Solver: expected to be a PathExpression: %1%", var->expr);
-        ostr << path->path->name;
-    }
-
-    ostr << "." << var->member;
-}
-
-z3::expr Z3Solver::declareVar(const IR::StateVariable &var) {
-    BUG_CHECK(var, "Z3Solver: attempted to declare a non-member: %1%", var);
-    auto sort = toSort(var->type);
+z3::expr Z3Solver::declareVar(const IR::SymbolicVariable &var) {
+    auto sort = toSort(var.type);
     auto expr = z3context.constant(generateName(var).c_str(), sort);
     BUG_CHECK(
         !declaredVarsById.empty(),
         "DeclaredVarsById should have at least one entry! Check if push() was used correctly.");
     // Need to take the reference here to avoid accidental copies.
     auto *latestVars = &declaredVarsById.back();
-    latestVars->emplace(expr.id(), var);
+    latestVars->emplace(expr.id(), &var);
     return expr;
 }
 
@@ -320,17 +303,17 @@ void Z3Solver::asrt(const Constraint *assertion) {
     }
 }
 
-const Model *Z3Solver::getModel() const {
-    auto *result = new Model();
+const SymbolicMapping &Z3Solver::getSymbolicMapping() const {
+    auto *result = new SymbolicMapping();
     // First, collect a map of all the declared variables we have encountered in the stack.
-    std::map<unsigned int, IR::StateVariable> declaredVars;
+    std::map<unsigned int, const IR::SymbolicVariable *> declaredVars;
     for (auto it = declaredVarsById.rbegin(); it != declaredVarsById.rend(); ++it) {
         auto latestVars = *it;
         for (auto var : latestVars) {
             declaredVars.emplace(var);
         }
     }
-    // Then, get the model and match each declaration in the model to its IR::StateVariable.
+    // Then, get the model and match each declaration in the model to its IR::SymbolicVariable.
     try {
         Util::ScopedTimer ctZ3("z3");
         Util::ScopedTimer ctCheckSat("getModel");
@@ -346,13 +329,13 @@ const Model *Z3Solver::getModel() const {
             auto z3Expr = z3Func();
             auto z3Value = z3Model.get_const_interp(z3Func);
 
-            // Convert to a state variable and value.
+            // Convert to a symbolic variable and value.
             auto exprId = z3Expr.id();
             BUG_CHECK(declaredVars.count(exprId) > 0, "Z3Solver: unknown variable declaration: %1%",
                       z3Expr);
-            const auto stateVar = declaredVars.at(exprId);
-            const auto *value = toLiteral(z3Value, stateVar->type);
-            result->emplace(stateVar, value);
+            const auto *symbolicVar = declaredVars.at(exprId);
+            const auto *value = toLiteral(z3Value, symbolicVar->type);
+            result->emplace(symbolicVar, value);
         }
     } catch (z3::exception &e) {
         BUG("Z3Solver : Z3 exception: %1%", e.msg());
@@ -361,7 +344,7 @@ const Model *Z3Solver::getModel() const {
     } catch (...) {
         BUG("Z3Solver : unknown segmentation fault in getModel");
     }
-    return result;
+    return *result;
 }
 
 const IR::Literal *Z3Solver::toLiteral(const z3::expr &e, const IR::Type *type) {
@@ -533,14 +516,8 @@ bool Z3Translator::preorder(const IR::BoolLiteral *boolLiteral) {
     return false;
 }
 
-bool Z3Translator::preorder(const IR::Member *member) {
-    result = solver.declareVar(member);
-    return false;
-}
-
-bool Z3Translator::preorder(const IR::ConcolicVariable *var) {
-    /// Declare the member contained within the concolic variable
-    result = solver.declareVar(var->concolicMember);
+bool Z3Translator::preorder(const IR::SymbolicVariable *var) {
+    result = solver.declareVar(*var);
     return false;
 }
 

diff --git a/backends/p4tools/common/core/z3_solver.h b/backends/p4tools/common/core/z3_solver.h
@@ -1,16 +1,15 @@
 #ifndef BACKENDS_P4TOOLS_COMMON_CORE_Z3_SOLVER_H_
 #define BACKENDS_P4TOOLS_COMMON_CORE_Z3_SOLVER_H_
 
-#include <stddef.h>
 #include <z3++.h>
 
+#include <cstddef>
 #include <iosfwd>
 #include <optional>
 #include <string>
 #include <vector>
 
 #include "backends/p4tools/common/core/solver.h"
-#include "backends/p4tools/common/lib/model.h"
 #include "ir/ir.h"
 #include "ir/json_generator.h"
 #include "lib/cstring.h"
@@ -22,7 +21,7 @@ namespace P4Tools {
 /// A stack of maps, which map Z3-internal expression IDs of declared Z3 variables to their
 /// corresponding P4 state variable. The maps are pushed and pop according to the solver push() and
 /// pop() operations.
-using Z3DeclareVariablesMap = std::vector<ordered_map<unsigned, const IR::StateVariable>>;
+using Z3DeclaredVariablesMap = std::vector<ordered_map<unsigned, const IR::SymbolicVariable *>>;
 
 /// A Z3-based implementation of AbstractSolver. Encapsulates a z3::solver and a z3::context.
 class Z3Solver : public AbstractSolver {
@@ -31,7 +30,7 @@ class Z3Solver : public AbstractSolver {
     friend class Z3SolverAccessor;
 
  public:
-    virtual ~Z3Solver() = default;
+    ~Z3Solver() override = default;
 
     explicit Z3Solver(bool isIncremental = true,
                       std::optional<std::istream *> inOpt = std::nullopt);
@@ -44,20 +43,20 @@ class Z3Solver : public AbstractSolver {
 
     std::optional<bool> checkSat(const std::vector<const Constraint *> &asserts) override;
 
-    const Model *getModel() const override;
+    [[nodiscard]] const SymbolicMapping &getSymbolicMapping() const override;
 
     void toJSON(JSONGenerator & /*json*/) const override;
 
-    bool isInIncrementalMode() const override;
+    [[nodiscard]] bool isInIncrementalMode() const override;
 
     /// Get the actual Z3 solver backing this class.
-    const z3::solver &getZ3Solver() const;
+    [[nodiscard]] const z3::solver &getZ3Solver() const;
 
     /// Get the actual Z3 context that this class uses.
-    const z3::context &getZ3Ctx() const;
+    [[nodiscard]] const z3::context &getZ3Ctx() const;
 
     /// @returns the list of active assertions on this solver.
-    safe_vector<const Constraint *> getAssertions() const;
+    [[nodiscard]] safe_vector<const Constraint *> getAssertions() const;
 
  private:
     /// Resets the internal state: pops all assertions from previous solver
@@ -76,17 +75,13 @@ class Z3Solver : public AbstractSolver {
     /// Converts a P4 type to a Z3 sort.
     z3::sort toSort(const IR::Type *type);
 
-    /// Declares the given state variable to Z3.
+    /// Declares the given symbolic variable to Z3.
     ///
     /// @returns the resulting Z3 variable.
-    z3::expr declareVar(const IR::StateVariable &var);
+    z3::expr declareVar(const IR::SymbolicVariable &var);
 
-    /// Generates a Z3 name for the given variable.
-    std::string generateName(const IR::StateVariable &var) const;
-
-    /// Generates a Z3 name for the given variable. The generated name is written to the given
-    /// output stream.
-    void generateName(std::ostringstream &ostr, const IR::StateVariable &var) const;
+    /// Generates a Z3 name for the given symbolic variable.
+    [[nodiscard]] static std::string generateName(const IR::SymbolicVariable &var);
 
     /// Converts a Z3 expression to an IR::Literal with the given type.
     static const IR::Literal *toLiteral(const z3::expr &e, const IR::Type *type);
@@ -107,7 +102,7 @@ class Z3Solver : public AbstractSolver {
 
     /// For each state variable declared in the solver, this maps the variable's Z3 expression ID
     /// to the original state variable.
-    Z3DeclareVariablesMap declaredVarsById;
+    Z3DeclaredVariablesMap declaredVarsById;
 
     /// The sequence of P4 assertions that have been made to the solver.
     safe_vector<const Constraint *> p4Assertions;

diff --git a/backends/p4tools/common/lib/format_int.cpp b/backends/p4tools/common/lib/format_int.cpp
@@ -13,7 +13,6 @@
 
 #include "lib/cstring.h"
 #include "lib/exceptions.h"
-#include "lib/log.h"
 
 namespace P4Tools {