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/regression/cbmc/memory_allocation2/cmdline.desc b/regression/cbmc/memory_allocation2/cmdline.desc new file mode 100644 index 00000000000..4e63275dc07 --- /dev/null +++ b/regression/cbmc/memory_allocation2/cmdline.desc @@ -0,0 +1,11 @@ +CORE +main.c +--bounds-check -DCMDLINE --mmio-regions 0x1000:400,0x11000:400 --mmio-regions 0x21000:400,0x31000:400 +^EXIT=10$ +^SIGNAL=0$ +^\[main\.array_bounds\.[1-5]\] .*: SUCCESS$ +^\[main\.array_bounds\.[67]\] line 40 array.buffer (dynamic object )?upper bound in buffers\[\(signed long (long )?int\)0\]->buffer\[\(signed long (long )?int\)100\]: FAILURE$ +^\*\* 1 of 12 failed +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc/memory_allocation2/main.c b/regression/cbmc/memory_allocation2/main.c index 6549e71957a..c90056fa1e5 100644 --- a/regression/cbmc/memory_allocation2/main.c +++ b/regression/cbmc/memory_allocation2/main.c @@ -24,10 +24,12 @@ static buffert(*const buffers[4]) = {BUF0, BUF1, BUF2, BUF3}; main() { +#ifndef CMDLINE __CPROVER_allocated_memory(BUF0_BASE, sizeof(buffert)); __CPROVER_allocated_memory(BUF1_BASE, sizeof(buffert)); __CPROVER_allocated_memory(BUF2_BASE, sizeof(buffert)); __CPROVER_allocated_memory(BUF3_BASE, sizeof(buffert)); +#endif _cbmc_printf2(sizeof_buffers, sizeof(buffers)); _cbmc_printf2(sizeof_buffers_0, sizeof(buffers[0])); @@ -36,4 +38,7 @@ main() buffers[0]->buffer[0]; buffers[0]->buffer[BUFFER_SIZE - 1]; buffers[0]->buffer[BUFFER_SIZE]; // should be out-of-bounds + buffers[1]->buffer[0]; + buffers[2]->buffer[0]; + buffers[3]->buffer[0]; } diff --git a/regression/cbmc/memory_allocation2/test.desc b/regression/cbmc/memory_allocation2/test.desc index c88637311c2..715aa1e3f23 100644 --- a/regression/cbmc/memory_allocation2/test.desc +++ b/regression/cbmc/memory_allocation2/test.desc @@ -4,8 +4,8 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^\[main\.array_bounds\.[1-5]\] .*: SUCCESS$ -^\[main\.array_bounds\.[67]\] line 38 array.buffer (dynamic object )?upper bound in buffers\[\(signed long (long )?int\)0\]->buffer\[\(signed long (long )?int\)100\]: FAILURE$ -^\*\* 1 of 6 failed +^\[main\.array_bounds\.[67]\] line 40 array.buffer (dynamic object )?upper bound in buffers\[\(signed long (long )?int\)0\]->buffer\[\(signed long (long )?int\)100\]: FAILURE$ +^\*\* 1 of 12 failed ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp index 97057b1b65c..0b7c7d861ab 100644 --- a/src/ansi-c/goto_check_c.cpp +++ b/src/ansi-c/goto_check_c.cpp @@ -44,6 +44,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "literals/convert_integer_literal.h" + class goto_check_ct { public: @@ -76,6 +78,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_list_option("mmio-regions")); } typedef goto_functionst::goto_functiont goto_functiont; @@ -327,6 +331,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 optionst::value_listt ®ions); }; /// Allows to: @@ -463,6 +469,22 @@ void goto_check_ct::collect_allocations(const goto_functionst &goto_functions) } } +void goto_check_ct::parse_mmio_regions(const optionst::value_listt ®ions) +{ + for(const std::string &range : regions) + { + const auto sep = range.find(':'); + if(sep == std::string::npos || sep + 1 == range.size()) + continue; + + const std::string start = range.substr(0, sep); + const std::string size = range.substr(sep + 1); + + allocations.push_back( + {convert_integer_literal(start), convert_integer_literal(size)}); + } +} + void goto_check_ct::invalidate(const exprt &lhs) { if(lhs.id() == ID_index) diff --git a/src/ansi-c/goto_check_c.h b/src/ansi-c/goto_check_c.h index eed055fb480..20b56466ea2 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,9 @@ 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_comma_separated_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) */ \