From f2dc978365f4bf2675f9d8688a38cdcfc24e9116 Mon Sep 17 00:00:00 2001 From: svorenova Date: Wed, 1 Aug 2018 15:23:02 +0100 Subject: [PATCH 1/5] Add a new comment to mark variables that should not be nondet initialized This will be used by nondet-static option and will mark internal variables that are not CPROVER variables such as language specific internal variables - in Java, for example, @inflight_exception and clinit_already_run --- src/util/irep_ids.def | 1 + 1 file changed, 1 insertion(+) diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 151eb6f6b6e..332a826b712 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -665,6 +665,7 @@ IREP_ID_TWO(java_lambda_method_handles, lambda_method_handles) IREP_ID_ONE(havoc_object) IREP_ID_TWO(overflow_shl, overflow-shl) IREP_ID_TWO(C_no_initialization_required, #no_initialization_required) +IREP_ID_TWO(C_no_nondet_initialization, #no_nondet_initialization) IREP_ID_TWO(overlay_class, java::com.diffblue.OverlayClassImplementation) IREP_ID_TWO(overlay_method, java::com.diffblue.OverlayMethodImplementation) IREP_ID_TWO(ignored_method, java::com.diffblue.IgnoredMethodImplementation) From b3c08d3dcabe3963bdc48b0eebeccd0df173e7a0 Mon Sep 17 00:00:00 2001 From: svorenova Date: Wed, 1 Aug 2018 15:38:14 +0100 Subject: [PATCH 2/5] Mark internal Java variables with ID_C_no_nondet_initialization This sets the flag to be true for java::@inflight_exception and static initializer internal variables (including clinit_already_run) --- jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp | 1 + jbmc/src/java_bytecode/java_static_initializers.cpp | 1 + 2 files changed, 2 insertions(+) diff --git a/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp b/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp index 106cd0fb642..1fc8e06b4b2 100644 --- a/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp @@ -51,6 +51,7 @@ void java_internal_additions(symbol_table_baset &dest) symbol.name = INFLIGHT_EXCEPTION_VARIABLE_NAME; symbol.mode = ID_java; symbol.type = pointer_type(empty_typet()); + symbol.type.set(ID_C_no_nondet_initialization, true); symbol.value = null_pointer_exprt(to_pointer_type(symbol.type)); symbol.is_file_local = false; symbol.is_static_lifetime = true; diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp index a5dfd289cfa..74513546f4e 100644 --- a/jbmc/src/java_bytecode/java_static_initializers.cpp +++ b/jbmc/src/java_bytecode/java_static_initializers.cpp @@ -91,6 +91,7 @@ static symbolt add_new_variable_symbol( new_symbol.pretty_name = name; new_symbol.base_name = name; new_symbol.type = type; + new_symbol.type.set(ID_C_no_nondet_initialization, true); new_symbol.value = value; new_symbol.is_lvalue = true; new_symbol.is_state_var = true; From a50562e9f9500b4dbbc25f1bd28049f37338e991 Mon Sep 17 00:00:00 2001 From: svorenova Date: Wed, 1 Aug 2018 15:42:51 +0100 Subject: [PATCH 3/5] Mark java.lang.String.Literals with ID_C_constant This will also make sure that nondet-static option does not nondet- initialize these --- jbmc/src/java_bytecode/java_string_literals.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/jbmc/src/java_bytecode/java_string_literals.cpp b/jbmc/src/java_bytecode/java_string_literals.cpp index 464a1e38274..8463139d7b8 100644 --- a/jbmc/src/java_bytecode/java_string_literals.cpp +++ b/jbmc/src/java_bytecode/java_string_literals.cpp @@ -84,6 +84,7 @@ symbol_exprt get_or_create_string_literal_symbol( symbolt new_symbol; new_symbol.name = escaped_symbol_name_with_prefix; new_symbol.type = string_type; + new_symbol.type.set(ID_C_constant, true); new_symbol.base_name = escaped_symbol_name; new_symbol.pretty_name = value; new_symbol.mode = ID_java; @@ -131,6 +132,7 @@ symbol_exprt get_or_create_string_literal_symbol( array_symbol.is_state_var = true; array_symbol.value = data; array_symbol.type = array_symbol.value.type(); + array_symbol.type.set(ID_C_constant, true); if(symbol_table.add(array_symbol)) throw "failed to add constarray symbol to symbol table"; @@ -161,6 +163,7 @@ symbol_exprt get_or_create_string_literal_symbol( java_int_type(), symbol_table); return_symbol.type = return_symbol.value.type(); + return_symbol.type.set(ID_C_constant, true); if(symbol_table.add(return_symbol)) throw "failed to add return symbol to symbol table"; From b62bf0158161d68756186671f13a15fb78ac9912 Mon Sep 17 00:00:00 2001 From: svorenova Date: Wed, 1 Aug 2018 16:01:20 +0100 Subject: [PATCH 4/5] Make nondet-static check for ID_C_no_nondet_initialization --- src/goto-instrument/nondet_static.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/goto-instrument/nondet_static.cpp b/src/goto-instrument/nondet_static.cpp index 51cbf5034fe..57856ae3528 100644 --- a/src/goto-instrument/nondet_static.cpp +++ b/src/goto-instrument/nondet_static.cpp @@ -42,6 +42,14 @@ void nondet_static( if(has_prefix(id2string(sym.get_identifier()), CPROVER_PREFIX)) continue; + // any other internal variable such as Java specific? + if( + ns.lookup(sym.get_identifier()) + .type.get_bool(ID_C_no_nondet_initialization)) + { + continue; + } + // static lifetime? if(!ns.lookup(sym.get_identifier()).is_static_lifetime) continue; From daff1d1c75c5a4795320fe523e6845571dd77397 Mon Sep 17 00:00:00 2001 From: svorenova Date: Wed, 1 Aug 2018 16:10:14 +0100 Subject: [PATCH 5/5] Make nondet-static replace lines in CPROVER_init Instead of keeping both the original line that sets the value of a variable and the new line that nondet initializes it, we only keep the new one --- src/goto-instrument/nondet_static.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/goto-instrument/nondet_static.cpp b/src/goto-instrument/nondet_static.cpp index 57856ae3528..cfa058baad7 100644 --- a/src/goto-instrument/nondet_static.cpp +++ b/src/goto-instrument/nondet_static.cpp @@ -58,11 +58,11 @@ void nondet_static( if(is_constant_or_has_constant_components(sym.type(), ns)) continue; - i_it=init.insert_before(++i_it); + const goto_programt::instructiont original_instruction = instruction; i_it->make_assignment(); i_it->code=code_assignt(sym, side_effect_expr_nondett(sym.type())); - i_it->source_location=instruction.source_location; - i_it->function=instruction.function; + i_it->source_location = original_instruction.source_location; + i_it->function = original_instruction.function; } else if(instruction.is_function_call()) {