diff --git a/regression/cbmc/Pointer28/main.c b/regression/cbmc/Pointer28/main.c index 761d8a9275d..b76605d27ea 100644 --- a/regression/cbmc/Pointer28/main.c +++ b/regression/cbmc/Pointer28/main.c @@ -1,7 +1,6 @@ int main() { int *p = (int *)4; - __CPROVER_allocated_memory(4, sizeof(int)); int i; int **q; char *pp; @@ -21,7 +20,6 @@ int main() __CPROVER_assert(p == 0, "i==0 => p==NULL"); q = (int **)8; - __CPROVER_allocated_memory(8, sizeof(int *)); *q = &i; **q = 0x01020304; __CPROVER_assert(i == 0x01020304, "**q"); diff --git a/regression/cbmc/Pointer28/test.desc b/regression/cbmc/Pointer28/test.desc index f5e039ba3ed..dee6cd0a129 100644 --- a/regression/cbmc/Pointer28/test.desc +++ b/regression/cbmc/Pointer28/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check --little-endian +--pointer-check --little-endian --mmio-regions 4:4,8:8 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/memory_allocation1/cmdline.desc b/regression/cbmc/memory_allocation1/cmdline.desc new file mode 100644 index 00000000000..7d9a5de5c42 --- /dev/null +++ b/regression/cbmc/memory_allocation1/cmdline.desc @@ -0,0 +1,12 @@ +CORE broken-smt-backend +main.c +--pointer-check -DCMDLINE --mmio-regions 0x10:4 +^EXIT=10$ +^SIGNAL=0$ +^\[main\.pointer_dereference\.2\] .* dereference failure: invalid integer address in \*p: SUCCESS$ +^\[main\.assertion\.1\] .* assertion \*p==42: SUCCESS$ +^\[main\.pointer_dereference\.[0-9]+\] .* dereference failure: invalid integer address in p\[.*1\]: FAILURE$ +^\[main\.assertion\.2\] .* assertion \*\(p\+1\)==42: SUCCESS$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc/memory_allocation1/main.c b/regression/cbmc/memory_allocation1/main.c index 3d9a3e59810..c9cc7b63208 100644 --- a/regression/cbmc/memory_allocation1/main.c +++ b/regression/cbmc/memory_allocation1/main.c @@ -4,7 +4,9 @@ int main() { int *p=0x10; +#ifndef CMDLINE __CPROVER_allocated_memory(0x10, sizeof(int)); +#endif *p=42; assert(*p==42); *(p+1)=42; diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h index 51de0f7bbfb..f02cb915f8d 100644 --- a/src/ansi-c/cprover_builtin_headers.h +++ b/src/ansi-c/cprover_builtin_headers.h @@ -46,7 +46,6 @@ __CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *); __CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *); __CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *); __CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *); -void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent); // float stuff int __CPROVER_fpclassify(int, int, int, int, int, ...); diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp index ebec548c21f..cd4861f5e11 100644 --- a/src/ansi-c/goto_check_c.cpp +++ b/src/ansi-c/goto_check_c.cpp @@ -33,6 +33,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -44,6 +45,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "literals/convert_integer_literal.h" + class goto_check_ct { public: @@ -76,6 +79,8 @@ class goto_check_ct error_labels = _options.get_list_option("error-label"); enable_pointer_primitive_check = _options.get_bool_option("pointer-primitive-check"); + + parse_mmio_regions(_options.get_option("mmio-regions")); } typedef goto_functionst::goto_functiont goto_functiont; @@ -84,13 +89,6 @@ class goto_check_ct const irep_idt &function_identifier, goto_functiont &goto_function); - /// Fill the list of allocations \ref allocationst with for - /// every allocation instruction. Also check that each allocation is - /// well-formed. - /// \param goto_functions: goto functions from which the allocations are to be - /// collected - void collect_allocations(const goto_functionst &goto_functions); - protected: const namespacet &ns; std::unique_ptr local_bitvector_analysis; @@ -327,6 +325,8 @@ class goto_check_ct /// \returns a pair (name, status) if the match succeeds /// and the name is known, nothing otherwise. named_check_statust match_named_check(const irep_idt &named_check) const; + + void parse_mmio_regions(const std::string ®ions); }; /// Allows to: @@ -420,35 +420,19 @@ static exprt implication(exprt lhs, exprt rhs) } } -void goto_check_ct::collect_allocations(const goto_functionst &goto_functions) +void goto_check_ct::parse_mmio_regions(const std::string ®ions) { - for(const auto &gf_entry : goto_functions.function_map) + for(const std::string &range : split_string(regions, ',', true, true)) { - for(const auto &instruction : gf_entry.second.body.instructions) - { - if(!instruction.is_function_call()) - continue; + const auto sep = range.find(':'); + if(sep == std::string::npos || sep + 1 == range.size()) + continue; - const auto &function = instruction.call_function(); - if( - function.id() != ID_symbol || - to_symbol_expr(function).get_identifier() != CPROVER_PREFIX - "allocated_memory") - continue; + const std::string start = range.substr(0, sep); + const std::string size = range.substr(sep + 1); - const code_function_callt::argumentst &args = - instruction.call_arguments(); - if( - args.size() != 2 || args[0].type().id() != ID_unsignedbv || - args[1].type().id() != ID_unsignedbv) - throw "expected two unsigned arguments to " CPROVER_PREFIX - "allocated_memory"; - - DATA_INVARIANT( - args[0].type() == args[1].type(), - "arguments of allocated_memory must have same type"); - allocations.push_back({args[0], args[1]}); - } + allocations.push_back( + {convert_integer_literal(start), convert_integer_literal(size)}); } } @@ -2402,8 +2386,6 @@ void goto_check_c( { goto_check_ct goto_check(ns, options, message_handler); - goto_check.collect_allocations(goto_functions); - for(auto &gf_entry : goto_functions.function_map) { goto_check.goto_check(gf_entry.first, gf_entry.second); diff --git a/src/ansi-c/goto_check_c.h b/src/ansi-c/goto_check_c.h index 52baf3cdf1d..e7b2d4a39dc 100644 --- a/src/ansi-c/goto_check_c.h +++ b/src/ansi-c/goto_check_c.h @@ -44,6 +44,7 @@ void goto_check_c( "(pointer-overflow-check)(conversion-check)(undefined-shift-check)" \ "(float-overflow-check)(nan-check)(no-built-in-assertions)" \ "(pointer-primitive-check)" \ + "(mmio-regions):" \ "(retain-trivial-checks)" \ "(error-label):" \ "(no-assertions)(no-assumptions)" \ @@ -64,6 +65,8 @@ void goto_check_c( " --nan-check check floating-point for NaN\n" \ " --enum-range-check checks that all enum type expressions have values in the enum range\n" /* NOLINT(whitespace/line_length) */ \ " --pointer-primitive-check checks that all pointers in pointer primitives are valid or null\n" /* NOLINT(whitespace/line_length) */ \ + " --mmio-regions addr:sz,... list of start-address:size address ranges\n" \ + " permitted for read/write access\n" \ " --retain-trivial-checks include checks that are trivially true\n" \ " --error-label label check that label is unreachable\n" \ " --no-built-in-assertions ignore assertions in built-in library\n" \ @@ -86,6 +89,8 @@ void goto_check_c( 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("pointer-primitive-check", cmdline.isset("pointer-primitive-check")); /* NOLINT(whitespace/line_length) */ \ + if(cmdline.isset("mmio-regions")) \ + options.set_option("mmio-regions", cmdline.get_values("mmio-regions")); \ options.set_option("retain-trivial-checks", \ cmdline.isset("retain-trivial-checks")); \ options.set_option("assertions", !cmdline.isset("no-assertions")); /* NOLINT(whitespace/line_length) */ \