Skip to content

Commit 251a1c1

Browse files
peterschrammelpeterschrammel
authored
Merge pull request #328 from tautschnig/check-options
Cleanup of *-check options handling, refined options for SV-COMP
2 parents c84f8a6 + 8a164ad commit 251a1c1

15 files changed

+117
-374
lines changed

‎src/aa-symex/symex_parseoptions.cpp‎

Lines changed: 3 additions & 50 deletions
Original file line numberDiff line numberDiff line change
@@ -28,8 +28,6 @@ Author: Daniel Kroening, [email protected]
2828
#include <goto-programs/goto_inline.h>
2929
#include <goto-programs/xml_goto_trace.h>
3030

31-
#include <analyses/goto_check.h>
32-
3331
#include <langapi/mode.h>
3432

3533
#include <cbmc/version.h>
@@ -112,47 +110,8 @@ void symex_parseoptionst::get_command_line_options(optionst &options)
112110
if(cmdline.isset("unwindset"))
113111
options.set_option("unwindset", cmdline.getval("unwindset"));
114112

115-
// check array bounds
116-
if(cmdline.isset("bounds-check"))
117-
options.set_option("bounds-check", true);
118-
else
119-
options.set_option("bounds-check", false);
120-
121-
// check division by zero
122-
if(cmdline.isset("div-by-zero-check"))
123-
options.set_option("div-by-zero-check", true);
124-
else
125-
options.set_option("div-by-zero-check", false);
126-
127-
// check overflow/underflow
128-
if(cmdline.isset("signed-overflow-check"))
129-
options.set_option("signed-overflow-check", true);
130-
else
131-
options.set_option("signed-overflow-check", false);
132-
133-
// check overflow/underflow
134-
if(cmdline.isset("unsigned-overflow-check"))
135-
options.set_option("unsigned-overflow-check", true);
136-
else
137-
options.set_option("unsigned-overflow-check", false);
138-
139-
// check for NaN (not a number)
140-
if(cmdline.isset("nan-check"))
141-
options.set_option("nan-check", true);
142-
else
143-
options.set_option("nan-check", false);
144-
145-
// check pointers
146-
if(cmdline.isset("pointer-check"))
147-
options.set_option("pointer-check", true);
148-
else
149-
options.set_option("pointer-check", false);
150-
151-
// check for memory leaks
152-
if(cmdline.isset("memory-leak-check"))
153-
options.set_option("memory-leak-check", true);
154-
else
155-
options.set_option("memory-leak-check", false);
113+
// all checks supported by goto_check
114+
GOTO_CHECK_PARSE_OPTIONS(cmdline, options);
156115

157116
// check assertions
158117
if(cmdline.isset("no-assertions"))
@@ -811,13 +770,7 @@ void symex_parseoptionst::help()
811770
" --round-to-zero IEEE floating point rounding mode\n"
812771
"\n"
813772
"Program instrumentation options:\n"
814-
" --bounds-check enable array bounds checks\n"
815-
" --div-by-zero-check enable division by zero checks\n"
816-
" --pointer-check enable pointer checks\n"
817-
" --memory-leak-check enable memory leak checks\n"
818-
" --signed-overflow-check enable arithmetic over- and underflow checks\n"
819-
" --unsigned-overflow-check enable arithmetic over- and underflow checks\n"
820-
" --nan-check check floating-point for NaN\n"
773+
GOTO_CHECK_HELP
821774
" --show-properties show the properties\n"
822775
" --no-assertions ignore user assertions\n"
823776
" --no-assumptions ignore user assumptions\n"

‎src/aa-symex/symex_parseoptions.h‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]
1414

1515
#include <langapi/language_ui.h>
1616

17+
#include <analyses/goto_check.h>
18+
1719
#include "path_search.h"
1820

1921
class goto_functionst;
@@ -23,8 +25,7 @@ class optionst;
2325
"(function):" \
2426
"D:I:" \
2527
"(depth):(context-bound):(unwind):" \
26-
"(bounds-check)(pointer-check)(div-by-zero-check)(memory-leak-check)" \
27-
"(signed-overflow-check)(unsigned-overflow-check)(nan-check)" \
28+
GOTO_CHECK_OPTIONS \
2829
"(no-assertions)(no-assumptions)" \
2930
"(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
3031
"(little-endian)(big-endian)" \

‎src/analyses/goto_check.cpp‎

