Add Program class, containing a cfg_t class

[elazarg]

Extract code from cfg_t class so it only deals with control flow structure.
The new class Program holds cfg_t and mapping labels to instructions and from labels to assertions (a cache, essentially).

The class GuardedInstruction is removed, as it only clutters the code.

Summary by CodeRabbit

• New Features

  • Introduced a Program class for encapsulating control flow graphs and associated instructions.
  • Added methods for managing assertions and retrieving instructions within the Program class.
  • Enhanced ebpf_checker with new methods for validating eBPF assertions.

• Bug Fixes

  • Improved error handling in various functions related to instruction processing and verification.

• Documentation

  • Updated documentation to reflect changes in function signatures and class structures.

• Refactor

  • Transitioned from using cfg_t to Program across multiple components, streamlining the handling of instruction sequences.

• Tests

  • Updated test cases to utilize the new Program class, ensuring consistency and correctness in verification processes.

[coderabbitai]

Actionable comments posted: 11

🔭 Outside diff range comments (2)

src/asm_ostream.cpp (1)

Line range hint 417-417: Resolved syntax error highlighted by static analysis

The syntax error reported by cppcheck at line 134 has been addressed, preventing potential compilation issues.

🧰 Tools

🪛 cppcheck (2.10-2)

[error] 134-134: Syntax Error

(internalAstError)

src/crab_verifier.cpp (1)

Line range hint 91-96: Consider extracting reachability check to a separate method

The reachability check logic could be moved to a dedicated method in Program class.

+bool Program::is_reachable(const label_t& label) const {
+    if (const auto passume = std::get_if<Assume>(&instruction_at(label))) {
+        return !inv_pair.post.is_bottom();
+    }
+    return true;
+}

📜 Review details

Configuration used: CodeRabbit UI
Review profile: ASSERTIVE
Plan: Pro

📥 Commits

Reviewing files that changed from the base of the PR and between 3f78808 and 72a1c28.

📒 Files selected for processing (22)

• src/asm_cfg.cpp (14 hunks)
• src/asm_ostream.cpp (2 hunks)
• src/asm_syntax.hpp (0 hunks)
• src/crab/array_domain.cpp (0 hunks)
• src/crab/array_domain.hpp (0 hunks)
• src/crab/cfg.hpp (1 hunks)
• src/crab/ebpf_checker.cpp (1 hunks)
• src/crab/fwd_analyzer.cpp (5 hunks)
• src/crab/fwd_analyzer.hpp (2 hunks)
• src/crab/type_domain.hpp (1 hunks)
• src/crab/wto.cpp (2 hunks)
• src/crab/wto.hpp (3 hunks)
• src/crab_utils/graph_ops.hpp (5 hunks)
• src/crab_verifier.cpp (2 hunks)
• src/crab_verifier.hpp (2 hunks)
• src/ebpf_verifier.hpp (1 hunks)
• src/main/check.cpp (2 hunks)
• src/program.hpp (1 hunks)
• src/test/ebpf_yaml.cpp (3 hunks)
• src/test/test_marshal.cpp (3 hunks)
• src/test/test_verify.cpp (3 hunks)
• src/test/test_wto.cpp (3 hunks)

💤 Files with no reviewable changes (3)

• src/asm_syntax.hpp
• src/crab/array_domain.hpp
• src/crab/array_domain.cpp

🧰 Additional context used

📓 Learnings (2)

src/crab/fwd_analyzer.hpp (2)

Learnt from: elazarg
PR: vbpf/ebpf-verifier#692
File: src/crab/ebpf_domain.cpp:1366-1367
Timestamp: 2024-11-12T09:50:23.369Z
Learning: The project is compiled with C++20.

Learnt from: elazarg
PR: vbpf/ebpf-verifier#692
File: src/crab/ebpf_domain.cpp:641-642
Timestamp: 2024-11-12T09:50:16.890Z
Learning: The project uses the C++20 standard and supports C++20 features.

src/crab_verifier.cpp (2)

Learnt from: elazarg
PR: vbpf/ebpf-verifier#692
File: src/crab/ebpf_domain.cpp:1366-1367
Timestamp: 2024-11-12T09:50:23.369Z
Learning: The project is compiled with C++20.

Learnt from: elazarg
PR: vbpf/ebpf-verifier#692
File: src/crab/ebpf_domain.cpp:641-642
Timestamp: 2024-11-12T09:50:16.890Z
Learning: The project uses the C++20 standard and supports C++20 features.

🪛 cppcheck (2.10-2)

src/crab/fwd_analyzer.cpp

[style] 75-75: The function 'run_forward_analyzer' is never used.

(unusedFunction)

src/asm_ostream.cpp

[error] 134-134: Syntax Error

(internalAstError)

🔇 Additional comments (30)

src/crab/type_domain.hpp (1)

15-16: Include asm_syntax.hpp for Reg definition

