Skip to content

Commit 0190a5a

Browse files
author
Remi Delmas
committed
write set inclusion checks on contract replacement
1 parent 01a1122 commit 0190a5a

File tree

11 files changed

+579
-228
lines changed

11 files changed

+579
-228
lines changed

‎src/ansi-c/library/cprover_dfcc.c‎

Lines changed: 384 additions & 91 deletions
Large diffs are not rendered by default.

‎src/goto-instrument/contracts/dfcc.cpp‎

Lines changed: 3 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -46,12 +46,6 @@ Author: Remi Delmas, delmarsd@amazon.com
4646
#include "memory_predicates.h"
4747
#include "utils.h"
4848

49-
/// True if 's1' contains 's2'.
50-
static bool string_starts_with(std::string s1, std::string s2)
51-
{
52-
return (s1.rfind(s2, 0) == 0);
53-
}
54-
5549
void dfcc(
5650
goto_modelt &goto_model,
5751
const std::string &harness_id,
@@ -219,9 +213,7 @@ void dfcct::partition_function_symbols(
219213
continue;
220214

221215
// is it a pure contract ?
222-
if(
223-
string_starts_with(id2string(sym_name), "contract::") &&
224-
symbol.is_property)
216+
if(symbol.is_property && (id2string(sym_name).rfind("contract::", 0) == 0))
225217
{
226218
contract_symbols.insert(sym_name);
227219
}
@@ -352,13 +344,13 @@ void dfcct::transform_goto_model(
352344
utils.create_initialize_function();
353345
}
354346

355-
/// Generate statics:
347+
/// Generates statics:
356348
/// ```
357349
/// static bool on_stack = false;
358350
/// static bool checked = false;
359351
/// ```
360352
///
361-
/// Generate instructions:
353+
/// Generates instructions:
362354
/// ```
363355
/// IF on_stack GOTO replace;
364356
/// ASSERT !checked "only a single top-level called allowed";

‎src/goto-instrument/contracts/dfcc_contract_handler.h‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,7 @@ class dfcc_contract_handlert
4444
const symbol_exprt &wrapper_write_set_symbol,
4545
goto_programt &dest) = 0;
4646

47-
/// Returns the size assigns clause of the given contract in number of CARs
47+
/// Returns the size assigns clause of the given contract in number of targets
4848
virtual const int
4949
get_assigns_clause_size(const irep_idt &contract_id) const = 0;
5050
};

‎src/goto-instrument/contracts/dfcc_instrument.cpp‎

Lines changed: 41 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ Author: Remi Delmas, delmarsd@amazon.com
66
77
\*******************************************************************/
88

9+
// TODO add property class on make_assertion
910
#include "dfcc_instrument.h"
1011
#include <goto-programs/goto_convert_class.h>
1112

@@ -130,17 +131,17 @@ void dfcc_instrumentt::instrument_function(const irep_idt &function_id)
130131

131132
function_cfg_infot cfg_info(goto_function);
132133

133-
const auto &dfcc_param = utils.add_parameter(
134+
const auto &write_set = utils.add_parameter(
134135
function_id,
135136
"__write_set_to_check",
136137
library.dfcc_type[dfcc_typet::SET_PTR]);
137138

138-
instrument_function_body(function_id, dfcc_param.symbol_expr(), cfg_info);
139+
instrument_function_body(function_id, write_set.symbol_expr(), cfg_info);
139140
}
140141