Lines changed: 48 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
2020
#include <util/base_type.h>
2121
#include <util/pointer_predicates.h>
2222
#include <util/cprover_prefix.h>
23+
#include <util/options.h>
2324

2425
#include "local_bitvector_analysis.h"
2526
#include "goto_check.h"
@@ -39,6 +40,8 @@ class goto_checkt
3940
enable_div_by_zero_check=_options.get_bool_option("div-by-zero-check");
4041
enable_signed_overflow_check=_options.get_bool_option("signed-overflow-check");
4142
enable_unsigned_overflow_check=_options.get_bool_option("unsigned-overflow-check");
43+
enable_pointer_overflow_check=_options.get_bool_option("pointer-overflow-check");
44+
enable_conversion_check=_options.get_bool_option("conversion-check");
4245
enable_undefined_shift_check=_options.get_bool_option("undefined-shift-check");
4346
enable_float_overflow_check=_options.get_bool_option("float-overflow-check");
4447
enable_simplify=_options.get_bool_option("simplify");
@@ -72,6 +75,7 @@ class goto_checkt
7275
void pointer_overflow_check(const exprt &expr, const guardt &guard);
7376
void pointer_validity_check(const dereference_exprt &expr, const guardt &guard);
7477
void integer_overflow_check(const exprt &expr, const guardt &guard);
78+
void conversion_check(const exprt &expr, const guardt &guard);
7579
void float_overflow_check(const exprt &expr, const guardt &guard);
7680
void nan_check(const exprt &expr, const guardt &guard);
7781

@@ -102,6 +106,8 @@ class goto_checkt
102106
bool enable_div_by_zero_check;
103107
bool enable_signed_overflow_check;
104108
bool enable_unsigned_overflow_check;
109+
bool enable_pointer_overflow_check;
110+
bool enable_conversion_check;
105111
bool enable_undefined_shift_check;
106112
bool enable_float_overflow_check;
107113
bool enable_simplify;
@@ -302,7 +308,7 @@ void goto_checkt::mod_by_zero_check(
302308

303309
/*******************************************************************\
304310
305-
Function: goto_checkt::integer_overflow_check
311+
Function: goto_checkt::conversion_check
306312
307313
Inputs:
308314
@@ -312,25 +318,20 @@ Function: goto_checkt::integer_overflow_check
312318
313319
\*******************************************************************/
314320

315-
void goto_checkt::integer_overflow_check(
321+
void goto_checkt::conversion_check(
316322
const exprt &expr,
317323
const guardt &guard)
318324
{
319-
if(!enable_signed_overflow_check &&
320-
!enable_unsigned_overflow_check)
325+
if(!enable_conversion_check)
321326
return;
322327

323328
// First, check type.
324329
const typet &type=ns.follow(expr.type());
325330

326-
if(type.id()==ID_signedbv && !enable_signed_overflow_check)
327-
return;
328-
329-
if(type.id()==ID_unsignedbv && !enable_unsigned_overflow_check)
331+
if(type.id()!=ID_signedbv &&
332+
type.id()!=ID_unsignedbv)
330333
return;
331334

332-
// add overflow subgoal
333-
334335
if(expr.id()==ID_typecast)
335336
{
336337
// conversion to signed int may overflow
@@ -490,10 +491,41 @@ void goto_checkt::integer_overflow_check(
490491
guard);
491492
}
492493
}
494+
}
495+
}
496+
497+
/*******************************************************************\
498+
499+
Function: goto_checkt::integer_overflow_check
500+
501+
Inputs:
502+
503+
Outputs:
504+
505+
Purpose:
506+
507+
\*******************************************************************/
493508

