cprover
scratch_program.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Loop Acceleration
4 
5 Author: Matt Lewis
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_SCRATCH_PROGRAM_H
13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_SCRATCH_PROGRAM_H
14 
15 #include <memory>
16 
17 #include <util/make_unique.h>
18 #include <util/symbol_table.h>
19 
22 
23 #include <goto-symex/goto_symex.h>
26 
27 #include <solvers/smt2/smt2_dec.h>
28 
30 #include <solvers/sat/satcheck.h>
31 
32 #include "path.h"
33 
34 // Wrapper around goto_symext to make initialize_entry_point_state available.
36 {
38  message_handlert &mh,
40  symex_target_equationt &_target,
41  const optionst &options,
44  : goto_symext(
45  mh,
47  _target,
48  options,
51  {
52  }
53 
54  std::unique_ptr<statet>
56  {
58  }
59 };
60 
62 {
63 public:
65  symbol_tablet &_symbol_table,
66  message_handlert &mh,
67  guard_managert &guard_manager)
68  : constant_propagation(true),
69  symbol_table(_symbol_table),
72  equation(mh),
73  path_storage(),
75  symex(mh, symbol_table, equation, options, path_storage, guard_manager),
76  satcheck(util_make_unique<satcheckt>(mh)),
77  satchecker(ns, *satcheck, mh),
78  z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3, mh),
79  checker(&z3) // checker(&satchecker)
80  {
81  }
82 
84  void append(goto_programt &program);
85  void append_path(patht &path);
86  void append_loop(goto_programt &program, goto_programt::targett loop_header);
87 
88  targett assign(const exprt &lhs, const exprt &rhs);
89  targett assume(const exprt &guard);
90 
91  bool check_sat(bool do_slice, guard_managert &guard_manager);
92 
93  bool check_sat(guard_managert &guard_manager)
94  {
95  return check_sat(true, guard_manager);
96  }
97 
98  exprt eval(const exprt &e);
99 
100  void fix_types();
101 
103 
104 protected:
105  std::unique_ptr<goto_symex_statet> symex_state;
114 
115  std::unique_ptr<propt> satcheck;
119  static optionst get_default_options();
120 };
121 
122 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_SCRATCH_PROGRAM_H
Base class for all expressions.
Definition: expr.h:54
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
instructionst::iterator targett
Definition: goto_program.h:646
std::list< instructiont > instructionst
Definition: goto_program.h:644
The main class for the forward symbolic simulator.
Definition: goto_symex.h:35
static get_goto_functiont get_goto_function(abstract_goto_modelt &goto_model)
Return a function to get/load a goto function from the given goto model Create a default delegate to ...
Definition: symex_main.cpp:493
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Definition: goto_symex.h:789
std::unique_ptr< statet > initialize_entry_point_state(const get_goto_functiont &get_goto_function)
Initialize the symbolic execution and the given state with the beginning of the entry point function.
Definition: symex_main.cpp:404
guard_managert & guard_manager
Used to create guards.
Definition: goto_symex.h:248
const symbol_tablet & outer_symbol_table
The symbol table associated with the goto-program being executed.
Definition: goto_symex.h:234
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
The type of delegate functions that retrieve a goto_functiont for a particular function identifier.
Definition: goto_symex.h:82
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
FIFO save queue: paths are resumed in the order that they were saved.
Definition: path_storage.h:184
Storage for symbolic execution paths to be resumed later.
Definition: path_storage.h:38
scratch_programt(symbol_tablet &_symbol_table, message_handlert &mh, guard_managert &guard_manager)
goto_functionst functions
bool check_sat(guard_managert &guard_manager)
bool check_sat(bool do_slice, guard_managert &guard_manager)
scratch_program_symext symex
symbol_tablet & symbol_table
targett assume(const exprt &guard)
void append_loop(goto_programt &program, goto_programt::targett loop_header)
targett assign(const exprt &lhs, const exprt &rhs)
symbol_tablet symex_symbol_table
static optionst get_default_options()
void append(goto_programt::instructionst &instructions)
decision_proceduret * checker
std::unique_ptr< goto_symex_statet > symex_state
bv_pointerst satchecker
exprt eval(const exprt &e)
void append_path(patht &path)
path_fifot path_storage
std::unique_ptr< propt > satcheck
symex_target_equationt equation
Decision procedure interface for various SMT 2.x solvers.
Definition: smt2_dec.h:28
The symbol table.
Definition: symbol_table.h:14
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Goto Programs with Functions.
Concrete Goto Program.
Symbolic Execution.
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition: make_unique.h:19
Loop Acceleration.
std::list< path_nodet > patht
Definition: path.h:44
Storage of symbolic execution paths to resume.
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:20
std::unique_ptr< statet > initialize_entry_point_state(const get_goto_functiont &get_goto_function)
scratch_program_symext(message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage, guard_managert &guard_manager)
Author: Diffblue Ltd.
Generate Equation using Symbolic Execution.