P4C
The P4 Compiler
Loading...
Searching...
No Matches
selected_branches.h
1#ifndef BACKENDS_P4TOOLS_MODULES_TESTGEN_CORE_SYMBOLIC_EXECUTOR_SELECTED_BRANCHES_H_
2#define BACKENDS_P4TOOLS_MODULES_TESTGEN_CORE_SYMBOLIC_EXECUTOR_SELECTED_BRANCHES_H_
3
4#include <cstdint>
5#include <list>
6#include <string>
7#include <vector>
8
9#include "ir/solver.h"
10
11#include "backends/p4tools/modules/testgen/core/program_info.h"
12#include "backends/p4tools/modules/testgen/core/symbolic_executor/symbolic_executor.h"
13#include "backends/p4tools/modules/testgen/lib/execution_state.h"
14
15namespace P4::P4Tools::P4Testgen {
16
19 public:
23 void runImpl(const Callback &callBack, ExecutionStateReference executionState) override;
24
27 std::string selectedBranchesStr);
28
29 private:
33 ExecutionState *chooseBranch(const std::vector<Branch> &branches, uint64_t nextBranch);
34
36 std::list<uint64_t> selectedBranches;
37};
38
39} // namespace P4::P4Tools::P4Testgen
40
41#endif /* BACKENDS_P4TOOLS_MODULES_TESTGEN_CORE_SYMBOLIC_EXECUTOR_SELECTED_BRANCHES_H_ */
Provides a higher-level interface for an SMT solver.
Definition solver.h:24
Represents state of execution after having reached a program point.
Definition execution_state.h:34
Stores target-specific information about a P4 program.
Definition core/program_info.h:21
Explores one path described by a list of branches.
Definition selected_branches.h:18
SelectedBranches(AbstractSolver &solver, const ProgramInfo &programInfo, std::string selectedBranchesStr)
Constructor for this strategy, considering inheritance.
Definition selected_branches.cpp:79
void runImpl(const Callback &callBack, ExecutionStateReference executionState) override
Definition selected_branches.cpp:19
Definition symbolic_executor.h:21
const ProgramInfo & programInfo
Target-specific information about the P4 program.
Definition symbolic_executor.h:62
std::function< bool(const FinalState &)> Callback
Definition symbolic_executor.h:36
Definition phv/solver/action_constraint_solver.cpp:33