CBMC
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>
18 
20 
21 #include "renaming_level.h"
22 
23 // Forward declaration required since subclass is used explicitly
24 // by the parent class.
25 class goto_symex_statet;
26 
32 {
33 public:
35  unsigned depth = 0;
36 
37 protected:
39 
40 public:
44 
45  const symex_level2t &get_level2() const
46  {
47  return level2;
48  }
49 
52 
53  // A guard is a particular condition that has to pass for an instruction
54  // to be executed. The easiest example is an if/else: each instruction along
55  // the if branch will be guarded by the condition of the if (and if there
56  // is an else branch then instructions on it will be guarded by the negation
57  // of the condition of the if).
59 
62  bool reachable;
63 
64  // Map L1 names to (L2) constants. Values will be evicted from this map
65  // when they become non-constant. This is used to propagate values that have
66  // been worked out to only have one possible value.
67  //
68  // "constants" can include symbols, but only in the context of an address-of
69  // op (i.e. &x can be propagated), and an address-taken thing should only be
70  // L1.
72 
73  void output_propagation_map(std::ostream &);
74 
76  unsigned atomic_section_id = 0;
77 
79  goto_statet() = delete;
80  goto_statet &operator=(const goto_statet &other) = delete;
81  goto_statet &operator=(goto_statet &&other) = default;
82  goto_statet(const goto_statet &other) = default;
83  goto_statet(goto_statet &&other) = default;
84 
85  explicit goto_statet(guard_managert &guard_manager)
86  : guard(true_exprt(), guard_manager), reachable(true)
87  {
88  }
89 
90  void apply_condition(
91  const exprt &condition, // L2
92  const goto_symex_statet &previous_state,
93  const namespacet &ns);
94 };
95 
96 #endif // CPROVER_GOTO_SYMEX_GOTO_STATE_H
Base class for all expressions.
Definition: expr.h:56
Container for data that varies per program point, e.g.
Definition: goto_state.h:32
symex_level2t level2
Definition: goto_state.h:38
goto_statet(const goto_statet &other)=default
guardt guard
Definition: goto_state.h:58
goto_statet(guard_managert &guard_manager)
Definition: goto_state.h:85
unsigned depth
Distance from entry.
Definition: goto_state.h:35
bool reachable
Is this code reachable? If not we can take shortcuts such as not entering function calls,...
Definition: goto_state.h:62
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:43
goto_statet(goto_statet &&other)=default
goto_statet & operator=(goto_statet &&other)=default
unsigned atomic_section_id
Threads.
Definition: goto_state.h:76
sharing_mapt< irep_idt, exprt > propagation
Definition: goto_state.h:71
goto_statet()=delete
Constructors.
const symex_level2t & get_level2() const
Definition: goto_state.h:45
goto_statet & operator=(const goto_statet &other)=delete
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
Definition: goto_state.h:51
void output_propagation_map(std::ostream &)
Print the constant propagation map in a human-friendly format.
Definition: goto_state.cpp:19
sharing_mapt< exprt, symbol_exprt, false, irep_hash > dereference_cache
This is used for eliminating repeated complicated dereferences.
Definition: goto_state.h:43
Central data structure: state.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
The Boolean constant true.
Definition: std_expr.h:3055
State type in value_set_domaint, used in value-set analysis and goto-symex.
Definition: value_set.h:44
Guard Data Structure.
Renaming levels.
Sharing map.
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:20
Functor to set the level 2 renaming of SSA expressions.
Value Set.