[P4_Symbolic] Pull common Z3 operations into util library to make them reusable. Change EvaluateSaiPipeline to take a forwarding pipeline config instead of a SAI Instantiation. #774
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Keyword Check:
~/sonic-buildimage/src/sonic-p4rt/sonic-pins$ ~/tools/keyword_checks.sh .
Keyword check Passed.
Build Result:
/sonic/src/sonic-p4rt/sonic-pins$ bazel build $BAZEL_BUILD_OPTS ...
INFO: Analyzed 602 targets (3 packages loaded, 81 targets configured).
INFO: Found 602 targets...
INFO: From Compiling p4_symbolic/symbolic/util.cc [for host]:
p4_symbolic/symbolic/util.cc:35:6: warning: 'bool p4_symbolic::symbolic::util::{anonymous}::Z3BooltoBool(Z3_lbool)' defined but not used [-Wunused-function]
35 | bool Z3BooltoBool(Z3_lbool z3_bool) {
| ^~~~~~~~~~~~
INFO: From Compiling p4_symbolic/symbolic/table.cc [for host]:
p4_symbolic/symbolic/table.cc: In function 'std::vector<std::pair<int, pdpi::IrTableEntry> > p4_symbolic::symbolic::table::{anonymous}::SortEntries(const p4_symbolic::ir::Table&, const std::vectorpdpi::IrTableEntry&)':
p4_symbolic/symbolic/table.cc:115:21: warning: comparison of integer expressions of different signedness: 'int' and 'std::vectorpdpi::IrTableEntry::size_type' {aka 'long unsigned int'} [-Wsign-compare]
115 | for (int i = 0; i < entries.size(); i++) {
| ~~^~~~~~~~~~~~~~~~
INFO: From Compiling p4_symbolic/sai/parser.cc:
p4_symbolic/sai/parser.cc: In function 'absl::lts_20230802::StatusOr<std::vectorz3::expr > p4_symbolic::EvaluateSaiParser(const SymbolicPerPacketState&)':
p4_symbolic/sai/parser.cc:93:51: warning: suggest parentheses around '&&' within '||' [-Wparentheses]
93 | constraints.push_back(icmp.valid == (ipv4.valid && ipv4.protocol == 0x01 ||
| ~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~
p4_symbolic/sai/parser.cc:95:50: warning: suggest parentheses around '&&' within '||' [-Wparentheses]
95 | constraints.push_back(tcp.valid == (ipv4.valid && ipv4.protocol == 0x06 ||
| ~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~
p4_symbolic/sai/parser.cc:97:50: warning: suggest parentheses around '&&' within '||' [-Wparentheses]
97 | constraints.push_back(udp.valid == (ipv4.valid && ipv4.protocol == 0x11 ||
| ~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~
INFO: From Compiling p4_symbolic/symbolic/util.cc:
INFO: From Executing genrule //p4_symbolic/symbolic:condtional_test_test_runner:
Finding packet for table MyIngress.t_1 and row -1
Dropped = 0
standard_metadata.ingress_port = #b000000000
standard_metadata.egress_spec = #b000000001
Finding packet for table MyIngress.t_2 and row -1
Dropped = 0
standard_metadata.ingress_port = #b000000001
standard_metadata.egress_spec = #b000000001
Finding packet for table MyIngress.t_3 and row -1
Cannot find solution!
Finding packet for table MyIngress.t_3 and row 0
Dropped = 0
standard_metadata.ingress_port = #b000000001
standard_metadata.egress_spec = #b000000001
INFO: Elapsed time: 34.847s, Critical Path: 7.62s
INFO: 52 processes: 5 internal, 47 linux-sandbox.
INFO: Build completed successfully, 52 total actions
Test Result:
/sonic/src/sonic-p4rt/sonic-pins$ bazel test $BAZEL_BUILD_OPTS --cache_test_results=no ...
INFO: Analyzed 602 targets (0 packages loaded, 21 targets configured).
INFO: Found 403 targets and 199 test targets...
INFO: Elapsed time: 210.134s, Critical Path: 116.38s
INFO: 253 processes: 299 linux-sandbox, 18 local.
INFO: Build completed successfully, 253 total actions
//dvaas:port_id_map_test PASSED in 0.5s
//dvaas:test_run_validation_test PASSED in 0.6s
//dvaas:test_vector_stats_diff_test PASSED in 0.0s
//dvaas:test_vector_stats_test PASSED in 0.1s
//dvaas:test_vector_test PASSED in 0.6s
//dvaas:user_provided_packet_test_vector_diff_test PASSED in 0.1s
//dvaas:user_provided_packet_test_vector_test PASSED in 0.0s
//gutil:collections_test PASSED in 0.5s
//gutil:io_test PASSED in 0.5s
//p4rt_app/tests:vrf_table_test PASSED in 2.6s
//p4rt_app/tests/lib:app_db_entry_builder_test PASSED in 0.0s
//p4rt_app/utils:event_data_tracker_test PASSED in 0.0s
//p4rt_app/utils:table_utility_test PASSED in 0.7s
//sai_p4/instantiations/google:clos_stage_test PASSED in 0.7s
//sai_p4/instantiations/google:fabric_border_router_p4info_up_to_date_test PASSED in 0.0s
//sai_p4/instantiations/google:middleblock_p4info_up_to_date_test PASSED in 0.0s
//sai_p4/instantiations/google:sai_nonstandard_platforms_build_test PASSED in 0.1s
//sai_p4/instantiations/google:sai_nonstandard_platforms_cc_test PASSED in 0.7s
//sai_p4/instantiations/google:sai_p4info_fetcher_test PASSED in 0.7s
//sai_p4/instantiations/google:sai_p4info_test PASSED in 1.1s
//sai_p4/instantiations/google:sai_pd_proto_test PASSED in 0.1s
//sai_p4/instantiations/google:sai_pd_util_test PASSED in 0.5s
//sai_p4/instantiations/google:tor_p4info_up_to_date_test PASSED in 0.0s
//sai_p4/instantiations/google:union_p4info_up_to_date_test PASSED in 0.1s
//sai_p4/instantiations/google:wbb_p4info_up_to_date_test PASSED in 0.0s
//sai_p4/instantiations/google/test_tools:table_entry_generator_helper_test PASSED in 1.5s
//sai_p4/instantiations/google/test_tools:test_entries_test PASSED in 0.9s
//sai_p4/instantiations/google/tests:p4_fuzzer_integration_test PASSED in 3.5s
//sai_p4/tools:p4info_tools_test PASSED in 0.7s
//sai_p4/tools:packetio_tools_test PASSED in 0.8s
//tests:thinkit_gnmi_interface_util_tests PASSED in 1.1s
//tests/qos:gnmi_parsers_test PASSED in 0.0s
//tests/qos:gnmi_parsers_test_runner PASSED in 0.0s
//thinkit:bazel_test_environment_test PASSED in 0.5s
//thinkit:generic_testbed_test PASSED in 1.5s
//thinkit:mock_control_device_test PASSED in 2.0s
//thinkit:mock_generic_testbed_test PASSED in 0.7s
//thinkit:mock_mirror_testbed_test PASSED in 0.6s
//thinkit:mock_ssh_client_test PASSED in 0.0s
//thinkit:mock_switch_test PASSED in 0.7s
//thinkit:mock_test_environment_test PASSED in 0.1s
//thinkit:switch_test PASSED in 0.8s
//sai_p4/instantiations/google/tests:p4_constraints_integration_test PASSED in 0.8s
Stats over 5 runs: max = 0.8s, min = 0.7s, avg = 0.7s, dev = 0.1s
//sai_p4/instantiations/google/test_tools:table_entry_generator_test PASSED in 44.2s
Stats over 50 runs: max = 44.2s, min = 0.8s, avg = 2.1s, dev = 6.1s
Executed 199 out of 199 tests: 199 tests pass.
INFO: Build completed successfully, 253 total actions