Skip to content

Commit

Permalink
Merge branch 'main' into symbolic_import_branch_131
Browse files Browse the repository at this point in the history
  • Loading branch information
@kishanps
kishanps authored Dec 11, 2024
2 parents 7734c49 + f89f776 commit 265568b
Show file tree
Hide file tree
Showing 22 changed files with 2,631 additions and 2,276 deletions.
1 change: 1 addition & 0 deletions p4_symbolic/symbolic/BUILD.bazel
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,7 @@ cc_library(
"values.h",
],
deps = [
"//gutil:collections",
"//gutil:status",
"//p4_pdpi:ir_cc_proto",
"//p4_pdpi/internal:ordered_map",
Expand Down
35 changes: 20 additions & 15 deletions p4_symbolic/symbolic/action.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,9 @@
#include "absl/status/status.h"
#include "absl/strings/str_cat.h"
#include "absl/strings/str_format.h"
#include "absl/strings/string_view.h"
#include "glog/logging.h"
#include "gutil/collections.h"
#include "p4_symbolic/symbolic/operators.h"
#include "p4_symbolic/symbolic/symbolic.h"
#include "p4_symbolic/z3_util.h"
Expand Down Expand Up @@ -320,27 +322,30 @@ absl::Status EvaluateAction(const ir::Action &action,
VLOG(1) << "evaluating action '" << context.action_name << "'";

// Add action parameters to scope.
const auto &parameters = action.action_definition().params_by_id();
const auto &parameters = action.action_definition().params_by_name();
if (static_cast<int>(parameters.size()) != args.size()) {
return absl::InvalidArgumentError(
absl::StrCat("Action ", action.action_definition().preamble().name(),
" called with incompatible number of parameters"));
}

// Find each parameter value in argument by parameter's name.
for (size_t i = 1; i <= parameters.size(); i++) {
// parameter id is the same as its index + 1.
const pdpi::IrActionDefinition::IrActionParamDefinition &parameter =
parameters.at(i);
const std::string &parameter_name = parameter.param().name();
const std::string &parameter_type_name =
parameter.param().type_name().name();
const int bitwidth = parameter.param().bitwidth();
ASSIGN_OR_RETURN(z3::expr parameter_value,
values::FormatP4RTValue(
Z3Context(), /*field_name=*/"", parameter_type_name,
args.at(i - 1).value(), bitwidth, translator));
context.scope.insert({parameter_name, parameter_value});
// Find each parameter value in arguments by argument name. We should not rely
// on argument order matching param definition order, because the P4 runtime
// spec does not enforce this assumption in implementations, and furthermore
// the spec explicitly states that read entries do not have to preserve the
// order of repeated fields in written entries.
for (const auto &arg : args) {
absl::string_view arg_name = arg.name();
ASSIGN_OR_RETURN(const pdpi::IrActionDefinition::IrActionParamDefinition
*param_definition,
gutil::FindPtrOrStatus(parameters, arg_name));
ASSIGN_OR_RETURN(
z3::expr parameter_value,
values::FormatP4RTValue(
Z3Context(), /*field_name=*/"",
param_definition->param().type_name().name(), arg.value(),
param_definition->param().bitwidth(), translator));
context.scope.insert({param_definition->param().name(), parameter_value});
}

// Iterate over the body in order, and evaluate each statement.
Expand Down
412 changes: 206 additions & 206 deletions p4_symbolic/symbolic/expected/basic.smt2
View file

Large diffs are not rendered by default.

186 changes: 93 additions & 93 deletions p4_symbolic/symbolic/expected/conditional.smt2
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,31 +4,31 @@
(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
(declare-fun ethernet.dst_addr () (_ BitVec 48))
(assert
(let (($x61 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x61)))
(let (($x64 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x64)))
(assert
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let (($x34 (and true (not $x31))))
(let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x42 (= ethernet.dst_addr (_ bv1 48))))
(let (($x43 (and true $x42)))
(let (($x44 (and true $x43)))
(let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
(let (($x54 (= ?x52 (_ bv511 9))))
(or $x54 (or (or false (= ?x52 (_ bv0 9))) (= ?x52 (_ bv1 9))))))))))))))
(let (($x34 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x36 (and true $x34)))
(let (($x37 (and true (not $x34))))
(let ((?x50 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x37 (_ bv511 9) (ite $x36 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x45 (= ethernet.dst_addr (_ bv1 48))))
(let (($x46 (and true $x45)))
(let (($x47 (and true $x46)))
(let ((?x55 (ite $x47 (_ bv1 9) ?x50)))
(let (($x57 (= ?x55 (_ bv511 9))))
(or $x57 (or (or false (= ?x55 (_ bv0 9))) (= ?x55 (_ bv1 9))))))))))))))
(assert
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let (($x39 (ite $x31 $x33 false)))
(let (($x34 (and true (not $x31))))
(let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x42 (= ethernet.dst_addr (_ bv1 48))))
(let (($x43 (and true $x42)))
(let (($x44 (and true $x43)))
(let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
(let (($x54 (= ?x52 (_ bv511 9))))
(and (and (not $x54) $x39) (= (- 1) (- 1))))))))))))))
(let (($x34 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x36 (and true $x34)))
(let (($x42 (ite $x34 $x36 false)))
(let (($x37 (and true (not $x34))))
(let ((?x50 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x37 (_ bv511 9) (ite $x36 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x45 (= ethernet.dst_addr (_ bv1 48))))
(let (($x46 (and true $x45)))
(let (($x47 (and true $x46)))
(let ((?x55 (ite $x47 (_ bv1 9) ?x50)))
(let (($x57 (= ?x55 (_ bv511 9))))
(and (and (not $x57) $x42) (= (- 1) (- 1))))))))))))))
(check-sat)

