Go to the documentation of this file.
58 if(exp.
id() != ID_symbol)
72 exprt result = size_of_opt.value();
73 result.
add(ID_C_c_sizeof_type) = type;
87 for(
const auto &t : loop)
89 t->is_goto() && t->get_target() == loop_head &&
90 t->location_number > loop_end->location_number)
95 loop_end->get_condition().find(ID_C_spec_loop_invariant));
121 a->source_location.set_comment(
"Check loop invariant before entry");
132 if(!loop_head->is_goto())
141 goto_function.body.insert_before_swap(loop_head, havoc_code);
148 goto_function.body.insert_before_swap(loop_end, a);
153 loop_end->targets.clear();
155 if(loop_head->is_goto())
158 loop_end->set_condition(
boolean_negate(loop_end->get_condition()));
174 return type.has_contract();
182 if(expression.
id() == ID_not || expression.
id() == ID_typecast)
189 if(expression.
id() == ID_notequal || expression.
id() == ID_implies)
197 if(expression.
id() == ID_if)
201 const auto &if_expression =
to_if_expr(expression);
206 if(expression.
id() == ID_and || expression.
id() == ID_or)
211 for(
const auto &operand : multi_ary_expression.operands())
216 else if(expression.
id() == ID_exists || expression.
id() == ID_forall)
221 const auto &quantified_variables = quantifier_expression.variables();
222 for(
const auto &quantified_variable : quantified_variables)
225 const auto &quantified_symbol =
to_symbol_expr(quantified_variable);
229 quantified_symbol.type(),
230 id2string(quantified_symbol.get_identifier()),
232 quantified_symbol.source_location(),
238 quantified_symbol.get_identifier(), quantified_symbol.type());
265 exprt assigns = type.assigns();
266 exprt requires = type.requires();
267 exprt ensures = type.ensures();
302 "ignored_return_value",
314 code_function_callt::argumentst::const_iterator a_it=
316 for(code_typet::parameterst::const_iterator p_it = type.parameters().begin();
317 p_it != type.parameters().end() && a_it != call.
arguments().end();
320 if(!p_it->get_identifier().empty())
347 std::advance(target, lines_to_iterate);
356 function_symbol.
location, function_id, function_symbol.
mode);
359 std::size_t lines_to_iterate = assigns_havoc.
instructions.size();
361 std::advance(target, lines_to_iterate);
376 std::advance(target, lines_to_iterate);
392 for(
const auto &loop : natural_loops.
loop_map)
394 goto_function, local_may_alias, loop.first, loop.second);
414 std::vector<exprt> &aliasable_references)
417 operands.reserve(aliasable_references.size());
418 for(
auto aliasable : aliasable_references)
426 goto_programt::instructionst::iterator &instruction_iterator,
429 std::set<irep_idt> &freely_assignable_symbols,
433 instruction_iterator->is_assign(),
434 "The first instruction of instrument_assign_statement should always be"
437 const exprt &lhs = instruction_iterator->get_assign().lhs();
444 int lines_to_iterate = alias_assertion.
instructions.size();
446 std::advance(instruction_iterator, lines_to_iterate);
450 goto_programt::instructionst::iterator &instruction_iterator,
454 std::set<irep_idt> &freely_assignable_symbols,
458 instruction_iterator->is_function_call(),
459 "The first argument of instrument_call_statement should always be "
466 if(called_name ==
"malloc")
468 goto_programt::instructionst::iterator local_instruction_iterator =
469 instruction_iterator;
473 local_instruction_iterator++;
474 if(local_instruction_iterator->is_assign())
476 const exprt &rhs = local_instruction_iterator->get_assign().rhs();
478 rhs.
id() == ID_typecast,
479 "malloc is called but the result is not cast. Excluding result from "
480 "the assignable memory frame.");
488 int lines_to_iterate = pointer_capture.
instructions.size();
490 std::advance(instruction_iterator, lines_to_iterate + 1);
497 freely_assignable_symbols.find(
499 freely_assignable_symbols.end())
507 ++instruction_iterator;
514 exprt called_assigns =
516 if(called_assigns.
is_nil())
524 ++instruction_iterator;
532 code_function_callt::argumentst::const_iterator a_it =
534 for(code_typet::parameterst::const_iterator p_it =
540 if(!p_it->get_identifier().empty())
551 called_assigns, *
this, function_id,
log);
558 ++instruction_iterator;
565 std::vector<goto_programt::instructiont> back_gotos;
566 std::vector<goto_programt::instructiont> malloc_calls;
573 back_gotos.push_back(instruction);
581 if(called_name ==
"malloc")
583 malloc_calls.push_back(instruction);
590 for(
auto goto_entry : back_gotos)
592 for(
const auto &target : goto_entry.targets)
594 for(
auto malloc_entry : malloc_calls)
597 malloc_entry.location_number >= target->location_number &&
598 malloc_entry.location_number < goto_entry.location_number)
600 log.
error() <<
"Call to malloc at location "
601 << malloc_entry.location_number <<
" falls between goto "
602 <<
"source location " << goto_entry.location_number
603 <<
" and it's destination at location "
604 << target->location_number <<
". "
605 <<
"Unable to complete instrumentation, as this malloc "
621 log.
error() <<
"Could not find function '" << function_name
622 <<
"' in goto-program; not enforcing contracts."
632 const irep_idt function_id(function_name);
636 exprt assigns_expr = type.assigns();
643 goto_programt::instructionst::iterator instruction_it =
650 function_symbol.
location, function_name, function_symbol.
mode);
653 std::set<irep_idt> freely_assignable_symbols;
656 freely_assignable_symbols.insert(param.get_identifier());
659 int lines_to_iterate = standin_decls.
instructions.size();
661 std::advance(instruction_it, lines_to_iterate);
669 for(; instruction_it != program.
instructions.end(); ++instruction_it)
671 if(instruction_it->is_decl())
673 freely_assignable_symbols.insert(
674 instruction_it->get_decl().symbol().get_identifier());
677 assigns.
add_target(instruction_it->get_decl().symbol());
687 else if(instruction_it->is_assign())
693 freely_assignable_symbols,
696 else if(instruction_it->is_function_call())
703 freely_assignable_symbols,
709 while(!instruction_it->is_end_function())
728 std::stringstream ss;
731 const irep_idt original(fun_to_enforce);
736 log.
error() <<
"Could not find function '" << fun_to_enforce
737 <<
"' in goto-program; not enforcing contracts."
747 sl.
set_file(
"instrumented for code contracts");
751 mangled_sym = *original_sym;
752 mangled_sym.
name = mangled;
757 mangled_found.second,
758 "There should be no existing function called " + ss.str() +
759 " in the symbol table because that name is a mangled name");
765 "There should be no function called " + fun_to_enforce +
766 " in the function map because that function should have had its"
772 "There should be a function called " + ss.str() +
773 " in the function map because we inserted a fresh goto-program"
774 " with that mangled name");
793 const exprt &assigns = code_type.assigns();
794 const exprt &requires = code_type.requires();
795 const exprt &ensures = code_type.ensures();
798 "Code contract enforcement is trivial without an ensures or assigns "
826 code_type.return_type(),
827 skip->source_location,
829 function_symbol.
mode)
841 goto_functionst::function_mapt::iterator f_it =
846 for(
const auto ¶meter : gf.parameter_identifiers)
851 parameter_symbol.
type,
854 parameter_symbol.
mode)
875 exprt requires_cond = requires;
888 exprt ensures_cond = ensures;
911 const std::set<std::string> &funs_to_replace)
914 for(
const auto &fun : funs_to_replace)
919 <<
"' does not have a contract; "
920 "not replacing calls with contract."
932 if(ins->is_function_call())
941 auto found = std::find(
942 funs_to_replace.begin(),
943 funs_to_replace.end(),
945 if(found == funs_to_replace.end())
949 function_name, goto_function.second.body, ins);
967 std::set<std::string> funs_to_replace;
971 funs_to_replace.insert(
id2string(goto_function.first));
978 std::set<std::string> funs_to_enforce;
982 funs_to_enforce.insert(
id2string(goto_function.first));
990 const std::set<std::string> &funs_to_enforce)
993 for(
const auto &fun : funs_to_enforce)
999 log.
error() <<
"Could not find function '" << fun
1000 <<
"' in goto-program; not enforcing contracts."
1009 log.
error() <<
"Could not find any contracts within function '" << fun
1021 const exprt &object_ptr,
1027 pointer_for(object_ptr),
1030 local_standin_variable(
typet())
1039 function_symbol.
mode);
1051 std::vector<symbol_exprt>
1054 std::vector<symbol_exprt> result;
1087 code_assignt(std::move(lhs), std::move(rhs)), location));
1088 target->code_nonconst().add_source_location() = location;
1090 return assigns_havoc;
1094 const exprt &object_ptr,
1100 pointer_for(object_ptr),
1103 main_struct_standin(
typet())
1105 const symbolt &struct_symbol =
1114 function_symbol.
mode);
1126 std::vector<exprt> component_members;
1131 component_members.push_back(current_member);
1134 while(!component_members.empty())
1136 exprt current_operation = component_members.front();
1141 operation_address.
type(),
1144 function_symbol.
mode);
1156 if(current_operation.
type().
id() == ID_struct_tag)
1158 const symbolt ¤t_struct_symbol =
1166 component_members.push_back(current_member);
1169 component_members.erase(component_members.begin());
1173 std::vector<symbol_exprt>
1187 const typet &standin_concrete_type =
1190 INVARIANT(left_size.has_value(),
"Unable to determine size of type (lhs).");
1192 right_size.has_value(),
"Unable to determine size of type (rhs).");
1193 if(*left_size == *right_size)
1199 disjuncts.push_back(
and_exprt{same_obj, same_offset});
1222 exprt current_size =
1224 exprt curr_upper_offset =
1228 exprt called_upper_offset =
1235 exprt in_range_upper =
1257 code_assignt(std::move(lhs), std::move(rhs)), location));
1258 target->code_nonconst().add_source_location() = location;
1260 return assigns_havoc;
1264 const exprt &object_ptr,
1269 lower_offset_object(),
1270 upper_offset_object(),
1271 array_standin_variable(
typet()),
1272 lower_offset_variable(
typet()),
1273 upper_offset_variable(
typet())
1282 function_symbol.
mode);
1293 if(object_ptr.
id() == ID_address_of)
1295 exprt constant_size =
1307 function_symbol.
mode);
1328 function_symbol.
mode);
1341 std::vector<symbol_exprt>
1344 std::vector<symbol_exprt> result;
1359 exprt array_type_size =
1365 irep_idt offset_irep(offset_string);
1370 assigns_tgts.insert(array_deref);
1373 for(
auto lhs : assigns_tgts)
1379 code_assignt(std::move(lhs), std::move(rhs)), location));
1380 target->code_nonconst().add_source_location() = location;
1383 return assigns_havoc;
1431 const exprt &assigns,
1435 : assigns_expr(assigns),
1437 function_id(function_id),
1455 if(current_operation.
id() == ID_address_of)
1460 targets.push_back(array_target);
1461 return array_target;
1463 else if(current_operation.
type().
id() == ID_struct_tag)
1468 targets.push_back(struct_target);
1469 return struct_target;
1476 targets.push_back(scalar_target);
1477 return scalar_target;
1493 target->get_init_block().instructions)
1510 for(
symbol_exprt symbol : target->temporary_declarations())
1528 for(
symbol_exprt symbol : target->temporary_declarations())
1530 dead_statements.
add(
1534 return dead_statements;
1546 target->havoc_code(location).instructions)
1548 havoc_statements.
add(std::move(instruction));
1551 return havoc_statements;
1563 bool first_iter =
true;
1569 result = target->alias_expression(left_ptr);
1574 result =
or_exprt(result, target->alias_expression(left_ptr));
1583 if(called_assigns.
targets.empty())
1588 bool first_clause =
true;
1592 bool first_iter =
true;
1598 current_target_compatible =
1599 target->compatible_expression(*called_target);
1604 current_target_compatible =
or_exprt(
1605 current_target_compatible,
1606 target->compatible_expression(*called_target));
1611 result = current_target_compatible;
1612 first_clause =
false;
1617 conjuncts.push_back(result);
1618 conjuncts.push_back(current_target_compatible);
std::vector< symbol_exprt > temporary_declarations() const
Class that provides messages with a built-in verbosity 'level'.
#define Forall_goto_program_instructions(it, program)
const componentst & components() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
exprt compatible_expression(const assigns_clause_targett &called_target)
const code_with_contract_typet & to_code_with_contract_type(const typet &type)
Cast a typet to a code_with_contract_typet.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const irep_idt function_id
goto_programt havoc_code(source_locationt location) const
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
source_locationt source_location
The location of the instruction in the source file.
const typet & subtype() const
exprt compatible_expression(const assigns_clause_targett &called_target)
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
void add_contract_check(const irep_idt &, const irep_idt &, goto_programt &dest)
void set_comment(const irep_idt &comment)
exprt upper_offset_object
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
goto_programt dead_stmts(source_locationt location, irep_idt function_name, irep_idt language_mode)
#define CHECK_RETURN(CONDITION)
The type of an expression, extends irept.
std::vector< assigns_clause_targett * > targets
Fresh auxiliary symbol creation.
const exprt & assigns_expr
void add_quantified_variable(exprt expression, replace_symbolt &replace, irep_idt mode)
This function recursively searches the expression to find nested or non-nested quantified expressions...
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
typet type
Type of symbol.
Operator to dereference a pointer.
std::vector< symbol_exprt > temporary_declarations() const
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
static exprt pointer_for(const exprt &exp)
irept & add(const irep_namet &name)
Various predicates over pointers in programs.
assigns_clause_array_targett(const exprt &object_ptr, code_contractst &contract, messaget &log_parameter, const irep_idt &function_id)
symbol_exprt lower_offset_variable
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
exprt compatible_expression(const assigns_clause_targett &called_target)
bool apply_function_contract(const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett target)
A non-fatal assertion, which checks a condition then permits execution to continue.
Unbounded, signed integers (mathematical integers, not bitvectors)
Predicate to be used with the exprt::visit() function.
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
The plus expression Associativity is not specified.
bool empty() const
Is the program empty?
exprt alias_expression(const exprt &lhs)
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
const exprt & assigns() const
const code_contractst & contract
assigns_clause_targett * add_pointer_target(exprt current_operation)
assigns_clause_targett * add_target(exprt current_operation)
assigns_clauset(const exprt &assigns, code_contractst &contract, const irep_idt function_id, messaget log_parameter)
const exprt pointer_object
function_mapt function_map
Expression to hold a symbol (variable)
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
void visit(class expr_visitort &visitor)
These are pre-order traversal visitors, i.e., the visitor is executed on a node before its children h...
static void check_apply_invariants(goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, const goto_programt::targett loop_head, const loopt &loop)
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
void instrument_call_statement(goto_programt::instructionst::iterator &ins_it, goto_programt &program, exprt &assigns, const irep_idt &function_id, std::set< irep_idt > &freely_assignable_symbols, assigns_clauset &assigns_clause)
Inserts an assertion statement into program before the function call at ins_it, to ensure that any me...
void instrument_assign_statement(goto_programt::instructionst::iterator &instruction_it, goto_programt &program, exprt &assigns, std::set< irep_idt > &freely_assignable_symbols, assigns_clauset &assigns_clause)
Inserts an assertion statement into program before the assignment instruction_it, to ensure that the ...
unsignedbv_typet unsigned_long_int_type()
void set_line(const irep_idt &line)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
std::vector< symbol_exprt > local_standin_variables
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
std::vector< symbol_exprt > temporary_declarations() const
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
std::set< exprt > modifiest
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
goto_programt init_block(source_locationt location)
irep_idt mode
Language mode.
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
signedbv_typet signed_int_type()
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
goto_programt & get_init_block()
Field-insensitive, location-sensitive may-alias analysis.
const std::string & id2string(const irep_idt &d)
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
bool has_contract(const irep_idt)
Does the named function have a contract?
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
#define PRECONDITION(CONDITION)
const source_locationt & source_location() const
const irep_idt & get_identifier() const
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
An assumption, which must hold in subsequent code.
exprt alias_expression(const exprt &lhs)
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
void set_file(const irep_idt &file)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
exprt create_alias_expression(const exprt &lhs, std::vector< exprt > &aliasable_references)
Creates a boolean expression which is true when there exists an expression in aliasable_references wi...
const code_function_callt & get_function_call() const
Get the function call for FUNCTION_CALL.
symbol_exprt main_struct_standin
bool check_for_looped_mallocs(const goto_programt &)
Check if there are any malloc statements which may be repeated because of a goto statement that jumps...
bool add_pointer_checks(const std::string &)
Insert assertion statements into the goto program to ensure that assigned memory is within the assign...
A loop, specified as a set of instructions.
Binary multiplication Associativity is not specified.
exprt alias_expression(const exprt &lhs)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
goto_programt & temporary_declarations(source_locationt location, irep_idt function_name, irep_idt language_mode)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
exprt compatible_expression(const assigns_clauset &called_assigns)
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
std::vector< exprt > operandst
The Boolean constant false.
void convert_to_goto(const codet &code, const irep_idt &mode, goto_programt &program)
Create goto instructions based on code and add them to program.
const parameterst & parameters() const
symbol_exprt array_standin_variable
exprt alias_expression(const exprt &lhs)
exprt pointer_offset(const exprt &pointer)
Helper functions for k-induction and loop invariants.
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
void apply_loop_contract(goto_functionst::goto_functiont &goto_function)
goto_programt havoc_code(source_locationt location, irep_idt function_name, irep_idt language_mode)
static instructiont make_return(const source_locationt &l=source_locationt::nil())
void operator()(const exprt &exp) override
A side_effect_exprt that returns a non-deterministically chosen value.
::goto_functiont goto_functiont
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &source_location, const irep_idt &function_id, const irep_idt &mode)
Extract member of struct or union.
instructionst instructions
The list of instructions in the goto program.
goto_programt havoc_code(source_locationt location) const
Deprecated expression utility functions.
symbol_exprt local_standin_variable
message_handlert & get_message_handler()
bool enforce_contracts()
Call enforce_contracts() on all functions that have a contract.
Structure type, corresponds to C style structs.
symbol_exprt upper_offset_variable
codet representation of a "return from a function" statement.
goto_functionst & goto_functions
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
source_locationt location
Source code location of definition of symbol.
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
exprt same_object(const exprt &p1, const exprt &p2)
exprt lower_offset_object
goto_programt havoc_code(source_locationt location) const
A generic container class for the GOTO intermediate representation of one function.
signedbv_typet signed_long_int_type()
bool replace_calls()
Call replace_calls() on all calls to any function that has a contract.
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
std::unordered_set< irep_idt > summarized
bool empty() const
Returns true if this loop contains no instructions.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
goto_programt standin_declarations
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
bool enforce_contract(const std::string &)
Enforce contract of a single function.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Semantic type conversion.
bool found_return_value()
A codet representing an assignment in the program.
exprt get_size(const typet &type, const namespacet &ns, messaget &log)
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
The Boolean constant true.
A constant literal expression.
assigns_clause_scalar_targett(const exprt &object_ptr, code_contractst &contract, messaget &log_parameter, const irep_idt &function_id)
bool is_function_call() const
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
This class represents an instruction in the GOTO intermediate representation.
const source_locationt & source_location() const
A base class for assigns clause targets.
const exprt & get_direct_pointer() const
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, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
assigns_clause_struct_targett(const exprt &object_ptr, code_contractst &contract, messaget &log_parameter, const irep_idt &function_id)
irep_idt name
The unique identifier.
instructionst::iterator targett
symbol_tablet & symbol_table
Verify and use annotated invariants and pre/post-conditions.
Replace expression or type symbols by an expression or type, respectively.
API to expression classes for 'mathematical' expressions.
Data structure for representing an arbitrary statement in a program.