cprover
nondet.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Non-deterministic object init and choice for CBMC
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
9 #include "nondet.h"
10 
11 #include "allocate_objects.h"
12 #include "arith_tools.h"
13 #include "c_types.h"
14 #include "fresh_symbol.h"
15 #include "symbol.h"
16 
18  const exprt &min_value_expr,
19  const exprt &max_value_expr,
20  const std::string &basename_prefix,
21  const source_locationt &source_location,
22  allocate_objectst &allocate_objects,
23  code_blockt &instructions)
24 {
25  const allocate_local_symbolt allocate_local_symbol =
26  [&allocate_objects](
27  const typet &type, std::string basename_prefix) -> symbol_exprt {
28  return allocate_objects.allocate_automatic_local_object(
29  type, basename_prefix);
30  };
31  return generate_nondet_int(
32  min_value_expr,
33  max_value_expr,
34  basename_prefix,
35  source_location,
36  allocate_local_symbol,
37  instructions);
38 }
39 
41  const exprt &min_value_expr,
42  const exprt &max_value_expr,
43  const std::string &basename_prefix,
44  const source_locationt &source_location,
45  const allocate_local_symbolt &alocate_local_symbol,
46  code_blockt &instructions)
47 {
48  PRECONDITION(min_value_expr.type() == max_value_expr.type());
49  const typet &int_type = min_value_expr.type();
50 
51  // Declare a symbol for the non deterministic integer.
52  const symbol_exprt &nondet_symbol =
53  alocate_local_symbol(int_type, basename_prefix);
54  instructions.add(code_declt(nondet_symbol));
55 
56  // Assign the symbol any non deterministic integer value.
57  // int_type name_prefix::nondet_int = NONDET(int_type)
58  instructions.add(code_assignt(
59  nondet_symbol, side_effect_expr_nondett(int_type, source_location)));
60 
61  // Constrain the non deterministic integer with a lower bound of `min_value`.
62  // ASSUME(name_prefix::nondet_int >= min_value)
63  instructions.add(
64  code_assumet(binary_predicate_exprt(nondet_symbol, ID_ge, min_value_expr)));
65 
66  // Constrain the non deterministic integer with an upper bound of `max_value`.
67  // ASSUME(name_prefix::nondet_int <= max_value)
68  instructions.add(
69  code_assumet(binary_predicate_exprt(nondet_symbol, ID_le, max_value_expr)));
70 
71  return nondet_symbol;
72 }
73 
75  const mp_integer &min_value,
76  const mp_integer &max_value,
77  const std::string &basename_prefix,
78  const typet &int_type,
79  const source_locationt &source_location,
80  allocate_objectst &allocate_objects,
81  code_blockt &instructions)
82 {
83  PRECONDITION(min_value <= max_value);
84  return generate_nondet_int(
85  from_integer(min_value, int_type),
86  from_integer(max_value, int_type),
87  basename_prefix,
88  source_location,
89  allocate_objects,
90  instructions);
91 }
92 
94  const irep_idt &name_prefix,
95  const alternate_casest &switch_cases,
96  const typet &int_type,
97  const irep_idt &mode,
98  const source_locationt &source_location,
99  symbol_table_baset &symbol_table)
100 {
101  PRECONDITION(!switch_cases.empty());
102 
103  if(switch_cases.size() == 1)
104  return code_blockt({switch_cases[0]});
105 
106  code_blockt result_block;
107 
108  allocate_objectst allocate_objects{
109  mode, source_location, name_prefix, symbol_table};
110 
111  const symbol_exprt &switch_value = generate_nondet_int(
112  0,
113  switch_cases.size() - 1,
114  "nondet_int",
115  int_type,
116  source_location,
117  allocate_objects,
118  result_block);
119 
120  code_blockt switch_block;
121  size_t case_number = 0;
122  for(const auto &switch_case : switch_cases)
123  {
124  code_blockt this_block;
125  this_block.add(switch_case);
126  this_block.add(code_breakt());
127  code_switch_caset this_case(
128  from_integer(case_number, switch_value.type()), this_block);
129  switch_block.add(std::move(this_case));
130  ++case_number;
131  }
132 
133  code_switcht result_switch(switch_value, switch_block);
134  result_block.add(std::move(result_switch));
135  return result_block;
136 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
generate_nondet_switch
code_blockt generate_nondet_switch(const irep_idt &name_prefix, const alternate_casest &switch_cases, const typet &int_type, const irep_idt &mode, const source_locationt &source_location, symbol_table_baset &symbol_table)
Pick nondeterministically between imperative actions 'switch_cases'.
Definition: nondet.cpp:93
code_switch_caset
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1439
arith_tools.h
generate_nondet_int
symbol_exprt generate_nondet_int(const exprt &min_value_expr, const exprt &max_value_expr, const std::string &basename_prefix, const source_locationt &source_location, allocate_objectst &allocate_objects, code_blockt &instructions)
Same as generate_nondet_int( const mp_integer &min_value, const mp_integer &max_value,...
Definition: nondet.cpp:17
typet
The type of an expression, extends irept.
Definition: type.h:29
fresh_symbol.h
Fresh auxiliary symbol creation.
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:402
exprt
Base class for all expressions.
Definition: expr.h:53
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
alternate_casest
std::vector< codet > alternate_casest
Definition: nondet.h:74
code_breakt
codet representation of a break statement (within a for or while loop).
Definition: std_code.h:1598
binary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:694
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
code_assumet
An assumption, which must hold in subsequent code.
Definition: std_code.h:535
symbol.h
Symbol table entry.
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
source_locationt
Definition: source_location.h:20
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1945
allocate_local_symbolt
std::function< symbol_exprt(const typet &type, std::string)> allocate_local_symbolt
Definition: nondet.h:19
nondet.h
code_switcht
codet representing a switch statement.
Definition: std_code.h:834
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
allocate_objectst
Definition: allocate_objects.h:31
allocate_objectst::allocate_automatic_local_object
exprt allocate_automatic_local_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const irep_idt &basename_prefix="tmp")
Creates a local variable with automatic lifetime.
Definition: allocate_objects.cpp:70
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
allocate_objects.h
c_types.h