From d02525737a36392ad155e08a5e34dd50d680e8dc Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Wed, 22 Apr 2020 15:07:57 +0100 Subject: [PATCH] Feature to verify that pointers used in pointer primitives are valid or null --- .../cbmc/pointer-primitive-check-01/main.c | 28 ++++++++ .../cbmc/pointer-primitive-check-01/test.desc | 16 +++++ .../cbmc/pointer-primitive-check-02/main.c | 11 +++ .../cbmc/pointer-primitive-check-02/test.desc | 9 +++ .../cbmc/pointer-primitive-check-03/main.c | 40 +++++++++++ .../cbmc/pointer-primitive-check-03/test.desc | 18 +++++ .../cbmc/pointer-primitive-check-04/main.c | 6 ++ .../cbmc/pointer-primitive-check-04/test.desc | 12 ++++ src/analyses/goto_check.cpp | 72 ++++++++++++++++++- src/analyses/goto_check.h | 9 ++- 10 files changed, 217 insertions(+), 4 deletions(-) create mode 100644 regression/cbmc/pointer-primitive-check-01/main.c create mode 100644 regression/cbmc/pointer-primitive-check-01/test.desc create mode 100644 regression/cbmc/pointer-primitive-check-02/main.c create mode 100644 regression/cbmc/pointer-primitive-check-02/test.desc create mode 100644 regression/cbmc/pointer-primitive-check-03/main.c create mode 100644 regression/cbmc/pointer-primitive-check-03/test.desc create mode 100644 regression/cbmc/pointer-primitive-check-04/main.c create mode 100644 regression/cbmc/pointer-primitive-check-04/test.desc diff --git a/regression/cbmc/pointer-primitive-check-01/main.c b/regression/cbmc/pointer-primitive-check-01/main.c new file mode 100644 index 00000000000..4aa5419b48f --- /dev/null +++ b/regression/cbmc/pointer-primitive-check-01/main.c @@ -0,0 +1,28 @@ + +void main() +{ + // we need a new variable for each check, as goto_checkt removes redundant + // assertions, and if we would use the same variable all pointer primitive + // assertions would look the same + + char *p1; + __CPROVER_same_object(p1, p1); + + char *p2; + __CPROVER_POINTER_OFFSET(p2); + + char *p3; + __CPROVER_POINTER_OBJECT(p3); + + char *p4; + __CPROVER_OBJECT_SIZE(p4); + + char *p5; + __CPROVER_r_ok(p5, 1); + + char *p6; + __CPROVER_w_ok(p6, 1); + + char *p7; + __CPROVER_DYNAMIC_OBJECT(p7); +} diff --git a/regression/cbmc/pointer-primitive-check-01/test.desc b/regression/cbmc/pointer-primitive-check-01/test.desc new file mode 100644 index 00000000000..34e6bd3c4b0 --- /dev/null +++ b/regression/cbmc/pointer-primitive-check-01/test.desc @@ -0,0 +1,16 @@ +CORE +main.c +--pointer-primitive-check +^EXIT=10$ +^SIGNAL=0$ +\[main.pointer_primitives.1\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE +\[main.pointer_primitives.2\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OFFSET.*: FAILURE +\[main.pointer_primitives.3\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE +\[main.pointer_primitives.4\] line \d+ pointer in pointer primitive is neither null nor valid in OBJECT_SIZE.*: FAILURE +\[main.pointer_primitives.5\] line \d+ pointer in pointer primitive is neither null nor valid in R_OK.*: FAILURE +\[main.pointer_primitives.6\] line \d+ pointer in pointer primitive is neither null nor valid in W_OK.*: FAILURE +\*\* 7 of \d+ failed +-- +^warning: ignoring +-- +Verifies that checks are added for all pointer primitives diff --git a/regression/cbmc/pointer-primitive-check-02/main.c b/regression/cbmc/pointer-primitive-check-02/main.c new file mode 100644 index 00000000000..dfe35182bed --- /dev/null +++ b/regression/cbmc/pointer-primitive-check-02/main.c @@ -0,0 +1,11 @@ +#include + +char *p1; + +void main() +{ + __CPROVER_POINTER_OBJECT(p1); + + char *p2 = NULL; + __CPROVER_POINTER_OBJECT(p2); +} diff --git a/regression/cbmc/pointer-primitive-check-02/test.desc b/regression/cbmc/pointer-primitive-check-02/test.desc new file mode 100644 index 00000000000..315e2d255c7 --- /dev/null +++ b/regression/cbmc/pointer-primitive-check-02/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--pointer-primitive-check +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +Verifies that a null pointer does not fail the pointer primitives check diff --git a/regression/cbmc/pointer-primitive-check-03/main.c b/regression/cbmc/pointer-primitive-check-03/main.c new file mode 100644 index 00000000000..54d135047da --- /dev/null +++ b/regression/cbmc/pointer-primitive-check-03/main.c @@ -0,0 +1,40 @@ +#include + +void main() +{ + // uninitialized pointer + char *p1; + __CPROVER_POINTER_OBJECT(p1); + + // special value of invalid pointer + char *p2 = (size_t)1 << (sizeof(char *) * 8 - 8); + __CPROVER_POINTER_OBJECT(p2); + + // pointer object 123, offset 123, not pointing to valid memory + char *p3 = ((size_t)123 << (sizeof(char *) * 8 - 8)) | 123; + __CPROVER_POINTER_OBJECT(p3); + + // negative offset + char *p4 = malloc(1); + p4 -= 1; + __CPROVER_POINTER_OBJECT(p4); + + // offset out of bounds + char *p5 = malloc(10); + p5 += 10; + __CPROVER_POINTER_OBJECT(p5); + + // dead + char *p6; + { + char c; + p6 = &c; + } + __CPROVER_POINTER_OBJECT(p6); + *p6; + + // deallocated + char *p7 = malloc(1); + free(p7); + __CPROVER_POINTER_OBJECT(p7); +} diff --git a/regression/cbmc/pointer-primitive-check-03/test.desc b/regression/cbmc/pointer-primitive-check-03/test.desc new file mode 100644 index 00000000000..fc848d3338f --- /dev/null +++ b/regression/cbmc/pointer-primitive-check-03/test.desc @@ -0,0 +1,18 @@ +CORE +main.c +--pointer-primitive-check +^EXIT=10$ +^SIGNAL=0$ +\[main.pointer_primitives.1\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE +\[main.pointer_primitives.2\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE +\[main.pointer_primitives.3\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE +\[main.pointer_primitives.4\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE +\[main.pointer_primitives.5\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE +\[main.pointer_primitives.6\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE +\[main.pointer_primitives.7\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE +\*\* 7 of \d+ failed +-- +^warning: ignoring +-- +Verifies that the pointer primitives check fails for the various forms of +invalid pointers diff --git a/regression/cbmc/pointer-primitive-check-04/main.c b/regression/cbmc/pointer-primitive-check-04/main.c new file mode 100644 index 00000000000..8031c6e830e --- /dev/null +++ b/regression/cbmc/pointer-primitive-check-04/main.c @@ -0,0 +1,6 @@ + +void main() +{ + char *p; + __CPROVER_assume(__CPROVER_r_ok(p, 1)); +} diff --git a/regression/cbmc/pointer-primitive-check-04/test.desc b/regression/cbmc/pointer-primitive-check-04/test.desc new file mode 100644 index 00000000000..3907f8f8aa5 --- /dev/null +++ b/regression/cbmc/pointer-primitive-check-04/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--pointer-primitive-check +^EXIT=10$ +^SIGNAL=0$ +\[main.pointer_primitives.1\] line \d+ pointer in pointer primitive is neither null nor valid in R_OK.*: FAILURE +\*\* 1 of \d+ failed +-- +^warning: ignoring +-- +Verifies that the check fails for a primitive in an assume that uses an +uninitialized pointer diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 4fff0ca80dd..8166485725f 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -72,6 +72,8 @@ class goto_checkt enable_built_in_assertions=_options.get_bool_option("built-in-assertions"); enable_assumptions=_options.get_bool_option("assumptions"); error_labels=_options.get_list_option("error-label"); + enable_pointer_primitive_check = + _options.get_bool_option("pointer-primitive-check"); } typedef goto_functionst::goto_functiont goto_functiont; @@ -185,6 +187,20 @@ class goto_checkt const exprt &src_expr, const guardt &guard); + /// Generates VCCs to check that pointers passed to pointer primitives are + /// either null or valid + /// + /// \param expr: the pointer primitive expression + /// \param guard: the condition under which the operation happens + void pointer_primitive_check(const exprt &expr, const guardt &guard); + + /// Returns true if the given expression is a pointer primitive such as + /// __CPROVER_r_ok() + /// + /// \param expr expression + /// \return true if the given expression is a pointer primitive + bool is_pointer_primitive(const exprt &expr); + conditionst address_check(const exprt &address, const exprt &size); void integer_overflow_check(const exprt &, const guardt &); void conversion_check(const exprt &, const guardt &); @@ -238,6 +254,7 @@ class goto_checkt bool enable_assertions; bool enable_built_in_assertions; bool enable_assumptions; + bool enable_pointer_primitive_check; typedef optionst::value_listt error_labelst; error_labelst error_labels; @@ -1163,6 +1180,53 @@ void goto_checkt::pointer_validity_check( } } +void goto_checkt::pointer_primitive_check( + const exprt &expr, + const guardt &guard) +{ + if(!enable_pointer_primitive_check) + return; + + const exprt pointer = (expr.id() == ID_r_ok || expr.id() == ID_w_ok) + ? to_binary_expr(expr).lhs() + : to_unary_expr(expr).op(); + + CHECK_RETURN(pointer.type().id() == ID_pointer); + + const auto size_of_expr_opt = size_of_expr(pointer.type().subtype(), ns); + + const exprt size = !size_of_expr_opt.has_value() + ? from_integer(1, size_type()) + : size_of_expr_opt.value(); + + const conditionst &conditions = address_check(pointer, size); + + exprt::operandst conjuncts; + + for(const auto &c : conditions) + conjuncts.push_back(c.assertion); + + const or_exprt or_expr(null_object(pointer), conjunction(conjuncts)); + + add_guarded_property( + or_expr, + "pointer in pointer primitive is neither null nor valid", + "pointer primitives", + expr.source_location(), + expr, + guard); +} + +bool goto_checkt::is_pointer_primitive(const exprt &expr) +{ + // we don't need to include the __CPROVER_same_object primitive here as it + // is replaced by lower level primitives in the special function handling + // during typechecking (see c_typecheck_expr.cpp) + return expr.id() == ID_pointer_object || expr.id() == ID_pointer_offset || + expr.id() == ID_object_size || expr.id() == ID_r_ok || + expr.id() == ID_w_ok || expr.id() == ID_is_dynamic_object; +} + goto_checkt::conditionst goto_checkt::address_check(const exprt &address, const exprt &size) { @@ -1740,6 +1804,10 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard) { pointer_validity_check(to_dereference_expr(expr), expr, guard); } + else if(is_pointer_primitive(expr)) + { + pointer_primitive_check(expr, guard); + } } void goto_checkt::check(const exprt &expr) @@ -1860,6 +1928,8 @@ void goto_checkt::goto_check( flag_resetter.set_flag(enable_undefined_shift_check, false); else if(d.first == "disable:nan-check") flag_resetter.set_flag(enable_nan_check, false); + else if(d.first == "disable:pointer-primitive-check") + flag_resetter.set_flag(enable_pointer_primitive_check, false); } new_code.clear(); @@ -2049,7 +2119,7 @@ void goto_checkt::goto_check( } else if(i.is_dead()) { - if(enable_pointer_check) + if(enable_pointer_check || enable_pointer_primitive_check) { assert(i.code.operands().size()==1); const symbol_exprt &variable=to_symbol_expr(i.code.op0()); diff --git a/src/analyses/goto_check.h b/src/analyses/goto_check.h index d7d67a4321d..ad47e6827d7 100644 --- a/src/analyses/goto_check.h +++ b/src/analyses/goto_check.h @@ -38,7 +38,8 @@ void goto_check( "(div-by-zero-check)(enum-range-check)(signed-overflow-check)(unsigned-" \ "overflow-check)" \ "(pointer-overflow-check)(conversion-check)(undefined-shift-check)" \ - "(float-overflow-check)(nan-check)(no-built-in-assertions)" + "(float-overflow-check)(nan-check)(no-built-in-assertions)" \ + "(pointer-primitive-check)" // clang-format off #define HELP_GOTO_CHECK \ @@ -55,7 +56,7 @@ void goto_check( " --nan-check check floating-point for NaN\n" \ " --no-built-in-assertions ignore assertions in built-in library\n" \ " --enum-range-check checks that all enum type expressions have values in the enum range\n" /* NOLINT(whitespace/line_length) */ \ -// clang-format on + " --pointer-primitive-check checks that all pointers in pointer primitives are valid or null\n" /* NOLINT(whitespace/line_length) */ #define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \ options.set_option("bounds-check", cmdline.isset("bounds-check")); \ @@ -70,6 +71,8 @@ void goto_check( options.set_option("undefined-shift-check", cmdline.isset("undefined-shift-check")); /* NOLINT(whitespace/line_length) */ \ options.set_option("float-overflow-check", cmdline.isset("float-overflow-check")); /* NOLINT(whitespace/line_length) */ \ options.set_option("nan-check", cmdline.isset("nan-check")); \ - options.set_option("built-in-assertions", !cmdline.isset("no-built-in-assertions")) /* NOLINT(whitespace/line_length) */ + options.set_option("built-in-assertions", !cmdline.isset("no-built-in-assertions")); /* NOLINT(whitespace/line_length) */ \ + options.set_option("pointer-primitive-check", cmdline.isset("pointer-primitive-check")) /* NOLINT(whitespace/line_length) */ +// clang-format on #endif // CPROVER_ANALYSES_GOTO_CHECK_H