Skip to content

Commit cec18ba

Browse files
committed
remove repeated inclusion checks in nested loops
This commit introduces a new internal pragma, called `contracts:disable:assigns-check`, and annotates statements that have already been instrumented with inclusion checks to avoid instrumenting them again.
1 parent 49a75bf commit cec18ba

File tree

4 files changed

+70
-8
lines changed

4 files changed

+70
-8
lines changed

src/goto-instrument/contracts/assigns.cpp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -117,6 +117,10 @@ assigns_clauset::conditional_address_ranget::generate_snapshot_instructions()
117117
location));
118118

119119
instructions.destructive_append(skip_program);
120+
121+
// The assignments above are only performed on locally defined temporaries
122+
// and need not be checked for inclusion in the enclosing scope's write set.
123+
add_pragma_disable_assigns_check(instructions);
120124
return instructions;
121125
}
122126

src/goto-instrument/contracts/contracts.cpp

Lines changed: 35 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -141,9 +141,6 @@ void code_contractst::check_apply_loop_contracts(
141141
generated_code,
142142
ID_loop_entry);
143143

144-
// Create 'loop_entry' history variables
145-
insert_before_swap_and_advance(goto_function.body, loop_head, generated_code);
146-
147144
// Generate: assert(invariant) just before the loop
148145
// We use a block scope to create a temporary assertion,
149146
// and immediately convert it to goto instructions.
@@ -155,6 +152,14 @@ void code_contractst::check_apply_loop_contracts(
155152
"Check loop invariant before entry");
156153
}
157154

155+
// Add 'loop_entry' history variables and base case assertion.
156+
// These variables are local and thus
157+
// need not be checked against the enclosing scope's write set.
158+
insert_before_swap_and_advance(
159+
goto_function.body,
160+
loop_head,
161+
add_pragma_disable_assigns_check(generated_code));
162+
158163
// havoc the variables that may be modified
159164
modifiest modifies;
160165
if(assigns.is_nil())
@@ -177,7 +182,8 @@ void code_contractst::check_apply_loop_contracts(
177182
for(const auto &target : assigns.operands())
178183
modifies.insert(target);
179184

180-
// create snapshots of the CARs -- must be done before havocing
185+
// Create snapshots of write set CARs.
186+
// This must be done before havocing the write set.
181187
for(const auto &car : loop_assigns.get_write_set())
182188
{
183189
auto snapshot_instructions = car.generate_snapshot_instructions();
@@ -189,7 +195,17 @@ void code_contractst::check_apply_loop_contracts(
189195
havoc_assigns_targetst havoc_gen(modifies, ns);
190196
havoc_gen.append_full_havoc_code(
191197
loop_head->source_location(), generated_code);
192-
insert_before_swap_and_advance(goto_function.body, loop_head, generated_code);
198+
199+
// Add the havocing code, but only check against the enclosing scope's
200+
// write set if it was manually specified.
201+
if(assigns.is_nil())
202+
insert_before_swap_and_advance(
203+
goto_function.body,
204+
loop_head,
205+
add_pragma_disable_assigns_check(generated_code));
206+
else
207+
insert_before_swap_and_advance(
208+
goto_function.body, loop_head, generated_code);
193209

194210
// Generate: assume(invariant) just after havocing
195211
// We use a block scope to create a temporary assumption,
@@ -744,7 +760,6 @@ void code_contractst::instrument_assign_statement(
744760
instruction_it->is_assign(),
745761
"The first instruction of instrument_assign_statement should always be"
746762
" an assignment");
747-
748763
add_inclusion_check(
749764
program, assigns_clause, instruction_it, instruction_it->assign_lhs());
750765
}
@@ -834,7 +849,9 @@ void code_contractst::instrument_call_statement(
834849

835850
alias_checking_instructions.destructive_append(skip_program);
836851
insert_before_swap_and_advance(
837-
body, instruction_it, alias_checking_instructions);
852+
body,
853+
instruction_it,
854+
add_pragma_disable_assigns_check(alias_checking_instructions));
838855

839856
// move past the call and then insert the invalidation instructions
840857
instruction_it++;
@@ -866,7 +883,9 @@ void code_contractst::instrument_call_statement(
866883

867884
invalidation_instructions.destructive_append(skip_program);
868885
insert_before_swap_and_advance(
869-
body, instruction_it, invalidation_instructions);
886+
body,
887+
instruction_it,
888+
add_pragma_disable_assigns_check(invalidation_instructions));
870889

871890
instruction_it--;
872891
}
@@ -1003,6 +1022,14 @@ void code_contractst::check_frame_conditions(
10031022

10041023
for(; instruction_it != instruction_end; ++instruction_it)
10051024
{
1025+
const auto &pragmas = instruction_it->source_location().get_pragmas();
1026+
if(pragmas.find(CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK) != pragmas.end())
1027+
continue;
1028+
1029+
// Do not instrument this instruction again in the future,
1030+
// since we are going to instrument it now below.
1031+
add_pragma_disable_assigns_check(*instruction_it);
1032+
10061033
if(instruction_it->is_decl())
10071034
{
10081035
// grab the declared symbol

src/goto-instrument/contracts/utils.cpp

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,21 @@ Date: September 2021
1414
#include <util/pointer_expr.h>
1515
#include <util/pointer_predicates.h>
1616

17+
goto_programt::instructiont &
18+
add_pragma_disable_assigns_check(goto_programt::instructiont &instr)
19+
{
20+
instr.source_location_nonconst().add_pragma(
21+
CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK);
22+
return instr;
23+
}
24+
25+
goto_programt &add_pragma_disable_assigns_check(goto_programt &prog)
26+
{
27+
Forall_goto_program_instructions(it, prog)
28+
add_pragma_disable_assigns_check(*it);
29+
return prog;
30+
}
31+
1732
static void append_safe_havoc_code_for_expr(
1833
const source_locationt location,
1934
const namespacet &ns,

src/goto-instrument/contracts/utils.h

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,8 @@ Date: September 2021
1717

1818
#include <goto-programs/goto_model.h>
1919

20+
#define CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK "contracts:disable:assigns-check"
21+
2022
/// \brief A class that overrides the low-level havocing functions in the base
2123
/// utility class, to havoc only when expressions point to valid memory,
2224
/// i.e. if all dereferences within an expression are valid
@@ -42,6 +44,20 @@ class havoc_if_validt : public havoc_utilst
4244
const namespacet &ns;
4345
};
4446

47+
/// \brief Adds a pragma on a GOTO instruction to disable inclusion checking.
48+
///
49+
/// \param instr: A mutable reference to the GOTO instruction.
50+
/// \return The same reference after mutation (i.e., adding the pragma).
51+
goto_programt::instructiont &
52+
add_pragma_disable_assigns_check(goto_programt::instructiont &instr);
53+
54+
/// \brief Adds pragmas on all instructions in a GOTO program
55+
/// to disable inclusion checking on them.
56+
///
57+
/// \param prog: A mutable reference to the GOTO program.
58+
/// \return The same reference after mutation (i.e., adding the pragmas).
59+
goto_programt &add_pragma_disable_assigns_check(goto_programt &prog);
60+
4561
/// \brief Generate a validity check over all dereferences in an expression
4662
///
4763
/// This function generates a formula:

0 commit comments

Comments
 (0)