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 #include <string>
17 
18 #include <util/make_unique.h>
19 #include <util/message.h>
20 #include <util/symbol_table.h>
21 
24 
25 #include <goto-symex/goto_symex.h>
28 
29 #include <solvers/smt2/smt2_dec.h>
30 
32 #include <solvers/sat/satcheck.h>
33 
34 #include "path.h"
35 
37 {
38 public:
40  symbol_tablet &_symbol_table,
41  message_handlert &mh,
42  guard_managert &guard_manager)
43  : constant_propagation(true),
44  symbol_table(_symbol_table),
47  equation(mh),
48  path_storage(),
50  symex(mh, symbol_table, equation, options, path_storage, guard_manager),
51  satcheck(util_make_unique<satcheckt>(mh)),
52  satchecker(ns, *satcheck, mh),
53  z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3),
54  checker(&z3) // checker(&satchecker)
55  {
56  }
57 
59  void append(goto_programt &program);
60  void append_path(patht &path);
61  void append_loop(goto_programt &program, goto_programt::targett loop_header);
62 
63  targett assign(const exprt &lhs, const exprt &rhs);
64  targett assume(const exprt &guard);
65 
66  bool check_sat(bool do_slice, guard_managert &guard_manager);
67 
68  bool check_sat(guard_managert &guard_manager)
69  {
70  return check_sat(true, guard_manager);
71  }
72 
73  exprt eval(const exprt &e);
74 
75  void fix_types();
76 
78 
79 protected:
80  std::unique_ptr<goto_symex_statet> symex_state;
89 
90  std::unique_ptr<propt> satcheck;
95 };
96 
97 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_SCRATCH_PROGRAM_H
scratch_programt::symex_symbol_table
symbol_tablet symex_symbol_table
Definition: scratch_program.h:83
path.h
Loop Acceleration.
symex_target_equation.h
Generate Equation using Symbolic Execution.
scratch_programt::ns
namespacet ns
Definition: scratch_program.h:84
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
path_fifot
FIFO save queue: paths are resumed in the order that they were saved.
Definition: path_storage.h:184
optionst
Definition: options.h:23
decision_proceduret
Definition: decision_procedure.h:21
goto_programt::instructionst
std::list< instructiont > instructionst
Definition: goto_program.h:577
scratch_programt::checker
decision_proceduret * checker
Definition: scratch_program.h:93
scratch_programt::options
optionst options
Definition: scratch_program.h:87
exprt
Base class for all expressions.
Definition: expr.h:53
scratch_programt::symbol_table
symbol_tablet & symbol_table
Definition: scratch_program.h:82
scratch_programt::scratch_programt
scratch_programt(symbol_tablet &_symbol_table, message_handlert &mh, guard_managert &guard_manager)
Definition: scratch_program.h:39
scratch_programt::append
void append(goto_programt::instructionst &instructions)
Definition: scratch_program.cpp:82
path_storage.h
Storage of symbolic execution paths to resume.
scratch_programt::constant_propagation
bool constant_propagation
Definition: scratch_program.h:77
bv_pointers.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
guard_expr_managert
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:23
util_make_unique
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition: make_unique.h:19
scratch_programt::append_loop
void append_loop(goto_programt &program, goto_programt::targett loop_header)
Definition: scratch_program.cpp:185
make_unique.h
scratch_programt::functions
goto_functionst functions
Definition: scratch_program.h:81
scratch_programt
Definition: scratch_program.h:37
scratch_programt::fix_types
void fix_types()
Definition: scratch_program.cpp:128
scratch_programt::eval
exprt eval(const exprt &e)
Definition: scratch_program.cpp:77
goto_symex.h
Symbolic Execution.
goto_symext
The main class for the forward symbolic simulator.
Definition: goto_symex.h:48
smt2_dec.h
scratch_programt::check_sat
bool check_sat(guard_managert &guard_manager)
Definition: scratch_program.h:68
bv_pointerst
Definition: bv_pointers.h:18
scratch_programt::assume
targett assume(const exprt &guard)
Definition: scratch_program.cpp:97
message_handlert
Definition: message.h:28
scratch_programt::z3
smt2_dect z3
Definition: scratch_program.h:92
scratch_programt::equation
symex_target_equationt equation
Definition: scratch_program.h:85
scratch_programt::satcheck
std::unique_ptr< propt > satcheck
Definition: scratch_program.h:90
scratch_programt::append_path
void append_path(patht &path)
Definition: scratch_program.cpp:153
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: symex_target_equation.h:41
goto_program.h
Concrete Goto Program.
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
satcheck.h
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
scratch_programt::symex_state
std::unique_ptr< goto_symex_statet > symex_state
Definition: scratch_program.h:80
patht
std::list< path_nodet > patht
Definition: path.h:45
scratch_programt::symex
goto_symext symex
Definition: scratch_program.h:88
smt2_dect
Decision procedure interface for various SMT 2.x solvers.
Definition: smt2_dec.h:30
goto_functions.h
Goto Programs with Functions.
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
scratch_programt::get_default_options
static optionst get_default_options()
Definition: scratch_program.cpp:211
scratch_programt::satchecker
bv_pointerst satchecker
Definition: scratch_program.h:91
scratch_programt::check_sat
bool check_sat(bool do_slice, guard_managert &guard_manager)
Definition: scratch_program.cpp:26
symbol_table.h
Author: Diffblue Ltd.
message.h
scratch_programt::assign
targett assign(const exprt &lhs, const exprt &rhs)
Definition: scratch_program.cpp:90
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
scratch_programt::path_storage
path_fifot path_storage
Definition: scratch_program.h:86