Skip to content

Commit

Permalink
Replace boost::container::flat_map with a custom flat_map implementat…
Browse files Browse the repository at this point in the history
…ion in P4Tools.
  • Loading branch information
fruffy committed Jun 6, 2024
1 parent d5df09b commit 86430b2
Show file tree
Hide file tree
Showing 10 changed files with 381 additions and 20 deletions.
1 change: 0 additions & 1 deletion backends/p4tools/BUILD.bazel
Original file line number Diff line number Diff line change
Expand Up @@ -181,7 +181,6 @@ cc_binary(
deps = [
":testgen_lib",
"//:lib",
"@boost//:filesystem",
"@boost//:multiprecision",
],
)
Expand Down
2 changes: 0 additions & 2 deletions backends/p4tools/common/lib/model.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,6 @@
#include <string>
#include <utility>

#include <boost/container/vector.hpp>

#include "frontends/p4/optimizeExpressions.h"
#include "ir/indexed_vector.h"
#include "ir/irutils.h"
Expand Down
7 changes: 4 additions & 3 deletions backends/p4tools/common/lib/model.h
Original file line number Diff line number Diff line change
Expand Up @@ -5,16 +5,17 @@
#include <utility>
#include <vector>

#include <boost/container/flat_map.hpp>

#include "ir/ir.h"
#include "ir/solver.h"
#include "ir/visitor.h"
#include "lib/map.h"

namespace P4Tools {

/// Symbolic maps map a state variable to a IR::Expression.
using SymbolicMapType = boost::container::flat_map<IR::StateVariable, const IR::Expression *>;
using SymbolicMapType =
P4C::flat_map<IR::StateVariable, const IR::Expression *, std::less<IR::StateVariable>,
std::vector<std::pair<IR::StateVariable, const IR::Expression *>>>;

/// Represents a solution found by the solver. A model is a concretized form of a symbolic
/// environment. All the expressions in a Model must be of type IR::Literal.
Expand Down
2 changes: 0 additions & 2 deletions backends/p4tools/common/lib/symbolic_env.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,6 @@
#include <algorithm>
#include <utility>

#include <boost/container/vector.hpp>

#include "backends/p4tools/common/lib/model.h"
#include "ir/indexed_vector.h"
#include "ir/vector.h"
Expand Down
1 change: 0 additions & 1 deletion backends/p4tools/common/options.h
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
#ifndef BACKENDS_P4TOOLS_COMMON_OPTIONS_H_
#define BACKENDS_P4TOOLS_COMMON_OPTIONS_H_

// Boost
#include <cstdint>
#include <optional>
#include <tuple>
Expand Down
1 change: 0 additions & 1 deletion backends/p4tools/modules/testgen/lib/execution_state.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,6 @@
#include <variant>
#include <vector>

#include <boost/container/vector.hpp>
#include <boost/multiprecision/cpp_int.hpp>

#include "backends/p4tools/common/compiler/convert_hs_index.h"
Expand Down
2 changes: 0 additions & 2 deletions backends/p4tools/modules/testgen/lib/final_state.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,6 @@
#include <variant>
#include <vector>

#include <boost/container/vector.hpp>

#include "backends/p4tools/common/lib/model.h"
#include "backends/p4tools/common/lib/symbolic_env.h"
#include "backends/p4tools/common/lib/trace_event.h"
Expand Down
60 changes: 59 additions & 1 deletion backends/p4tools/p4tools.def
Original file line number Diff line number Diff line change
Expand Up @@ -23,12 +23,21 @@ class StateVariable : Expression {
StateVariable(ArrayIndex arr) : Expression(arr->getSourceInfo(), arr->type), ref(arr) {}

/// Implements comparisons so that StateVariables can be used as map keys.
// Delegate to IR's notion of equality.
bool operator==(const StateVariable &other) const override {
// Delegate to IR's notion of equality.
return *ref == *other.ref;
}

/// Implements comparisons so that StateVariables can be used as map keys.
/// Note that we ignore the type of the variable in the comparison.
equiv {
// We use a custom compare function.
// TODO: Is there a faster way to implement this comparison?
return compare(ref, a.ref) == 0;
}

/// Implements comparisons so that StateVariables can be used as map keys.
/// Note that we ignore the type of the variable in the comparison.
bool operator<(const StateVariable &other) const {
// We use a custom compare function.
// TODO: Is there a faster way to implement this comparison?
Expand Down Expand Up @@ -122,6 +131,30 @@ class StateVariable : Expression {
dbprint { ref->dbprint(out); }
}

#emit
namespace IR {
/// Equals for StateVariable pointers. We only compare the label.
struct StateVariableEqual {
bool operator()(const IR::StateVariable *s1, const IR::StateVariable *s2) const {
return s1->equiv(*s2);
}
bool operator()(const IR::StateVariable &s1, const IR::StateVariable &s2) const {
return s1.equiv(s2);
}
};

/// Less for StateVariable pointers. We only compare the label.
struct StateVariableLess {
bool operator()(const IR::StateVariable *s1, const IR::StateVariable *s2) const {
return s1->operator<(*s2);
}
bool operator()(const IR::StateVariable &s1, const IR::StateVariable &s2) const {
return s1.operator<(s2);
}
};
} // namespace IR
#end

/// Signifies that a particular expression is tainted.
/// This tainted expression must be resolved explicitly.
class TaintExpression : Expression {
Expand Down Expand Up @@ -151,6 +184,31 @@ class SymbolicVariable : Expression {
dbprint { out << "|" + label +"(" << type << ")|"; }
}

#emit
namespace IR {
/// Equals for SymbolicVariable pointers. We only compare the label.
struct SymbolicVariableEqual {
bool operator()(const IR::SymbolicVariable *s1, const IR::SymbolicVariable *s2) const {
return s1->label == s2->label;
}
bool operator()(const IR::SymbolicVariable &s1, const IR::SymbolicVariable &s2) const {
return s1.label == s2.label;
}
};

/// Less for SymbolicVariable pointers. We only compare the label.
struct SymbolicVariableLess {
bool operator()(const IR::SymbolicVariable *s1, const IR::SymbolicVariable *s2) const {
return s1->operator<(*s2);
}
bool operator()(const IR::SymbolicVariable &s1, const IR::SymbolicVariable &s2) const {
return s1.operator<(s2);
}
};
} // namespace IR
#end


/// This type replaces Type_Varbits and can store information about the current size
class Extracted_Varbits : Type_Bits {
public:
Expand Down
11 changes: 4 additions & 7 deletions ir/solver.h
Original file line number Diff line number Diff line change
Expand Up @@ -4,12 +4,10 @@
#include <optional>
#include <vector>

#include <boost/container/flat_map.hpp>
#include <boost/container/flat_set.hpp>

#include "ir/ir.h"
#include "lib/castable.h"
#include "lib/cstring.h"
#include "lib/flat_map.h"

/// Represents a constraint that can be shipped to and asserted within a solver.
// TODO: This should implement AbstractRepCheckedNode<Constraint>.
Expand All @@ -23,10 +21,9 @@ struct SymbolicVarComp {
};

/// 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>;
using SymbolicMapping =
P4C::flat_map<const IR::SymbolicVariable *, const IR::Expression *, IR::SymbolicVariableLess,
std::vector<std::pair<const IR::SymbolicVariable *, const IR::Expression *>>>;

/// Provides a higher-level interface for an SMT solver.
class AbstractSolver : public ICastable {
Expand Down
Loading

0 comments on commit 86430b2

Please sign in to comment.