;
Expand All @@ -37,31 +37,31 @@
(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
(declare-fun ethernet.dst_addr () (_ BitVec 48))
(assert
(let (($x61 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x61)))
(let (($x64 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x64)))
(assert
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let (($x34 (and true (not $x31))))
(let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x42 (= ethernet.dst_addr (_ bv1 48))))
(let (($x43 (and true $x42)))
(let (($x44 (and true $x43)))
(let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
(let (($x54 (= ?x52 (_ bv511 9))))
(or $x54 (or (or false (= ?x52 (_ bv0 9))) (= ?x52 (_ bv1 9))))))))))))))
(let (($x34 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x36 (and true $x34)))
(let (($x37 (and true (not $x34))))
(let ((?x50 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x37 (_ bv511 9) (ite $x36 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x45 (= ethernet.dst_addr (_ bv1 48))))
(let (($x46 (and true $x45)))
(let (($x47 (and true $x46)))
(let ((?x55 (ite $x47 (_ bv1 9) ?x50)))
(let (($x57 (= ?x55 (_ bv511 9))))
(or $x57 (or (or false (= ?x55 (_ bv0 9))) (= ?x55 (_ bv1 9))))))))))))))
(assert
(let (($x34 (and true (not (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))))
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x40 (ite $x31 false $x34)))
(let ((?x38 (ite $x34 (_ bv511 9) (ite (and true $x31) (_ bv511 9) standard_metadata.egress_spec))))
(let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) ?x38)))
(let (($x42 (= ethernet.dst_addr (_ bv1 48))))
(let (($x43 (and true $x42)))
(let (($x44 (and true $x43)))
(let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
(let (($x54 (= ?x52 (_ bv511 9))))
(and (and (not $x54) $x40) (= (- 1) (- 1))))))))))))))
(let (($x37 (and true (not (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))))
(let (($x34 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x43 (ite $x34 false $x37)))
(let ((?x41 (ite $x37 (_ bv511 9) (ite (and true $x34) (_ bv511 9) standard_metadata.egress_spec))))
(let ((?x50 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) ?x41)))
(let (($x45 (= ethernet.dst_addr (_ bv1 48))))
(let (($x46 (and true $x45)))
(let (($x47 (and true $x46)))
(let ((?x55 (ite $x47 (_ bv1 9) ?x50)))
(let (($x57 (= ?x55 (_ bv511 9))))
(and (and (not $x57) $x43) (= (- 1) (- 1))))))))))))))
(check-sat)