141142
void dfcc_instrumentt::instrument_function_body(
142143
const irep_idt &function_id,
143-
const symbol_exprt &dfcc_param,
144+
const symbol_exprt &write_set,
144145
cfg_infot &cfg_info)
145146
{
146147
auto &goto_function = goto_model.goto_functions.function_map.at(function_id);
@@ -160,7 +161,7 @@ void dfcc_instrumentt::instrument_function_body(
160161
// instrument the whole body
161162
instrument_instructions(
162163
function_id,
163-
dfcc_param,
164+
write_set,
164165
body,
165166
body.instructions.begin(),
166167
body.instructions.end(),
@@ -188,7 +189,7 @@ void dfcc_instrumentt::instrument_function_body(
188189

189190
void dfcc_instrumentt::instrument_instructions(
190191
const irep_idt &function_id,
191-
const symbol_exprt &dfcc_param,
192+
const symbol_exprt &write_set,
192193
goto_programt &goto_program,
193194
goto_programt::targett first_instruction,
194195
const goto_programt::targett &last_instruction, // excluding the last
@@ -222,25 +223,25 @@ void dfcc_instrumentt::instrument_instructions(
222223

223224
if(target->is_decl() && must_track_decl_or_dead(target, cfg_info))
224225
{
225-
instrument_decl(function_id, dfcc_param, target, goto_program, cfg_info);
226+
instrument_decl(function_id, write_set, target, goto_program, cfg_info);
226227
}
227228
if(target->is_dead() && must_track_decl_or_dead(target, cfg_info))
228229
{
229-
instrument_dead(function_id, dfcc_param, target, goto_program, cfg_info);
230+
instrument_dead(function_id, write_set, target, goto_program, cfg_info);
230231
}
231232
else if(target->is_assign())
232233
{
233234
instrument_assign(
234-
function_id, dfcc_param, target, goto_program, cfg_info);
235+
function_id, write_set, target, goto_program, cfg_info);
235236
}
236237
else if(target->is_function_call())
237238
{
238239
instrument_function_call(
239-
function_id, dfcc_param, target, goto_program, cfg_info);
240+
function_id, write_set, target, goto_program, cfg_info);
240241
}
241242
else if(target->is_other())
242243
{
243-
instrument_other(function_id, dfcc_param, target, goto_program, cfg_info);
244+
instrument_other(function_id, write_set, target, goto_program, cfg_info);
244245
}
245246
// else do nothing
246247
target++;
@@ -263,14 +264,14 @@ bool dfcc_instrumentt::must_track_decl_or_dead(
263264

264265
void dfcc_instrumentt::instrument_decl(
265266
const irep_idt &function_id,
266-
const symbol_exprt &dfcc_param,
267+
const symbol_exprt &write_set,
267268
goto_programt::targett &target,
268269
goto_programt &goto_program,
269270
cfg_infot &cfg_info)
270271
{
271272
// ```
272273
// DECL decl_symbol;
273-
// IF !__dfcc_param GOTO skip_target;
274+
// IF !__write_set GOTO skip_target;
274275
// CALL __CPROVER_assignable_obj_set_add(__stack_allocated, &decl_symbol);
275276
// skip_target: SKIP;
276277
// ```
@@ -279,11 +280,11 @@ void dfcc_instrumentt::instrument_decl(
279280
target++;
280281
goto_programt payload;
281282
auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
282-
utils.make_null_check_expr(dfcc_param)));
283+
utils.make_null_check_expr(write_set)));
283284

284285
payload.add(goto_programt::make_function_call(code_function_callt{
285286
library.dfcc_fun_symbol[dfcc_funt::SET_ADD_ALLOCATED].symbol_expr(),
286-
{dfcc_param, address_of_exprt(decl_symbol)}}));
287+
{write_set, address_of_exprt(decl_symbol)}}));
287288

288289
auto label_instruction = payload.add(goto_programt::make_skip());
289290
goto_instruction->complete_goto(label_instruction);
@@ -295,7 +296,7 @@ void dfcc_instrumentt::instrument_decl(
295296

296297
void dfcc_instrumentt::instrument_dead(
297298
const irep_idt &function_id,
298-
const symbol_exprt &dfcc_param,
299+
const symbol_exprt &write_set,
299300
goto_programt::targett &target,
300301
goto_programt &goto_program,
301302
cfg_infot &cfg_info)
@@ -311,11 +312,11 @@ void dfcc_instrumentt::instrument_dead(
311312
goto_programt payload;
312313

313314
auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
314-
utils.make_null_check_expr(dfcc_param)));
315+
utils.make_null_check_expr(write_set)));
315316

316317
payload.add(goto_programt::make_function_call(code_function_callt{
317318
library.dfcc_fun_symbol[dfcc_funt::SET_REMOVE_DEAD].symbol_expr(),
318-
{dfcc_param, address_of_exprt(decl_symbol)}}));
319+
{write_set, address_of_exprt(decl_symbol)}}));
319320

320321
auto label_instruction = payload.add(goto_programt::make_skip());
321322
goto_instruction->complete_goto(label_instruction);
@@ -387,7 +388,7 @@ bool dfcc_instrumentt::must_check_assign_lhs(
387388

388389
void dfcc_instrumentt::instrument_assign(
389390
const irep_idt &function_id,
390-
const symbol_exprt &dfcc_param,
391+
const symbol_exprt &write_set,
391392
goto_programt::targett &target,
392393
goto_programt &goto_program,
393394
cfg_infot &cfg_info)
@@ -414,8 +415,9 @@ void dfcc_instrumentt::instrument_assign(
414415
goto_programt payload;
415416

416417
auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
417-
utils.make_null_check_expr(dfcc_param)));
418+
utils.make_null_check_expr(write_set)));
418419

