From 1b2e321dab7e493a3df6639a49f77b940eb77e1f Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 31 Aug 2016 09:24:54 +0100 Subject: [PATCH 1/3] Don't reference CPROVER_memory from Java code. Fixes #197. goto-symex's value-set analysis can reach the conclusion that an integer may be cast to a pointer, and so generate a reference to the __CPROVER_memory symbol. This is invalid in Java however, since the symbol is not defined and of course Java cannot express dereferencing a non-pointer type. This change disables generation of __CPROVER_memory references when a Java-typed entry point is found. I couldn't provide a test case against master at this time however because the examples in both of the above bugs now succeed against master, presumably because value-set analysis has been improved and is harder to confuse into introducing a pointer-to-int cast. --- src/cbmc/bmc.cpp | 7 +++++++ src/goto-symex/goto_symex.h | 3 +++ src/goto-symex/symex_dereference.cpp | 5 +++-- src/pointer-analysis/value_set_dereference.cpp | 8 +++++++- src/pointer-analysis/value_set_dereference.h | 7 +++++-- 5 files changed, 25 insertions(+), 5 deletions(-) diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index ba970e659c8..8b76cabec38 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -428,6 +429,12 @@ safety_checkert::resultt bmct::run( symex.set_message_handler(get_message_handler()); symex.options=options; + { + const symbolt *init_symbol; + if(!ns.lookup(CPROVER_PREFIX "initialize", init_symbol)) + symex.mode=init_symbol->mode; + } + status() << "Starting Bounded Model Checking" << eom; symex.last_source_location.make_nil(); diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 09efe7cadac..9680ccd0799 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -49,6 +49,7 @@ class goto_symext remaining_vccs(0), constant_propagation(true), new_symbol_table(_new_symbol_table), + mode(), ns(_ns), target(_target), atomic_section_counter(0), @@ -95,6 +96,8 @@ class goto_symext optionst options; symbol_tablet &new_symbol_table; + irep_idt mode; + protected: const namespacet &ns; symex_targett ⌖ diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp index f2f0176ec68..81e99e99fa9 100644 --- a/src/goto-symex/symex_dereference.cpp +++ b/src/goto-symex/symex_dereference.cpp @@ -295,8 +295,9 @@ void goto_symext::dereference_rec( ns, new_symbol_table, options, - symex_dereference_state); - + symex_dereference_state, + mode); + // std::cout << "**** " << from_expr(ns, "", tmp1) << std::endl; exprt tmp2=dereference.dereference( tmp1, guard, write?value_set_dereferencet::WRITE:value_set_dereferencet::READ); diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 57c6b3682fd..03a8c52bcfc 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -454,7 +454,13 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( // This is stuff like *((char *)5). // This is turned into an access to __CPROVER_memory[...]. - const symbolt &memory_symbol=ns.lookup(CPROVER_PREFIX "memory"); + if(language_mode==ID_java) + { + result.value=nil_exprt(); + return result; + } + + const symbolt &memory_symbol=ns.lookup(CPROVER_PREFIX "memory"); exprt symbol_expr=symbol_exprt(memory_symbol.name, memory_symbol.type); exprt pointer_offset=unary_exprt( diff --git a/src/pointer-analysis/value_set_dereference.h b/src/pointer-analysis/value_set_dereference.h index 9e43f799e04..de05d250f00 100644 --- a/src/pointer-analysis/value_set_dereference.h +++ b/src/pointer-analysis/value_set_dereference.h @@ -39,11 +39,13 @@ class value_set_dereferencet const namespacet &_ns, symbol_tablet &_new_symbol_table, const optionst &_options, - dereference_callbackt &_dereference_callback): + dereference_callbackt &_dereference_callback, + const irep_idt _language_mode = irep_idt()): ns(_ns), new_symbol_table(_new_symbol_table), options(_options), - dereference_callback(_dereference_callback) + dereference_callback(_dereference_callback), + language_mode(_language_mode) { } virtual ~value_set_dereferencet() { } @@ -80,6 +82,7 @@ class value_set_dereferencet symbol_tablet &new_symbol_table; const optionst &options; dereference_callbackt &dereference_callback; + const irep_idt language_mode; static unsigned invalid_counter; bool dereference_type_compare( From 387156aa305004be217088197b69e0cf266b65cd Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 5 Dec 2016 14:39:54 +0000 Subject: [PATCH 2/3] Make symex language mode symbol clearer 'mode' replaced by 'language_mode', a field containing ID_java or similar to denote the source language in use if known. --- src/cbmc/bmc.cpp | 2 +- src/goto-symex/goto_symex.h | 6 ++++-- src/goto-symex/symex_dereference.cpp | 2 +- src/pointer-analysis/value_set_dereference.cpp | 2 +- src/pointer-analysis/value_set_dereference.h | 4 +++- 5 files changed, 10 insertions(+), 6 deletions(-) diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 8b76cabec38..37e0ade8b3a 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -432,7 +432,7 @@ safety_checkert::resultt bmct::run( { const symbolt *init_symbol; if(!ns.lookup(CPROVER_PREFIX "initialize", init_symbol)) - symex.mode=init_symbol->mode; + symex.language_mode=init_symbol->mode; } status() << "Starting Bounded Model Checking" << eom; diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 9680ccd0799..46f12e023ca 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -49,7 +49,7 @@ class goto_symext remaining_vccs(0), constant_propagation(true), new_symbol_table(_new_symbol_table), - mode(), + language_mode(), ns(_ns), target(_target), atomic_section_counter(0), @@ -96,7 +96,9 @@ class goto_symext optionst options; symbol_tablet &new_symbol_table; - irep_idt mode; + /// language_mode: ID_java, ID_C or another language identifier + /// if we know the source language in use, irep_idt() otherwise. + irep_idt language_mode; protected: const namespacet &ns; diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp index 81e99e99fa9..dbe5e9aed3c 100644 --- a/src/goto-symex/symex_dereference.cpp +++ b/src/goto-symex/symex_dereference.cpp @@ -296,7 +296,7 @@ void goto_symext::dereference_rec( new_symbol_table, options, symex_dereference_state, - mode); + language_mode); // std::cout << "**** " << from_expr(ns, "", tmp1) << std::endl; exprt tmp2=dereference.dereference( diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 03a8c52bcfc..860e80bb1a3 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -460,7 +460,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( return result; } - const symbolt &memory_symbol=ns.lookup(CPROVER_PREFIX "memory"); + const symbolt &memory_symbol=ns.lookup(CPROVER_PREFIX "memory"); exprt symbol_expr=symbol_exprt(memory_symbol.name, memory_symbol.type); exprt pointer_offset=unary_exprt( diff --git a/src/pointer-analysis/value_set_dereference.h b/src/pointer-analysis/value_set_dereference.h index de05d250f00..f0e4ac6c1c0 100644 --- a/src/pointer-analysis/value_set_dereference.h +++ b/src/pointer-analysis/value_set_dereference.h @@ -40,7 +40,7 @@ class value_set_dereferencet symbol_tablet &_new_symbol_table, const optionst &_options, dereference_callbackt &_dereference_callback, - const irep_idt _language_mode = irep_idt()): + const irep_idt _language_mode=irep_idt()): ns(_ns), new_symbol_table(_new_symbol_table), options(_options), @@ -82,6 +82,8 @@ class value_set_dereferencet symbol_tablet &new_symbol_table; const optionst &options; dereference_callbackt &dereference_callback; + /// language_mode: ID_java, ID_C or another language identifier + /// if we know the source language in use, irep_idt() otherwise. const irep_idt language_mode; static unsigned invalid_counter; From 66db65183fb2bb9eab66acc2421a98f66eed0f03 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 5 Dec 2016 15:57:12 +0000 Subject: [PATCH 3/3] Add comment that goto_program_dereference doesn't specify language mode Explicitly pass ID_nil instead of silently leaving the language uninitialised as before. --- src/pointer-analysis/goto_program_dereference.h | 6 +++++- src/pointer-analysis/value_set_dereference.h | 2 +- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/pointer-analysis/goto_program_dereference.h b/src/pointer-analysis/goto_program_dereference.h index 5dfcd3123a8..68d8550ebc9 100644 --- a/src/pointer-analysis/goto_program_dereference.h +++ b/src/pointer-analysis/goto_program_dereference.h @@ -19,6 +19,10 @@ Author: Daniel Kroening, kroening@kroening.com class goto_program_dereferencet:protected dereference_callbackt { public: + // Note: this currently doesn't specify a source language + // for the final argument to value_set_dereferencet. + // This means that language-inappropriate values such as + // (struct A*)some_integer_value in Java, may be returned. goto_program_dereferencet( const namespacet &_ns, symbol_tablet &_new_symbol_table, @@ -27,7 +31,7 @@ class goto_program_dereferencet:protected dereference_callbackt options(_options), ns(_ns), value_sets(_value_sets), - dereference(_ns, _new_symbol_table, _options, *this) { } + dereference(_ns, _new_symbol_table, _options, *this, ID_nil) { } void dereference_program( goto_programt &goto_program, diff --git a/src/pointer-analysis/value_set_dereference.h b/src/pointer-analysis/value_set_dereference.h index f0e4ac6c1c0..e481b8085d8 100644 --- a/src/pointer-analysis/value_set_dereference.h +++ b/src/pointer-analysis/value_set_dereference.h @@ -40,7 +40,7 @@ class value_set_dereferencet symbol_tablet &_new_symbol_table, const optionst &_options, dereference_callbackt &_dereference_callback, - const irep_idt _language_mode=irep_idt()): + const irep_idt _language_mode): ns(_ns), new_symbol_table(_new_symbol_table), options(_options),