Implement ebpf_check_constraints_at_label

[Alan-Jowett]

Resolves: #728

This pull request exposes a new API "ebpf_check_constraints_at_label" which permits the caller to compare a set of constraints against the model at a specific label. If the model and the constraints differ it will return the two sets of constraints.

Enhancements and New Features:

• src/asm_parse.hpp: Exposed existing function to parse linear constraints.
• src/asm_syntax.hpp: Extended the label_t struct to support initialization from a string label.
• src/config.hpp: Added a new option to store pre-invariants in the verifier options.
• src/crab_verifier.cpp: Implemented functions to store pre-invariants and check constraints at specific labels. [1] [2] [3] [4]
• src/crab_verifier.hpp: Declared the new function for checking constraints at a label.

Test Case Updates:

• src/ebpf_yaml.cpp: Updated YAML parsing to include invariants to check and modified test case execution to validate these invariants. [1] [2] [3] [4] [5]
• src/ebpf_yaml.hpp: Added a new field to the TestCase struct for invariants to check.
• test-data/add.yaml: Added a new test case to check concrete state invariants.

Summary by CodeRabbit

Summary by CodeRabbit

• New Features

  • Introduced a new function to parse linear constraints and handle pre-invariants.
  • Added support for checking invariants in YAML test cases.
  • Enhanced the RawTestCase structure to include invariants to check.
  • Added new member variables to manage invariants in the TestCase struct.

• Bug Fixes

  • Improved error handling for invariant checks during verification.

• Documentation

  • Updated test cases to include new examples for checking concrete states.

• Chores

  • Added new headers and modified existing structures to accommodate new features.