;
Expand All @@ -70,31 +70,31 @@
(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
(declare-fun ethernet.dst_addr () (_ BitVec 48))
(assert
(let (($x61 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x61)))
(let (($x64 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x64)))
(assert
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let (($x34 (and true (not $x31))))
(let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x42 (= ethernet.dst_addr (_ bv1 48))))
(let (($x43 (and true $x42)))
(let (($x44 (and true $x43)))
(let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
(let (($x54 (= ?x52 (_ bv511 9))))
(or $x54 (or (or false (= ?x52 (_ bv0 9))) (= ?x52 (_ bv1 9))))))))))))))
(let (($x34 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x36 (and true $x34)))
(let (($x37 (and true (not $x34))))
(let ((?x50 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x37 (_ bv511 9) (ite $x36 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x45 (= ethernet.dst_addr (_ bv1 48))))
(let (($x46 (and true $x45)))
(let (($x47 (and true $x46)))
(let ((?x55 (ite $x47 (_ bv1 9) ?x50)))
(let (($x57 (= ?x55 (_ bv511 9))))
(or $x57 (or (or false (= ?x55 (_ bv0 9))) (= ?x55 (_ bv1 9))))))))))))))
(assert
(let (($x42 (= ethernet.dst_addr (_ bv1 48))))
(let (($x43 (and true $x42)))
(let (($x44 (and true $x43)))
(let ((?x49 (ite $x44 0 (- 1))))
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let (($x34 (and true (not $x31))))
(let ((?x47 (ite (and true (not $x43)) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
(let (($x54 (= ?x52 (_ bv511 9))))
(and (and (not $x54) true) (= ?x49 (- 1))))))))))))))
(let (($x45 (= ethernet.dst_addr (_ bv1 48))))
(let (($x46 (and true $x45)))
(let (($x47 (and true $x46)))
(let ((?x52 (ite $x47 0 (- 1))))
(let (($x34 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x36 (and true $x34)))
(let (($x37 (and true (not $x34))))
(let ((?x50 (ite (and true (not $x46)) (_ bv511 9) (ite $x37 (_ bv511 9) (ite $x36 (_ bv511 9) standard_metadata.egress_spec)))))
(let ((?x55 (ite $x47 (_ bv1 9) ?x50)))
(let (($x57 (= ?x55 (_ bv511 9))))
(and (and (not $x57) true) (= ?x52 (- 1))))))))))))))
(check-sat)

;
Expand All @@ -103,31 +103,31 @@
(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
(declare-fun ethernet.dst_addr () (_ BitVec 48))
(assert
(let (($x61 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x61)))
(let (($x64 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x64)))
(assert
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let (($x34 (and true (not $x31))))
(let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x42 (= ethernet.dst_addr (_ bv1 48))))
(let (($x43 (and true $x42)))
(let (($x44 (and true $x43)))
(let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
(let (($x54 (= ?x52 (_ bv511 9))))
(or $x54 (or (or false (= ?x52 (_ bv0 9))) (= ?x52 (_ bv1 9))))))))))))))
(let (($x34 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x36 (and true $x34)))
(let (($x37 (and true (not $x34))))
(let ((?x50 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x37 (_ bv511 9) (ite $x36 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x45 (= ethernet.dst_addr (_ bv1 48))))
(let (($x46 (and true $x45)))
(let (($x47 (and true $x46)))
(let ((?x55 (ite $x47 (_ bv1 9) ?x50)))
(let (($x57 (= ?x55 (_ bv511 9))))
(or $x57 (or (or false (= ?x55 (_ bv0 9))) (= ?x55 (_ bv1 9))))))))))))))
(assert
(let (($x42 (= ethernet.dst_addr (_ bv1 48))))
(let (($x43 (and true $x42)))
(let (($x44 (and true $x43)))
(let ((?x49 (ite $x44 0 (- 1))))
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let (($x34 (and true (not $x31))))
(let ((?x47 (ite (and true (not $x43)) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
(let (($x54 (= ?x52 (_ bv511 9))))
(let (($x97 (and (not $x54) true)))
(and $x97 (= ?x49 0))))))))))))))
(let (($x45 (= ethernet.dst_addr (_ bv1 48))))
(let (($x46 (and true $x45)))
(let (($x47 (and true $x46)))
(let ((?x52 (ite $x47 0 (- 1))))
(let (($x34 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x36 (and true $x34)))
(let (($x37 (and true (not $x34))))
(let ((?x50 (ite (and true (not $x46)) (_ bv511 9) (ite $x37 (_ bv511 9) (ite $x36 (_ bv511 9) standard_metadata.egress_spec)))))
(let ((?x55 (ite $x47 (_ bv1 9) ?x50)))
(let (($x57 (= ?x55 (_ bv511 9))))
(let (($x100 (and (not $x57) true)))
(and $x100 (= ?x52 0))))))))))))))
(check-sat)

Loading

0 comments on commit 265568b

Please sign in to comment.