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 
15  const exprt &min_value_expr,
16  const exprt &max_value_expr,
17  const std::string &basename_prefix,
18  const source_locationt &source_location,
19  allocate_objectst &allocate_objects,
20  code_blockt &instructions)
21 {
22  const allocate_local_symbolt allocate_local_symbol =
23  [&allocate_objects](
24  const typet &type, std::string basename_prefix) -> symbol_exprt {
25  return allocate_objects.allocate_automatic_local_object(
26  type, basename_prefix);
27  };
28  return generate_nondet_int(
29  min_value_expr,
30  max_value_expr,
31  basename_prefix,
32  source_location,
33  allocate_local_symbol,
34  instructions);
35 }
36 
38  const exprt &min_value_expr,
39  const exprt &max_value_expr,
40  const std::string &basename_prefix,
41  const source_locationt &source_location,
42  const allocate_local_symbolt &alocate_local_symbol,
43  code_blockt &instructions)
44 {
45  PRECONDITION(min_value_expr.type() == max_value_expr.type());
46  const typet &int_type = min_value_expr.type();
47 
48  // Declare a symbol for the non deterministic integer.
49  const symbol_exprt &nondet_symbol =
50  alocate_local_symbol(int_type, basename_prefix);
51  instructions.add(code_declt(nondet_symbol));
52 
53  // Assign the symbol any non deterministic integer value.
54  // int_type name_prefix::nondet_int = NONDET(int_type)
55  instructions.add(code_assignt(
56  nondet_symbol, side_effect_expr_nondett(int_type, source_location)));
57 
58  // Constrain the non deterministic integer with a lower bound of `min_value`.
59  // ASSUME(name_prefix::nondet_int >= min_value)
60  instructions.add(
61  code_assumet(binary_predicate_exprt(nondet_symbol, ID_ge, min_value_expr)));
62 
63  // Constrain the non deterministic integer with an upper bound of `max_value`.
64  // ASSUME(name_prefix::nondet_int <= max_value)
65  instructions.add(
66  code_assumet(binary_predicate_exprt(nondet_symbol, ID_le, max_value_expr)));
67 
68  return nondet_symbol;
69 }
70 
72  const mp_integer &min_value,
73  const mp_integer &max_value,
74  const std::string &basename_prefix,
75  const typet &int_type,
76  const source_locationt &source_location,
77  allocate_objectst &allocate_objects,
78  code_blockt &instructions)
79 {
80  PRECONDITION(min_value <= max_value);
81  return generate_nondet_int(
82  from_integer(min_value, int_type),
83  from_integer(max_value, int_type),
84  basename_prefix,
85  source_location,
86  allocate_objects,
87  instructions);
88 }
89 
91  const irep_idt &name_prefix,
92  const alternate_casest &switch_cases,
93  const typet &int_type,
94  const irep_idt &mode,
95  const source_locationt &source_location,
96  symbol_table_baset &symbol_table)
97 {
98  PRECONDITION(!switch_cases.empty());
99 
100  if(switch_cases.size() == 1)
101  return code_blockt({switch_cases[0]});
102 
103  code_blockt result_block;
104 
105  allocate_objectst allocate_objects{
106  mode, source_location, name_prefix, symbol_table};
107 
108  const symbol_exprt &switch_value = generate_nondet_int(
109  0,
110  switch_cases.size() - 1,
111  "nondet_int",
112  int_type,
113  source_location,
114  allocate_objects,
115  result_block);
116 
117  code_blockt switch_block;
118  size_t case_number = 0;
119  for(const auto &switch_case : switch_cases)
120  {
121  code_blockt this_block;
122  this_block.add(switch_case);
123  this_block.add(code_breakt());
124  code_switch_caset this_case(
125  from_integer(case_number, switch_value.type()), this_block);
126  switch_block.add(std::move(this_case));
127  ++case_number;
128  }
129 
130  code_switcht result_switch(switch_value, switch_block);
131  result_block.add(std::move(result_switch));
132  return result_block;
133 }
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:168
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:90
code_switch_caset
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1469
mp_integer
BigInt mp_integer
Definition: smt_terms.h:12
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:14
typet
The type of an expression, extends irept.
Definition: type.h:28
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:400
exprt
Base class for all expressions.
Definition: expr.h:54
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
alternate_casest
std::vector< codet > alternate_casest
Definition: nondet.h:73
code_breakt
codet representation of a break statement (within a for or while loop).
Definition: std_code.h:1628
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:643
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
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:565
code_blockt::add
void add(const codet &code)
Definition: std_code.h:206
source_locationt
Definition: source_location.h:19
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1966
allocate_local_symbolt
std::function< symbol_exprt(const typet &type, std::string)> allocate_local_symbolt
Definition: nondet.h:18
nondet.h
code_switcht
codet representing a switch statement.
Definition: std_code.h:864
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:28
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:293
allocate_objects.h