Skip to content

Commit

Permalink
PR feedback
Browse files Browse the repository at this point in the history
Signed-off-by: Alan Jowett <[email protected]>
  • Loading branch information
Alan Jowett committed Oct 25, 2024
1 parent 2b0ed35 commit 499572d
Show file tree
Hide file tree
Showing 3 changed files with 23 additions and 12 deletions.
27 changes: 16 additions & 11 deletions src/test/ebpf_yaml.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -131,12 +131,14 @@ static std::map<std::string, std::set<std::string>> parse_invariants_to_check(co
if (!case_node["invariants-to-check"].IsDefined() || case_node["invariants-to-check"].IsNull()) {
return {};
}

std::map<std::string, std::set<std::string>> res;
for (const auto& node : case_node["invariants-to-check"]) {
res.emplace(node.first.as<string>(), vector_to_set(node.second.as<vector<string>>()));
try {
for (const auto& node : case_node["invariants-to-check"]) {
res.emplace(node.first.as<string>(), vector_to_set(node.second.as<vector<string>>()));
}
} catch (const YAML::Exception& e) {
throw std::runtime_error("Error parsing 'invariants-to-check': " + std::string(e.what()));
}

return res;
}

Expand Down Expand Up @@ -278,14 +280,17 @@ std::optional<Failure> run_yaml_test_case(TestCase test_case, bool debug) {
std::set<string> actual_messages = extract_messages(ss.str());

for (auto& [label, expected_invariant] : test_case.invariants_to_check) {
ss.str("");
ss.clear();
if (!ebpf_check_constraints_at_label(ss, label, expected_invariant)) {
// If debug is enabled, print the output of ebpf_check_constraints_at_label.
if (debug) {
std::cout << ss.str();
ss = {};
try {
if (!ebpf_check_constraints_at_label(ss, label, expected_invariant)) {
// If debug is enabled, print the output of ebpf_check_constraints_at_label.
if (debug) {
std::cout << ss.str();
}
actual_messages.insert(label + ": Concrete invariants do not match abstract invariants");
}
actual_messages.insert(label + ": Concrete invariants do not match abstract invariants");
} catch (const std::exception& e) {
actual_messages.insert(label + ": Exception occurred during invariant check - " + std::string(e.what()));
}
}

Expand Down
2 changes: 1 addition & 1 deletion src/test/ebpf_yaml.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ struct TestCase {
InstructionSeq instruction_seq;
string_invariant expected_post_invariant;
std::set<std::string> expected_messages;
std::map<std::string, std::set<std::string>> invariants_to_check; ///< Map from label to expected invariants, used for checking invariants at specific labels.
std::map<std::string, std::set<std::string>> invariants_to_check; ///< Map from label to expected invariants, used for validating program state at specific labels during test execution.
};

void foreach_suite(const std::string& path, const std::function<void(const TestCase&)>& f);
Expand Down
6 changes: 6 additions & 0 deletions test-data/add.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -193,14 +193,17 @@ invariants-to-check:
- r1.type=number
- r1.svalue=1
- r1.uvalue=1

2: # After the second assignment, r2 should be 2.

Check warning on line 197 in test-data/add.yaml

View workflow job for this annotation

GitHub Actions / validate-yaml

197:6 [comments] too few spaces before comment

Check warning on line 197 in test-data/add.yaml

View workflow job for this annotation

GitHub Actions / validate-yaml

197:6 [comments] too few spaces before comment
- r2.type=number
- r2.svalue=2
- r2.uvalue=2

3: # After the addition, r1 should be 3.

Check warning on line 202 in test-data/add.yaml

View workflow job for this annotation

GitHub Actions / validate-yaml

202:6 [comments] too few spaces before comment
- r1.type=number
- r1.svalue=3
- r1.uvalue=3

-2: # After the last assignment, r0 should be 3.

Check warning on line 207 in test-data/add.yaml

View workflow job for this annotation

GitHub Actions / validate-yaml

207:7 [comments] too few spaces before comment
- r0.type=number
- r0.svalue=3
Expand Down Expand Up @@ -233,14 +236,17 @@ invariants-to-check:
- r1.type=number
- r1.svalue=1
- r1.uvalue=1

2: # After the second assignment, r2 should be 2.

Check warning on line 240 in test-data/add.yaml

View workflow job for this annotation

GitHub Actions / validate-yaml

240:6 [comments] too few spaces before comment
- r2.type=number
- r2.svalue=2
- r2.uvalue=2

3: # After the addition, r1 should be 3. Invalid invariant to test negative case.

Check warning on line 245 in test-data/add.yaml

View workflow job for this annotation

GitHub Actions / validate-yaml

245:6 [comments] too few spaces before comment
- r1.type=number
- r1.svalue=2
- r1.uvalue=2

-2: # After the last assignment, r0 should be 3.

Check warning on line 250 in test-data/add.yaml

View workflow job for this annotation

GitHub Actions / validate-yaml

250:7 [comments] too few spaces before comment
- r0.type=number
- r0.svalue=3
Expand Down

0 comments on commit 499572d

Please sign in to comment.