420+
// TODO use dfcc_utilst class
419421
auto &check_sym = get_fresh_aux_symbol(
420422
bool_typet(),
421423
id2string(function_id),
@@ -431,7 +433,7 @@ void dfcc_instrumentt::instrument_assign(
431433
payload.add(goto_programt::make_function_call(code_function_callt{
432434
check_var,
433435
library.dfcc_fun_symbol[dfcc_funt::SET_CHECK_ASSIGNMENT].symbol_expr(),
434-
{dfcc_param, lhs, utils.make_sizeof_expr(lhs)}}));
436+
{write_set, lhs, utils.make_sizeof_expr(lhs)}}));
435437

436438
// TODO add property class on assertion source_location
437439
payload.add(goto_programt::make_assertion(check_var));
@@ -460,11 +462,11 @@ void dfcc_instrumentt::instrument_assign(
460462
goto_programt payload;
461463

462464
auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
463-
utils.make_null_check_expr(dfcc_param)));
465+
utils.make_null_check_expr(write_set)));
464466

465467
payload.add(goto_programt::make_function_call(code_function_callt{
466468
library.dfcc_fun_symbol[dfcc_funt::SET_ADD_ALLOCATED].symbol_expr(),
467-
{dfcc_param, lhs}}));
469+
{write_set, lhs}}));
468470

469471
auto label_instruction = payload.add(goto_programt::make_skip());
470472
goto_instruction->complete_goto(label_instruction);
@@ -478,7 +480,7 @@ void dfcc_instrumentt::instrument_assign(
478480

479481
void dfcc_instrumentt::instrument_function_call(
480482
const irep_idt &function_id,
481-
const symbol_exprt &dfcc_param,
483+
const symbol_exprt &write_set,
482484
goto_programt::targett &target,
483485
goto_programt &goto_program,
484486
cfg_infot &cfg_info)
@@ -521,7 +523,7 @@ void dfcc_instrumentt::instrument_function_call(
521523
goto_programt payload;
522524

523525
auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
524-
utils.make_null_check_expr(dfcc_param)));
526+
utils.make_null_check_expr(write_set)));
525527

526528
auto &check_sym = get_fresh_aux_symbol(
527529
bool_typet(),
@@ -540,7 +542,7 @@ void dfcc_instrumentt::instrument_function_call(
540542
payload.add(goto_programt::make_function_call(code_function_callt{
541543
check_var,
542544
library.dfcc_fun_symbol[dfcc_funt::SET_CHECK_DEALLOCATE].symbol_expr(),
543-
{dfcc_param, ptr}}));
545+
{write_set, ptr}}));
544546

545547
// TODO add property class on assertion source_location
546548
payload.add(goto_programt::make_assertion(check_var));
@@ -549,7 +551,7 @@ void dfcc_instrumentt::instrument_function_call(
549551
payload.add(goto_programt::make_function_call(code_function_callt{
550552
library.dfcc_fun_symbol[dfcc_funt::SET_REMOVE_DEALLOCATED]
551553
.symbol_expr(),
552-
{dfcc_param, ptr}}));
554+
{write_set, ptr}}));
553555

554556
auto label_instruction = payload.add(goto_programt::make_skip());
555557
goto_instruction->complete_goto(label_instruction);
@@ -570,13 +572,13 @@ void dfcc_instrumentt::instrument_function_call(
570572
goto_programt payload;
571573

572574
auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
573-
utils.make_null_check_expr(dfcc_param)));
575+
utils.make_null_check_expr(write_set)));
574576

575577
const auto &lhs = target->call_lhs();
576578
target++;
577579
payload.add(goto_programt::make_function_call(code_function_callt{
578580
library.dfcc_fun_symbol[dfcc_funt::SET_ADD_ALLOCATED].symbol_expr(),
579-
{dfcc_param, lhs}}));
581+
{write_set, lhs}}));
580582

