Skip to content

Commit

Permalink
Replace boost::container::flat_map with absl::btree_map in P4Tools.
Browse files Browse the repository at this point in the history
Signed-off-by: fruffy <[email protected]>
  • Loading branch information
fruffy committed Jul 1, 2024
1 parent b27702f commit 21bf9fa
Show file tree
Hide file tree
Showing 10 changed files with 68 additions and 21 deletions.
1 change: 1 addition & 0 deletions BUILD.bazel
Original file line number Diff line number Diff line change
Expand Up @@ -244,6 +244,7 @@ cc_library(
"@com_github_p4lang_p4runtime//:p4info_cc_proto",
"@com_github_p4lang_p4runtime//:p4runtime_cc_proto",
"@com_github_p4lang_p4runtime//:p4types_cc_proto",
"@com_google_absl//absl/container:btree",
"@com_google_absl//absl/container:flat_hash_map",
"@com_google_absl//absl/container:flat_hash_set",
"@com_google_absl//absl/container:inlined_vector",
Expand Down
2 changes: 1 addition & 1 deletion backends/p4tools/BUILD.bazel
Original file line number Diff line number Diff line change
Expand Up @@ -85,6 +85,7 @@ cc_library(
"@boost//:multiprecision",
"@com_github_p4lang_p4runtime//:p4info_cc_proto",
"@com_github_z3prover_z3//:api",
"@com_google_absl//absl/container:btree",
],
)

Expand Down Expand Up @@ -181,7 +182,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: 3 additions & 4 deletions backends/p4tools/common/lib/model.h
Original file line number Diff line number Diff line change
@@ -1,11 +1,10 @@
#ifndef BACKENDS_P4TOOLS_COMMON_LIB_MODEL_H_
#define BACKENDS_P4TOOLS_COMMON_LIB_MODEL_H_

#include <absl/container/btree_map.h>

#include <map>
#include <utility>
#include <vector>

#include <boost/container/flat_map.hpp>

#include "ir/ir.h"
#include "ir/solver.h"
Expand All @@ -14,7 +13,7 @@
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 = absl::btree_map<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
@@ -1,12 +1,11 @@
#ifndef IR_SOLVER_H_
#define IR_SOLVER_H_

#include <absl/container/btree_map.h>

#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"
Expand All @@ -23,10 +22,8 @@ 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 =
absl::btree_map<const IR::SymbolicVariable *, const IR::Expression *, SymbolicVarComp>;

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

0 comments on commit 21bf9fa

Please sign in to comment.