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 <util/arith_tools.h>
12 #include <util/c_types.h>
13 #include <util/fresh_symbol.h>
14 #include <util/symbol.h>
15 
37  const mp_integer &min_value,
38  const mp_integer &max_value,
39  const std::string &name_prefix,
40  const typet &int_type,
41  const irep_idt &mode,
42  const source_locationt &source_location,
43  symbol_table_baset &symbol_table,
44  code_blockt &instructions)
45 {
46  PRECONDITION(min_value < max_value);
47 
48  // Declare a symbol for the non deterministic integer.
49  const symbol_exprt &nondet_symbol =
51  int_type, name_prefix, "nondet_int", source_location, mode, symbol_table)
52  .symbol_expr();
53  instructions.add(code_declt(nondet_symbol));
54 
55  // Assign the symbol any non deterministic integer value.
56  // int_type name_prefix::nondet_int = NONDET(int_type)
57  instructions.add(
58  code_assignt(nondet_symbol, side_effect_expr_nondett(int_type)));
59 
60  // Constrain the non deterministic integer with a lower bound of `min_value`.
61  // ASSUME(name_prefix::nondet_int >= min_value)
62  instructions.add(
65  nondet_symbol, ID_ge, from_integer(min_value, int_type))));
66 
67  // Constrain the non deterministic integer with an upper bound of `max_value`.
68  // ASSUME(name_prefix::nondet_int <= max_value)
69  instructions.add(
72  nondet_symbol, ID_le, from_integer(max_value, int_type))));
73 
74  return nondet_symbol;
75 }
76 
88  const irep_idt &name_prefix,
89  const alternate_casest &switch_cases,
90  const typet &int_type,
91  const irep_idt &mode,
92  const source_locationt &source_location,
93  symbol_table_baset &symbol_table)
94 {
95  PRECONDITION(!switch_cases.empty());
96 
97  if(switch_cases.size() == 1)
98  return code_blockt({switch_cases[0]});
99 
100  code_blockt result_block;
101 
102  const symbol_exprt &switch_value = generate_nondet_int(
103  0,
104  switch_cases.size() - 1,
105  id2string(name_prefix),
106  int_type,
107  mode,
108  source_location,
109  symbol_table,
110  result_block);
111 
112  code_blockt switch_block;
113  size_t case_number = 0;
114  for(const auto &switch_case : switch_cases)
115  {
116  code_blockt this_block;
117  this_block.add(switch_case);
118  this_block.add(code_breakt());
119  code_switch_caset this_case(
120  from_integer(case_number, switch_value.type()), this_block);
121  switch_block.add(std::move(this_case));
122  ++case_number;
123  }
124 
125  code_switcht result_switch(switch_value, switch_block);
126  result_block.add(std::move(result_switch));
127  return result_block;
128 }
The type of an expression, extends irept.
Definition: type.h:27
symbol_exprt generate_nondet_int(const mp_integer &min_value, const mp_integer &max_value, const std::string &name_prefix, const typet &int_type, const irep_idt &mode, const source_locationt &source_location, symbol_table_baset &symbol_table, code_blockt &instructions)
Gets a fresh nondet choice in range (min_value, max_value).
Definition: nondet.cpp:36
BigInt mp_integer
Definition: mp_arith.h:22
codet representing a switch statement.
Definition: std_code.h:705
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
Symbol table entry.
Fresh auxiliary symbol creation.
typet & type()
Return the type of the expression.
Definition: expr.h:68
void add(const codet &code)
Definition: std_code.h:189
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
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:87
A codet representing the declaration of a local variable.
Definition: std_code.h:352
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
An assumption, which must hold in subsequent code.
Definition: std_code.h:496
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
codet representation of a break statement (within a for or while loop).
Definition: std_code.h:1400
The symbol table base class interface.
static mp_integer max_value(const typet &type)
Get max value for an integer type.
A codet representing sequential composition of program statements.
Definition: std_code.h:150
Expression to hold a symbol (variable)
Definition: std_expr.h:143
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1326
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:835
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
A codet representing an assignment in the program.
Definition: std_code.h:256
std::vector< codet > alternate_casest
Definition: nondet.h:26