Including "asm_syntax.hpp" is necessary for the Reg type used in the reg_pack functions.

src/crab/fwd_analyzer.cpp (1)

75-75: Verify usage of run_forward_analyzer function

The run_forward_analyzer function has been updated to accept a Program object, but static analysis indicates it's unused. Verify that this function is called elsewhere in the codebase to avoid potential issues.

Run the following script to search for usages of run_forward_analyzer:

✅ Verification successful

Function run_forward_analyzer is actively used in the codebase

The function is called in src/crab_verifier.cpp to generate invariants and is properly declared in the header file. This is a valid and active usage.

🏁 Scripts executed

The following scripts were executed for the analysis:

Script:

#!/bin/bash
# Description: Search for usages of 'run_forward_analyzer' in the codebase.

rg 'run_forward_analyzer\('

Length of output: 478

🧰 Tools

🪛 cppcheck (2.10-2)

[style] 75-75: The function 'run_forward_analyzer' is never used.

(unusedFunction)

src/main/check.cpp (1)

242-244: Update to use Program::from_sequence

Replacing prepare_cfg with Program::from_sequence aligns with the new Program class and maintains consistency across the codebase.

src/test/ebpf_yaml.cpp (5)

248-251: Refactored to use Program class correctly

The transition from cfg_t to Program is properly implemented here. The creation of the Program instance and subsequent calls to analyze and check_assertions align with the new structure.

---

261-261: Updated exception handling to use InvalidControlFlow

Catching InvalidControlFlow& ex ensures that exceptions related to control flow are properly handled under the new Program class.

---

356-356: Safe extraction of InstructionSeq from variant

After confirming that prog_or_error is not a string, it's safe to extract InstructionSeq using std::get<InstructionSeq>. This correctly handles the variant contents.

---

360-360: Conditional debug output is appropriate

Printing inst_seq to std::cout is guarded by the debug flag, preventing unnecessary output during normal execution.

---

368-370: Consistent use of Program class in analysis

The creation of the Program instance and performing analysis with analyze and invariants.verified correctly utilize the new Program structure.

src/crab/ebpf_checker.cpp (2)

18-18: Included missing header file

The inclusion of program.hpp ensures that the Program class definitions are available, resolving any potential compilation issues.

---

Line range hint 71-73: Consistent use of ebpf_checker class

The ebpf_checker class properly encapsulates the assertion checking logic. The new methods added align with the types of assertions being handled.

src/asm_ostream.cpp (3)

98-121: Renamed functions to reflect Program usage

Functions such as print_cfg have been appropriately renamed to print_program, and their parameters updated to accept a Program object. This aligns with the shift from cfg_t to Program and maintains consistency across the codebase.

---

124-149: Updated DOT graph printing functions

The print_dot functions now operate on a Program object instead of cfg_t, ensuring that the graphical representation of the program's control flow reflects the new structure.

🧰 Tools

🪛 cppcheck (2.10-2)

[error] 134-134: Syntax Error

(internalAstError)

---

177-179: Adjusted invariant printing to use Program

The print_invariants function now takes a Program object, which is consistent with the refactoring efforts and ensures accurate output of program invariants.

src/test/test_verify.cpp (3)

42-45: No issues with the update to Program usage in FAIL_ANALYZE macro.

---

51-64: Use of Program in VERIFY_PROGRAM macro aligns with updated design.

---

631-632: Thread creation with updated Program instances is correct.

src/crab_utils/graph_ops.hpp (2)

505-505: Addition of edge_marks as thread-local storage is appropriate.

---

539-539: Clearing edge_marks in clear_thread_local_state() ensures proper reset.

src/ebpf_verifier.hpp (1)

10-10: Inclusion of program.hpp replaces the outdated cfg.hpp.

src/crab/fwd_analyzer.hpp (1)

8-8: Update function signature to accept Program and include program.hpp.

This change reflects the transition from cfg_t to Program throughout the codebase.

Also applies to: 18-18

src/test/test_wto.cpp (1)

14-14: Verify namespace changes don't break other test files

The removal of crab:: prefix from cfg_from_adjacency_list calls is consistent with the using declaration on line 9, but could impact other test files.

Also applies to: 32-32, 47-47

✅ Verification successful

Namespace changes are safe to proceed

The function cfg_from_adjacency_list is only used in test_wto.cpp and not in any other test files. The removal of crab:: prefix is localized to this test file and won't impact other tests.

🏁 Scripts executed

The following scripts were executed for the analysis:

Script:

#!/bin/bash
# Check if cfg_from_adjacency_list is used with crab:: prefix in other files
rg "crab::cfg_from_adjacency_list" src/test/

Length of output: 359

---

Script:

#!/bin/bash
# Check if cfg_from_adjacency_list is used in other test files without namespace
rg "cfg_from_adjacency_list" src/test/ -g "!test_wto.cpp"