581583
auto label_instruction = payload.add(goto_programt::make_skip());
582584
goto_instruction->complete_goto(label_instruction);
@@ -595,21 +597,21 @@ void dfcc_instrumentt::instrument_function_call(
595597
// a user defined or library function symbol
596598
// propagate dfcc parameters
597599
auto &arguments = target->call_arguments();
598-
arguments.emplace_back(dfcc_param);
600+
arguments.emplace_back(write_set);
599601
}
600602
}
601603
else
602604
{
603605
// a function pointer expression
604606
// propagate dfcc parameters
605607
auto &arguments = target->call_arguments();
606-
arguments.emplace_back(dfcc_param);
608+
arguments.emplace_back(write_set);
607609
}
608610
}
609611

610612
void dfcc_instrumentt::instrument_other(
611613
const irep_idt &function_id,
612-
const symbol_exprt &dfcc_param,
614+
const symbol_exprt &write_set,
613615
goto_programt::targett &target,
614616
goto_programt &goto_program,
615617
cfg_infot &cfg_info)
@@ -631,7 +633,7 @@ void dfcc_instrumentt::instrument_other(
631633
goto_programt payload;
632634

633635
auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
634-
utils.make_null_check_expr(dfcc_param)));
636+
utils.make_null_check_expr(write_set)));
635637

636638
auto &check_sym = get_fresh_aux_symbol(
637639
bool_typet(),
@@ -650,7 +652,7 @@ void dfcc_instrumentt::instrument_other(
650652
payload.add(goto_programt::make_function_call(code_function_callt{
651653
check_var,
652654
library.dfcc_fun_symbol[dfcc_funt::SET_CHECK_ARRAY_SET].symbol_expr(),
653-
{dfcc_param, dest}}));
655+
{write_set, dest}}));
654656

655657
// TODO add property class on assertion source_location
656658
payload.add(goto_programt::make_assertion(check_var));
@@ -677,7 +679,7 @@ void dfcc_instrumentt::instrument_other(
677679
goto_programt payload;
678680

679681
auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
680-
utils.make_null_check_expr(dfcc_param)));
682+
utils.make_null_check_expr(write_set)));
681683

682684
auto &check_sym = get_fresh_aux_symbol(
683685
bool_typet(),
@@ -696,7 +698,7 @@ void dfcc_instrumentt::instrument_other(
696698
payload.add(goto_programt::make_function_call(code_function_callt{
697699
check_var,
698700
library.dfcc_fun_symbol[dfcc_funt::SET_CHECK_ARRAY_COPY].symbol_expr(),
699-
{dfcc_param, dest}}));
701+
{write_set, dest}}));
700702

701703
// TODO add property class on assertion source_location
702704
payload.add(goto_programt::make_assertion(check_var));
@@ -723,7 +725,7 @@ void dfcc_instrumentt::instrument_other(
723725
goto_programt payload;
724726

725727
auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
726-
utils.make_null_check_expr(dfcc_param)));
728+
utils.make_null_check_expr(write_set)));
727729

728730
auto &check_sym = get_fresh_aux_symbol(
729731
bool_typet(),
@@ -743,7 +745,7 @@ void dfcc_instrumentt::instrument_other(
743745
payload.add(goto_programt::make_function_call(code_function_callt{
744746
check_var,
745747
library.dfcc_fun_symbol[dfcc_funt::SET_CHECK_ARRAY_REPLACE].symbol_expr(),
746-
{dfcc_param, dest, src}}));
748+
{write_set, dest, src}}));
747749

748750
// TODO add property class on assertion source_location
749751
payload.add(goto_programt::make_assertion(check_var));
@@ -769,7 +771,7 @@ void dfcc_instrumentt::instrument_other(
769771
goto_programt payload;
770772

771773
auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
772-
utils.make_null_check_expr(dfcc_param)));
774+
utils.make_null_check_expr(write_set)));
773775

774776
auto &check_sym = get_fresh_aux_symbol(
775777
bool_typet(),
@@ -788,7 +790,7 @@ void dfcc_instrumentt::instrument_other(
788790
payload.add(goto_programt::make_function_call(code_function_callt{
789791
check_var,
790792
library.dfcc_fun_symbol[dfcc_funt::SET_CHECK_HAVOC_OBJECT].symbol_expr(),
791-
{dfcc_param, ptr}}));
793+
{write_set, ptr}}));
792794

793795
// TODO add property class on assertion source_location
794796
payload.add(goto_programt::make_assertion(check_var));

0 commit comments

Comments
 (0)