From 8f1868cf0a2f78bf09bce3e643f89847e51a9c47 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 15 Jul 2025 19:40:09 +0000 Subject: [PATCH 1/2] expr2c: output ID_allocate in a way that goto-cc can compile We can compile __CPROVER_allocate, but wouldn't be able to handle ALLOCATE(type, size, bool). --- .../gen_nondet_string_init.cpp | 2 +- src/ansi-c/expr2c.cpp | 20 ++++++++++++------- 2 files changed, 14 insertions(+), 8 deletions(-) diff --git a/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp b/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp index 547ae2f148f..b3b0e2fe976 100644 --- a/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp +++ b/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp @@ -92,7 +92,7 @@ SCENARIO( CPROVER_PREFIX "assume(tmp_object_factory <= 20);", "char (*nondet_infinite_array_pointer)[INFINITY()];", "nondet_infinite_array_pointer = " - "ALLOCATE(char [INFINITY()], INFINITY(), false);", + "__CPROVER_allocate(INFINITY(), false);", "*nondet_infinite_array_pointer = NONDET(char [INFINITY()]);", "int return_array;", "return_array = cprover_associate_array_to_pointer_func" diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 705936ad81d..6cf0f170abc 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -1156,24 +1156,30 @@ std::string expr2ct::convert_allocate(const exprt &src, unsigned &precedence) if(src.operands().size() != 2) return convert_norep(src, precedence); - unsigned p0; - std::string op0 = convert_with_precedence(to_binary_expr(src).op0(), p0); + const binary_exprt &binary_expr = to_binary_expr(src); unsigned p1; - std::string op1 = convert_with_precedence(to_binary_expr(src).op1(), p1); + std::string op1 = convert_with_precedence(binary_expr.op1(), p1); - std::string dest = "ALLOCATE"; + std::string dest = CPROVER_PREFIX "allocate"; dest += '('; + const typet &type = + static_cast(binary_expr.op0().find(ID_C_c_sizeof_type)); if( src.type().id() == ID_pointer && - to_pointer_type(src.type()).base_type().id() != ID_empty) + to_pointer_type(src.type()).base_type() == type) { - dest += convert(to_pointer_type(src.type()).base_type()); + dest += "sizeof(" + convert(to_pointer_type(src.type()).base_type()) + ')'; dest+=", "; } + else + { + unsigned p0; + dest += convert_with_precedence(binary_expr.op0(), p0); + } - dest += op0 + ", " + op1; + dest += ", " + op1; dest += ')'; return dest; From f06afc45ff59afc14698472642de8208c515e385 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 15 Jul 2025 19:38:03 +0000 Subject: [PATCH 2/2] goto-harness: use __CPROVER_(de)?allocate, not malloc/free Do not use C-specific functions when amending GOTO programs. Fixes: #8681 --- .../gen_nondet_string_init.cpp | 2 +- regression/goto-harness/no-malloc-free/main.c | 16 ++++ .../goto-harness/no-malloc-free/test.desc | 13 +++ src/goto-harness/recursive_initialization.cpp | 84 ++++++++----------- src/goto-harness/recursive_initialization.h | 14 +--- 5 files changed, 71 insertions(+), 58 deletions(-) create mode 100644 regression/goto-harness/no-malloc-free/main.c create mode 100644 regression/goto-harness/no-malloc-free/test.desc diff --git a/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp b/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp index b3b0e2fe976..307afac14c9 100644 --- a/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp +++ b/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp @@ -92,7 +92,7 @@ SCENARIO( CPROVER_PREFIX "assume(tmp_object_factory <= 20);", "char (*nondet_infinite_array_pointer)[INFINITY()];", "nondet_infinite_array_pointer = " - "__CPROVER_allocate(INFINITY(), false);", + CPROVER_PREFIX "allocate(INFINITY(), false);", "*nondet_infinite_array_pointer = NONDET(char [INFINITY()]);", "int return_array;", "return_array = cprover_associate_array_to_pointer_func" diff --git a/regression/goto-harness/no-malloc-free/main.c b/regression/goto-harness/no-malloc-free/main.c new file mode 100644 index 00000000000..51461a5dd36 --- /dev/null +++ b/regression/goto-harness/no-malloc-free/main.c @@ -0,0 +1,16 @@ +#include + +void test_fn(int *a) + // clang-format off + __CPROVER_requires((a == (int*)0) || __CPROVER_is_fresh(a, sizeof(*a))) + __CPROVER_requires((a != (int*)0) ==> (*a != 5)) + __CPROVER_ensures((a != (int*)0) ==> (*a == 5)) + __CPROVER_assigns(*a) +// clang-format on +{ + assert((a == (int *)0) || (*a != 5)); + if(a != (int *)0) + { + *a = 5; + } +} diff --git a/regression/goto-harness/no-malloc-free/test.desc b/regression/goto-harness/no-malloc-free/test.desc new file mode 100644 index 00000000000..6b47bfeed2a --- /dev/null +++ b/regression/goto-harness/no-malloc-free/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--harness-type call-function --function test_fn +^\[test_fn.assertion.1\] line 11 assertion \(a == \(int \*\)0\) \|\| \(\*a != 5\): FAILURE$ +^\*\* 1 of \d+ failed +VERIFICATION FAILED +^EXIT=10$ +^SIGNAL=0$ +-- +CALL.*malloc +CALL.*free +-- +Ensure that we do not generate calls to malloc or free. diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp index fc921934fac..395808b746b 100644 --- a/src/goto-harness/recursive_initialization.cpp +++ b/src/goto-harness/recursive_initialization.cpp @@ -372,24 +372,6 @@ irep_idt recursive_initializationt::build_constructor(const exprt &expr) return type_constructor_names.at(key); } -symbol_exprt recursive_initializationt::get_malloc_function() -{ - auto malloc_sym = goto_model.symbol_table.lookup("malloc"); - if(malloc_sym == nullptr) - { - symbolt new_malloc_sym{ - "malloc", - code_typet{ - {code_typet::parametert{size_type()}}, pointer_type(empty_typet{})}, - initialization_config.mode}; - new_malloc_sym.pretty_name = "malloc"; - new_malloc_sym.base_name = "malloc"; - goto_model.symbol_table.insert(new_malloc_sym); - return new_malloc_sym.symbol_expr(); - } - return malloc_sym->symbol_expr(); -} - bool recursive_initializationt::should_be_treated_as_array( const irep_idt &array_name) const { @@ -630,24 +612,6 @@ std::string recursive_initializationt::type2id(const typet &type) const return ""; } -symbol_exprt recursive_initializationt::get_free_function() -{ - auto free_sym = goto_model.symbol_table.lookup("free"); - if(free_sym == nullptr) - { - symbolt new_free_sym{ - "free", - code_typet{ - {code_typet::parametert{pointer_type(empty_typet{})}}, empty_typet{}}, - initialization_config.mode}; - new_free_sym.pretty_name = "free"; - new_free_sym.base_name = "free"; - goto_model.symbol_table.insert(new_free_sym); - return new_free_sym.symbol_expr(); - } - return free_sym->symbol_expr(); -} - code_blockt recursive_initializationt::build_pointer_constructor( const exprt &depth, const symbol_exprt &result) @@ -724,10 +688,13 @@ code_blockt recursive_initializationt::build_pointer_constructor( then_case.add(code_declt{local_result}); const namespacet ns{goto_model.symbol_table}; - then_case.add(code_function_callt{ + then_case.add(code_assignt{ local_result, - get_malloc_function(), - {*size_of_expr(non_const_pointer_type.base_type(), ns)}}); + side_effect_exprt{ + ID_allocate, + {*size_of_expr(non_const_pointer_type.base_type(), ns), false_exprt{}}, + non_const_pointer_type, + source_locationt::nil()}}); initialize( dereference_exprt{local_result}, plus_exprt{depth, from_integer(1, depth.type())}, @@ -869,10 +836,16 @@ code_blockt recursive_initializationt::build_dynamic_array_constructor( { body.add(code_ifthenelset{ equal_exprt{nondet_size, from_integer(array_size, nondet_size.type())}, - code_function_callt{local_result, - get_malloc_function(), - {mult_exprt{from_integer(array_size, size_type()), - *size_of_expr(element_type, ns)}}}}); + code_assignt{ + local_result, + side_effect_exprt{ + ID_allocate, + {mult_exprt{ + from_integer(array_size, size_type()), + *size_of_expr(element_type, ns)}, + false_exprt{}}, + mutable_dynamic_array_type, + source_locationt::nil()}}}); } const symbol_exprt &index_iter = get_fresh_local_symexpr("index"); @@ -942,6 +915,24 @@ bool recursive_initializationt::needs_freeing(const exprt &expr) const return true; } +code_blockt +recursive_initializationt::deallocate_code(const exprt &pointer) const +{ + code_blockt block; + const auto should_track = + get_fresh_local_typed_symexpr("mark_deallocated", bool_typet{}); + block.add(code_declt{should_track}); + const symbol_exprt deallocated = goto_model.get_symbol_table() + .lookup_ref(CPROVER_PREFIX "deallocated") + .symbol_expr(); + block.add(code_ifthenelset{ + should_track, + code_assignt{ + deallocated, + typecast_exprt::conditional_cast(pointer, deallocated.type())}}); + return block; +} + void recursive_initializationt::free_if_possible( const exprt &expr, code_blockt &body) @@ -949,11 +940,10 @@ void recursive_initializationt::free_if_possible( PRECONDITION(expr.id() == ID_symbol); const auto expr_id = to_symbol_expr(expr).get_identifier(); const auto maybe_cluster_index = find_equal_cluster(expr_id); - const auto call_free = code_function_callt{get_free_function(), {expr}}; if(!maybe_cluster_index.has_value()) { // not in any equality cluster -> just free - body.add(call_free); + body.add(deallocate_code(expr)); return; } @@ -965,7 +955,7 @@ void recursive_initializationt::free_if_possible( // in equality cluster but not common origin -> free if not equal to origin const auto condition = notequal_exprt{expr, *common_arguments_origins[*maybe_cluster_index]}; - body.add(code_ifthenelset{condition, call_free}); + body.add(code_ifthenelset{condition, deallocate_code(expr)}); } else { @@ -979,7 +969,7 @@ void recursive_initializationt::free_cluster_origins(code_blockt &body) { for(auto const &origin : common_arguments_origins) { - body.add(code_function_callt{get_free_function(), {*origin}}); + body.add(deallocate_code(*origin)); } } diff --git a/src/goto-harness/recursive_initialization.h b/src/goto-harness/recursive_initialization.h index 8f0e9145c9b..2b13ce9981b 100644 --- a/src/goto-harness/recursive_initialization.h +++ b/src/goto-harness/recursive_initialization.h @@ -98,11 +98,6 @@ class recursive_initializationt /// \param body: The code block to write initialisation code to. void initialize(const exprt &lhs, const exprt &depth, code_blockt &body); - /// Get the `free` function as symbol expression, and inserts it into the - /// goto-model if it doesn't exist already. - /// \return the symbol expression for the `free` function - symbol_exprt get_free_function(); - static bool is_initialization_allowed(const symbolt &symbol) { auto const symbol_name = id2string(symbol.name); @@ -125,11 +120,6 @@ class recursive_initializationt type_constructor_namest type_constructor_names; std::vector> common_arguments_origins; - /// Get the malloc function as symbol exprt, - /// and inserts it into the goto-model if it doesn't - /// exist already. - symbol_exprt get_malloc_function(); - bool should_be_treated_as_array(const irep_idt &pointer_name) const; std::optional find_equal_cluster(const irep_idt &name) const; @@ -275,6 +265,10 @@ class recursive_initializationt const exprt &depth, code_blockt &body, const std::vector &selection_spec); + + /// Generate code mimicking __CPROVER_deallocate (which is what C's free + /// calls) with \p pointer as argument. + code_blockt deallocate_code(const exprt &pointer) const; }; #endif // CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H