# Check for using declarations of cfg_from_adjacency_list in test files
rg "using.*cfg_from_adjacency_list" src/test/

Length of output: 105

src/crab_verifier.hpp (1)

7-7: Verify all required headers are included

The replacement of crab/cfg.hpp with program.hpp might miss some required types.

✅ Verification successful

The previous results show that Program uses cfg_t, but let's verify the complete class definition and usage to ensure all dependencies are properly included.

---

Let's verify the content of program.hpp to ensure it includes the necessary crab headers for cfg_t, and check if crab/cfg.hpp is still used elsewhere in the codebase.

---

Include change is properly handled

The program.hpp includes crab/cfg.hpp and provides all necessary types. The Program class directly uses cfg_t and the header dependency is correctly maintained.

🏁 Scripts executed

The following scripts were executed for the analysis:

Script:

#!/bin/bash
# Check if Program class uses any types from cfg.hpp
rg -l "class\s+Program" | xargs rg "cfg_t|crab::"

Length of output: 127

---

Script:

#!/bin/bash
# Find the Program class definition to check its dependencies
ast-grep --pattern 'class Program {
  $$$
}'

# Check what other files include program.hpp
rg -l '#include.*program\.hpp'

Length of output: 217

---

Script:

#!/bin/bash
# Check program.hpp content to verify it includes necessary headers
cat src/program.hpp

# Check if crab/cfg.hpp is still included anywhere else
rg -l '#include.*crab/cfg\.hpp'

Length of output: 2767

src/crab_verifier.cpp (1)

Line range hint 70-74: Verify error handling in assertions_at

Need to ensure assertions_at handles empty collections gracefully.

Also applies to: 85-89

✅ Verification successful

Empty collection handling is properly implemented in assertions_at

The implementation in program.hpp shows proper error handling:

• Checks for label existence using contains
• Throws CRAB_ERROR if label not found
• Uses at for safe map access which throws on missing keys

🏁 Scripts executed

The following scripts were executed for the analysis:

Script:

#!/bin/bash
# Check if assertions_at has null checks or error handling
ast-grep --pattern 'assertions_at($_) {
  $$$
}'

Length of output: 50

---

Script:

#!/bin/bash
# Search for assertions_at implementation using a more flexible pattern
ast-grep --pattern 'assertions_at'

# Also try ripgrep for a broader search
rg "assertions_at" -A 5

Length of output: 2290

src/crab/cfg.hpp (1)

19-19: LGTM: Proper scoping of cfg_builder_t

The forward declaration and friend declaration correctly reference the global scope for cfg_builder_t, maintaining proper visibility while allowing the builder to access cfg_t's internals.

Also applies to: 24-24

src/crab/wto.hpp (2)

31-33: LGTM: Proper header inclusion and namespace organization

The label.hpp include is required for direct usage of label types, and the namespace declaration properly scopes the implementation.

---

120-120: LGTM: Constructor signature updated for namespace consistency

The constructor signature correctly references cfg_t within the crab namespace.

src/crab/wto.cpp (1)

13-14: LGTM: Implementation properly scoped within crab namespace

The implementation is correctly wrapped in the crab namespace, maintaining consistency with the header file organization.

Also applies to: 311-311

src/test/test_marshal.cpp (3)

229-231: Improved variable naming for better clarity.

The variable name inst_seq better represents its purpose as an instruction sequence.

---

266-269: Consistent variable naming improvement.

Maintains consistency with the earlier renaming of parsed to inst_seq.

---

285-288: Consistent variable naming pattern.

Completes the consistent renaming pattern across all related functions.

[coderabbitai]

🧹 Nitpick (assertive)

Eliminate duplicated code when creating Program instances.

The code initializing inst_seq and prog for both prog1 and prog2 is duplicated. Refactor to reduce redundancy.

Apply this diff:

+auto create_program = [](const auto& prog_or_error, const raw_program& raw_prog) -> Program {
+    auto inst_seq = std::get_if<InstructionSeq>(&prog_or_error);
+    REQUIRE(inst_seq != nullptr);
+    return Program::from_sequence(*inst_seq, raw_prog.info, {});
+};

-auto inst_seq1 = std::get_if<InstructionSeq>(&prog_or_error1);
-REQUIRE(inst_seq1 != nullptr);
-const Program prog1 = Program::from_sequence(*inst_seq1, raw_prog1.info, {});
+const Program prog1 = create_program(prog_or_error1, raw_prog1);

-auto inst_seq2 = std::get_if<InstructionSeq>(&prog_or_error2);
-REQUIRE(inst_seq2 != nullptr);
-const Program prog2 = Program::from_sequence(*inst_seq2, raw_prog2.info, {});
+const Program prog2 = create_program(prog_or_error2, raw_prog2);

Also applies to: 626-628

[coveralls]

coverage: 89.57% (+0.02%) from 89.547%
when pulling ed6e733 on program
into 3f78808 on main.