cprover
goto_state.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Romain Brenguier, romain.brenguier@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_SYMEX_GOTO_STATE_H
13 #define CPROVER_GOTO_SYMEX_GOTO_STATE_H
14 
15 #include <util/sharing_map.h>
16 
17 #include <analyses/guard.h>
20 
21 #include "renaming_level.h"
22 
28 {
29 public:
31  unsigned depth = 0;
32 
33 protected:
35 
36 public:
37  const symex_level2t &get_level2() const
38  {
39  return level2;
40  }
41 
44 
45  // A guard is a particular condition that has to pass for an instruction
46  // to be executed. The easiest example is an if/else: each instruction along
47  // the if branch will be guarded by the condition of the if (and if there
48  // is an else branch then instructions on it will be guarded by the negation
49  // of the condition of the if).
51 
54  bool reachable;
55 
56  // Map L1 names to (L2) constants. Values will be evicted from this map
57  // when they become non-constant. This is used to propagate values that have
58  // been worked out to only have one possible value.
59  //
60  // "constants" can include symbols, but only in the context of an address-of
61  // op (i.e. &x can be propagated), and an address-taken thing should only be
62  // L1.
64 
65  void output_propagation_map(std::ostream &);
66 
68  unsigned atomic_section_id = 0;
69 
72  inline std::size_t complexity()
73  {
74  // TODO: This isn't too efficent for BDDs, try using a different size
75  // like DAG size.
76  return guard.as_expr().size();
77  }
78 
80  goto_statet() = delete;
81  goto_statet &operator=(const goto_statet &other) = delete;
82  goto_statet &operator=(goto_statet &&other) = default;
83  goto_statet(const goto_statet &other) = default;
84  goto_statet(goto_statet &&other) = default;
85 
86  explicit goto_statet(const class goto_symex_statet &s);
87 
88  explicit goto_statet(guard_managert &guard_manager)
89  : guard(true_exprt(), guard_manager), reachable(true)
90  {
91  }
92 
93  void apply_condition(
94  const exprt &condition, // L2
95  const goto_symex_statet &previous_state,
96  const namespacet &ns);
97 };
98 
99 #endif // CPROVER_GOTO_SYMEX_GOTO_STATE_H
guard_exprt
Definition: guard_expr.h:26
goto_statet::goto_statet
goto_statet(guard_managert &guard_manager)
Definition: goto_state.h:88
goto_statet::apply_condition
void apply_condition(const exprt &condition, const goto_symex_statet &previous_state, const namespacet &ns)
Given a condition that must hold on this path, propagate as much knowledge as possible.
Definition: goto_state.cpp:42
goto_statet::complexity
std::size_t complexity()
Get the complexity for this state.
Definition: goto_state.h:72
sharing_mapt
A map implemented as a tree where subtrees can be shared between different maps.
Definition: sharing_map.h:179
exprt::size
std::size_t size() const
Amount of nodes this expression tree contains.
Definition: expr.cpp:26
goto_statet::reachable
bool reachable
Is this code reachable? If not we can take shortcuts such as not entering function calls,...
Definition: goto_state.h:54
goto_symex_statet
Central data structure: state.
Definition: goto_symex_state.h:45
value_sett
State type in value_set_domaint, used in value-set analysis and goto-symex.
Definition: value_set.h:44
exprt
Base class for all expressions.
Definition: expr.h:52
goto_statet::output_propagation_map
void output_propagation_map(std::ostream &)
Print the constant propagation map in a human-friendly format.
Definition: goto_state.cpp:18
goto_statet::propagation
sharing_mapt< irep_idt, exprt > propagation
Definition: goto_state.h:63
goto_statet::operator=
goto_statet & operator=(const goto_statet &other)=delete
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
guard.h
symex_level2t
Functor to set the level 2 renaming of SSA expressions.
Definition: renaming_level.h:81
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:22
value_set.h
goto_statet::depth
unsigned depth
Distance from entry.
Definition: goto_state.h:31
guard_exprt::as_expr
exprt as_expr() const
Definition: guard_expr.h:49
renaming_level.h
goto_statet::level2
symex_level2t level2
Definition: goto_state.h:34
goto_statet::guard
guardt guard
Definition: goto_state.h:50
goto_statet::goto_statet
goto_statet()=delete
Constructors.
local_safe_pointers.h
goto_statet
Container for data that varies per program point, e.g.
Definition: goto_state.h:27
goto_statet::atomic_section_id
unsigned atomic_section_id
Threads.
Definition: goto_state.h:68
goto_statet::get_level2
const symex_level2t & get_level2() const
Definition: goto_state.h:37
true_exprt
The Boolean constant true.
Definition: std_expr.h:3954
sharing_map.h
goto_statet::value_set
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
Definition: goto_state.h:43