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