509+
void goto_checkt::integer_overflow_check(
510+
const exprt &expr,
511+
const guardt &guard)
512+
{
513+
if(!enable_signed_overflow_check &&
514+
!enable_unsigned_overflow_check)
494515
return;
495-
}
496-
else if(expr.id()==ID_div)
516+
517+
// First, check type.
518+
const typet &type=ns.follow(expr.type());
519+
520+
if(type.id()==ID_signedbv && !enable_signed_overflow_check)
521+
return;
522+
523+
if(type.id()==ID_unsignedbv && !enable_unsigned_overflow_check)
524+
return;
525+
526+
// add overflow subgoal
527+
528+
if(expr.id()==ID_div)
497529
{
498530
assert(expr.operands().size()==2);
499531

@@ -898,7 +930,7 @@ void goto_checkt::pointer_overflow_check(
898930
const exprt &expr,
899931
const guardt &guard)
900932
{
901-
if(!enable_pointer_check)
933+
if(!enable_pointer_overflow_check)
902934
return;
903935

904936
if(expr.id()==ID_plus ||
@@ -1429,8 +1461,7 @@ void goto_checkt::check_rec(
14291461
}
14301462
else if(expr.id()==ID_plus || expr.id()==ID_minus ||
14311463
expr.id()==ID_mult ||
1432-
expr.id()==ID_unary_minus ||
1433-
expr.id()==ID_typecast)
1464+
expr.id()==ID_unary_minus)
14341465
{
14351466
if(expr.type().id()==ID_signedbv ||
14361467
expr.type().id()==ID_unsignedbv)
@@ -1451,6 +1482,8 @@ void goto_checkt::check_rec(
14511482
pointer_overflow_check(expr, guard);
14521483
}
14531484
}
1485+
else if(expr.id()==ID_typecast)
1486+
conversion_check(expr, guard);
14541487
else if(expr.id()==ID_le || expr.id()==ID_lt ||
14551488
expr.id()==ID_ge || expr.id()==ID_gt)
14561489
pointer_rel_check(expr, guard);

‎src/analyses/goto_check.h‎

Lines changed: 35 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,12 +9,12 @@ Author: Daniel Kroening, [email protected]
99
#ifndef CPROVER_GOTO_PROGRAMS_GOTO_CHECK_H
1010
#define CPROVER_GOTO_PROGRAMS_GOTO_CHECK_H
1111

12-
#include <util/namespace.h>
13-
#include <util/options.h>
14-
1512
#include <goto-programs/goto_functions.h>
1613
#include <goto-programs/goto_model.h>
1714

15+
class namespacet;
16+
class optionst;
17+
1818
void goto_check(
1919
const namespacet &ns,
2020
const optionst &options,
@@ -29,4 +29,36 @@ void goto_check(
2929
const optionst &options,
3030
goto_modelt &goto_model);
3131

32+
#define GOTO_CHECK_OPTIONS \
33+
"(bounds-check)(pointer-check)(memory-leak-check)" \
34+
"(div-by-zero-check)(signed-overflow-check)(unsigned-overflow-check)" \
35+
"(pointer-overflow-check)(conversion-check)(undefined-shift-check)" \
36+
"(float-overflow-check)(nan-check)"
37+
38+
#define GOTO_CHECK_HELP \
39+
" --bounds-check enable array bounds checks\n" \
40+
" --pointer-check enable pointer checks\n" \
41+
" --memory-leak-check enable memory leak checks\n" \
42+
" --div-by-zero-check enable division by zero checks\n" \
43+
" --signed-overflow-check enable signed arithmetic over- and underflow checks\n" \
44+
" --unsigned-overflow-check enable arithmetic over- and underflow checks\n" \
45+
" --pointer-overflow-check enable pointer arithmetic over- and underflow checks\n" \
46+
" --conversion-check check whether values can be represented after type cast\n" \
47+
" --undefined-shift-check check shift greater than bit-width\n" \
48+
" --float-overflow-check check floating-point for +/-Inf\n" \
49+
" --nan-check check floating-point for NaN\n" \
50+
51+
#define GOTO_CHECK_PARSE_OPTIONS(cmdline, options) \
52+
options.set_option("bounds-check", cmdline.isset("bounds-check")); \
53+
options.set_option("pointer-check", cmdline.isset("pointer-check")); \
54+
options.set_option("memory-leak-check", cmdline.isset("memory-leak-check")); \
55+
options.set_option("div-by-zero-check", cmdline.isset("div-by-zero-check")); \
56+
options.set_option("signed-overflow-check", cmdline.isset("signed-overflow-check")); \
57+
options.set_option("unsigned-overflow-check", cmdline.isset("unsigned-overflow-check")); \
58+
options.set_option("pointer-overflow-check", cmdline.isset("pointer-overflow-check")); \
59+
options.set_option("conversion-check", cmdline.isset("conversion-check")); \
60+
options.set_option("undefined-shift-check", cmdline.isset("undefined-shift-check")); \
61+
options.set_option("float-overflow-check", cmdline.isset("float-overflow-check")); \
62+
options.set_option("nan-check", cmdline.isset("nan-check"))
63+
3264
#endif

‎src/cbmc/cbmc_parse_options.cpp‎

Lines changed: 3 additions & 57 deletions
Original file line numberDiff line numberDiff line change
@@ -46,8 +46,6 @@ Author: Daniel Kroening, [email protected]
4646

4747
#include <pointer-analysis/add_failed_symbols.h>
4848

49-
#include <analyses/goto_check.h>
50-
5149
#include <langapi/mode.h>
5250

5351
#include "cbmc_solvers.h"
@@ -218,53 +216,8 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
218216
else
219217
options.set_option("propagation", true);
220218

221-
// check array bounds
222-
if(cmdline.isset("bounds-check"))
223-
options.set_option("bounds-check", true);
224-
else
225-
options.set_option("bounds-check", false);
226-
227-
// check division by zero
228-
if(cmdline.isset("div-by-zero-check"))
229-
options.set_option("div-by-zero-check", true);
230-
else
231-
options.set_option("div-by-zero-check", false);
232-
233-
// check overflow/underflow
234-
if(cmdline.isset("signed-overflow-check"))
235-
options.set_option("signed-overflow-check", true);
236-
else
237-
options.set_option("signed-overflow-check", false);
238-
239-
// check overflow/underflow
240-
if(cmdline.isset("unsigned-overflow-check"))
241-
options.set_option("unsigned-overflow-check", true);
242-
else
243-
options.set_option("unsigned-overflow-check", false);
244-
245-
// check overflow/underflow
246-
if(cmdline.isset("float-overflow-check"))
247-
options.set_option("float-overflow-check", true);
248-
else
249-
options.set_option("float-overflow-check", false);
250-
251-
// check for NaN (not a number)
252-
if(cmdline.isset("nan-check"))
253-
options.set_option("nan-check", true);
254-
else
255-
options.set_option("nan-check", false);
256-
257-
// check pointers
258-
if(cmdline.isset("pointer-check"))
259-
options.set_option("pointer-check", true);
260-
else
261-
options.set_option("pointer-check", false);
262-
263-
// check for memory leaks
264-
if(cmdline.isset("memory-leak-check"))
265-
options.set_option("memory-leak-check", true);
266-
else
267-
options.set_option("memory-leak-check", false);
219+
// all checks supported by goto_check
220+
GOTO_CHECK_PARSE_OPTIONS(cmdline, options);
268221

269222
// check assertions
270223
if(cmdline.isset("no-assertions"))
@@ -1141,14 +1094,7 @@ void cbmc_parse_optionst::help()
11411094
" --show-goto-functions show goto program\n"
11421095
"\n"
11431096
"Program instrumentation options:\n"
1144-
" --bounds-check enable array bounds checks\n"
1145-
" --div-by-zero-check enable division by zero checks\n"
1146-
" --pointer-check enable pointer checks\n"
1147-
" --memory-leak-check enable memory leak checks\n"
1148-
" --signed-overflow-check enable arithmetic over- and underflow checks\n"
1149-
" --unsigned-overflow-check enable arithmetic over- and underflow checks\n"
1150-
" --float-overflow-check check floating-point for +/-Inf\n"
1151-
" --nan-check check floating-point for NaN\n"
1097+
GOTO_CHECK_HELP
11521098
" --no-assertions ignore user assertions\n"
11531099
" --no-assumptions ignore user assumptions\n"
11541100
" --error-label label check that label is unreachable\n"

‎src/cbmc/cbmc_parse_options.h‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]
1414

1515
#include <langapi/language_ui.h>
1616

17+
#include <analyses/goto_check.h>
18+
1719
#include "xml_interface.h"
1820

1921
class bmct;
@@ -28,8 +30,7 @@ class optionst;
2830
"D:I:(c89)(c99)(c11)(cpp89)(cpp99)(cpp11)" \
2931
"(classpath):(cp):(main-class):" \
3032
"(depth):(partial-loops)(no-unwinding-assertions)(unwinding-assertions)" \
31-
"(bounds-check)(pointer-check)(div-by-zero-check)(memory-leak-check)" \
32-
"(signed-overflow-check)(unsigned-overflow-check)(float-overflow-check)(nan-check)" \
33+
GOTO_CHECK_OPTIONS \
3334
"(no-assertions)(no-assumptions)" \
3435
"(xml-ui)(xml-interface)(json-ui)" \
3536
"(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \

0 commit comments

Comments
 (0)