cprover
symex_assign.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_SYMEX_ASSIGN_H
13 #define CPROVER_GOTO_SYMEX_SYMEX_ASSIGN_H
14 
15 #include "symex_target.h"
16 #include <util/expr.h>
17 
18 class byte_extract_exprt;
19 class expr_skeletont;
20 class goto_symex_statet;
21 class ssa_exprt;
22 struct symex_configt;
23 
26 {
27 public:
31  const namespacet &ns,
34  : state(state),
36  ns(ns),
38  target(target)
39  {
40  }
41 
46  void assign_symbol(
47  const ssa_exprt &lhs, // L1
48  const expr_skeletont &full_lhs,
49  const exprt &rhs,
50  const exprt::operandst &guard);
51 
52  void assign_rec(
53  const exprt &lhs,
54  const expr_skeletont &full_lhs,
55  const exprt &rhs,
56  exprt::operandst &guard);
57 
58 private:
61  const namespacet &ns;
64 
65  void assign_from_struct(
66  const ssa_exprt &lhs, // L1
67  const expr_skeletont &full_lhs,
68  const struct_exprt &rhs,
69  const exprt::operandst &guard);
70 
72  const ssa_exprt &lhs, // L1
73  const expr_skeletont &full_lhs,
74  const exprt &rhs,
75  const exprt::operandst &guard);
76 
79  template <bool use_update>
80  void assign_array(
81  const index_exprt &lhs,
82  const expr_skeletont &full_lhs,
83  const exprt &rhs,
84  exprt::operandst &guard);
85 
88  template <bool use_update>
90  const member_exprt &lhs,
91  const expr_skeletont &full_lhs,
92  const exprt &rhs,
93  exprt::operandst &guard);
94 
95  void assign_if(
96  const if_exprt &lhs,
97  const expr_skeletont &full_lhs,
98  const exprt &rhs,
99  exprt::operandst &guard);
100 
101  void assign_typecast(
102  const typecast_exprt &lhs,
103  const expr_skeletont &full_lhs,
104  const exprt &rhs,
105  exprt::operandst &guard);
106 
107  void assign_byte_extract(
108  const byte_extract_exprt &lhs,
109  const expr_skeletont &full_lhs,
110  const exprt &rhs,
111  exprt::operandst &guard);
112 };
113 
114 #endif // CPROVER_GOTO_SYMEX_SYMEX_ASSIGN_H
Expression of type type extracted from some object op starting at position offset (given in number of...
Expression in which some part is missing and can be substituted for another expression.
Definition: expr_skeleton.h:26
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
Central data structure: state.
The trinary if-then-else operator.
Definition: std_expr.h:2226
Array index operator.
Definition: std_expr.h:1328
Extract member of struct or union.
Definition: std_expr.h:2667
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
Struct constructor from list of elements.
Definition: std_expr.h:1722
Functor for symex assignment.
Definition: symex_assign.h:26
void assign_byte_extract(const byte_extract_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
void assign_if(const if_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
const symex_configt & symex_config
Definition: symex_assign.h:62
void assign_non_struct_symbol(const ssa_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, const exprt::operandst &guard)
goto_symex_statet & state
Definition: symex_assign.h:59
void assign_array(const index_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
symex_targett & target
Definition: symex_assign.h:63
void assign_rec(const exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
void assign_symbol(const ssa_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, const exprt::operandst &guard)
Record the assignment of value rhs to variable lhs in state and add the equation to target: lhs#{n+1}...
void assign_struct_member(const member_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
symex_targett::assignment_typet assignment_type
Definition: symex_assign.h:60
symex_assignt(goto_symex_statet &state, symex_targett::assignment_typet assignment_type, const namespacet &ns, const symex_configt &symex_config, symex_targett &target)
Definition: symex_assign.h:28
const namespacet & ns
Definition: symex_assign.h:61
void assign_from_struct(const ssa_exprt &lhs, const expr_skeletont &full_lhs, const struct_exprt &rhs, const exprt::operandst &guard)
Assign a struct expression to a symbol.
void assign_typecast(const typecast_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
The interface of the target container for symbolic execution to record its symbolic steps into.
Definition: symex_target.h:25
Semantic type conversion.
Definition: std_expr.h:1920
Configuration used for a symbolic execution.
Definition: symex_config.h:17
Generate Equation using Symbolic Execution.