From 57acb84695a1fc8530512464f0e26b2c2af4e2c6 Mon Sep 17 00:00:00 2001 From: clexmaAtFlankerB Date: Wed, 12 Jun 2024 22:53:40 +0800 Subject: [PATCH] update --- benchmark/case_0.c | 2 +- mk_cmake.py | 4 + src/goto-symex/builtin_functions.cpp | 313 ++++++++++++------ src/goto-symex/goto_symex.h | 2 + src/goto-symex/symex_assign.cpp | 14 +- src/irep2/irep2.h | 6 +- src/irep2/irep2_expr.cpp | 2 + src/irep2/irep2_expr.h | 79 +++++ src/irep2/templates/irep2_templates.cpp | 8 + .../templates/irep2_templates_expr_data.cpp | 5 + src/util/migrate.cpp | 51 +++ src/util/std_types.h | 22 ++ 12 files changed, 404 insertions(+), 104 deletions(-) create mode 100644 mk_cmake.py diff --git a/benchmark/case_0.c b/benchmark/case_0.c index ad0a186e..7bbb0a63 100644 --- a/benchmark/case_0.c +++ b/benchmark/case_0.c @@ -2,7 +2,7 @@ int main(){ // int whatever; - int * data = malloc(sizeof(int)); + int * data = malloc(2*sizeof(int)); // // *(data + 1) = whatever; // int n = *data; // if(n > 0) { diff --git a/mk_cmake.py b/mk_cmake.py new file mode 100644 index 00000000..5a7e8d62 --- /dev/null +++ b/mk_cmake.py @@ -0,0 +1,4 @@ +import os +import sys + +os.system("cd build && cmake .. -GNinja -DBUILD_TESTING=On -DENABLE_REGRESSION=On $ESBMC_CLANG -DENABLE_Z3=On -DZ3_DIR=/../../../z3-release -DCMAKE_INSTALL_PREFIX:PATH=$PWD/../../release ") diff --git a/src/goto-symex/builtin_functions.cpp b/src/goto-symex/builtin_functions.cpp index 7f4385cb..f931ada3 100644 --- a/src/goto-symex/builtin_functions.cpp +++ b/src/goto-symex/builtin_functions.cpp @@ -147,100 +147,210 @@ expr2tc goto_symext::symex_mem( // value // TODO slhv: change to heap var declaration - symbolt symbol; + bool is_old_encoding = !options.get_bool_option("z3-slhv"); + if (is_old_encoding) { + symbolt symbol; - symbol.name = "dynamic_" + i2string(dynamic_counter) + - (size_is_one ? "_value" : "_array"); + symbol.name = "dynamic_" + i2string(dynamic_counter) + + (size_is_one ? "_value" : "_array"); - symbol.id = std::string("symex_dynamic::") + (!is_malloc ? "alloca::" : "") + - id2string(symbol.name); - symbol.lvalue = true; + symbol.id = std::string("symex_dynamic::") + (!is_malloc ? "alloca::" : "") + + id2string(symbol.name); + symbol.lvalue = true; - typet renamedtype = ns.follow(migrate_type_back(type)); - if (size_is_one) - symbol.type = renamedtype; - else - { - symbol.type = typet(typet::t_array); - symbol.type.subtype() = renamedtype; - symbol.type.size(migrate_expr_back(size)); - } + typet renamedtype = ns.follow(migrate_type_back(type)); + if (size_is_one) + symbol.type = renamedtype; + else + { + symbol.type = typet(typet::t_array); + symbol.type.subtype() = renamedtype; + symbol.type.size(migrate_expr_back(size)); + } - symbol.type.dynamic(true); + symbol.type.dynamic(true); - symbol.type.set( - "alignment", constant_exprt(config.ansi_c.max_alignment(), size_type())); + symbol.type.set( + "alignment", constant_exprt(config.ansi_c.max_alignment(), size_type())); - symbol.mode = "C"; + symbol.mode = "C"; - new_context.add(symbol); + new_context.add(symbol); - type2tc new_type = migrate_type(symbol.type); + type2tc new_type = migrate_type(symbol.type); - type2tc rhs_type; - expr2tc rhs_ptr_obj; + type2tc rhs_type; + expr2tc rhs_ptr_obj; - if (size_is_one) - { - rhs_type = migrate_type(symbol.type); - rhs_ptr_obj = symbol2tc(new_type, symbol.id); - } - else - { - type2tc subtype = migrate_type(symbol.type.subtype()); - expr2tc sym = symbol2tc(new_type, symbol.id); - expr2tc idx_val = gen_long(size->type, 0L); - expr2tc idx = index2tc(subtype, sym, idx_val); - rhs_type = migrate_type(symbol.type.subtype()); - rhs_ptr_obj = idx; - } + if (size_is_one) + { + rhs_type = migrate_type(symbol.type); + rhs_ptr_obj = symbol2tc(new_type, symbol.id); + } + else + { + type2tc subtype = migrate_type(symbol.type.subtype()); + expr2tc sym = symbol2tc(new_type, symbol.id); + expr2tc idx_val = gen_long(size->type, 0L); + expr2tc idx = index2tc(subtype, sym, idx_val); + rhs_type = migrate_type(symbol.type.subtype()); + rhs_ptr_obj = idx; + } - expr2tc rhs_addrof = address_of2tc(rhs_type, rhs_ptr_obj); + expr2tc rhs_addrof = address_of2tc(rhs_type, rhs_ptr_obj); - expr2tc rhs = rhs_addrof; - expr2tc ptr_rhs = rhs; - guardt alloc_guard = cur_state->guard; + expr2tc rhs = rhs_addrof; + expr2tc ptr_rhs = rhs; + guardt alloc_guard = cur_state->guard; - if (options.get_bool_option("malloc-zero-is-null")) - { - expr2tc null_sym = symbol2tc(rhs->type, "NULL"); - expr2tc choice = greaterthan2tc(size, gen_long(size->type, 0)); - alloc_guard.add(choice); - rhs = if2tc(rhs->type, choice, rhs, null_sym); - } + if (options.get_bool_option("malloc-zero-is-null")) + { + expr2tc null_sym = symbol2tc(rhs->type, "NULL"); + expr2tc choice = greaterthan2tc(size, gen_long(size->type, 0)); + alloc_guard.add(choice); + rhs = if2tc(rhs->type, choice, rhs, null_sym); + } - if (!options.get_bool_option("force-malloc-success") && is_malloc) - { - expr2tc null_sym = symbol2tc(rhs->type, "NULL"); - expr2tc choice = sideeffect2tc( - get_bool_type(), - expr2tc(), - expr2tc(), - std::vector(), - type2tc(), - sideeffect2t::nondet); - replace_nondet(choice); - - rhs = if2tc(rhs->type, choice, rhs, null_sym); - alloc_guard.add(choice); - - ptr_rhs = rhs; - } + if (!options.get_bool_option("force-malloc-success") && is_malloc) + { + expr2tc null_sym = symbol2tc(rhs->type, "NULL"); + expr2tc choice = sideeffect2tc( + get_bool_type(), + expr2tc(), + expr2tc(), + std::vector(), + type2tc(), + sideeffect2t::nondet); + replace_nondet(choice); - if (rhs->type != lhs->type) - rhs = typecast2tc(lhs->type, rhs); + rhs = if2tc(rhs->type, choice, rhs, null_sym); + alloc_guard.add(choice); - cur_state->rename(rhs); - expr2tc rhs_copy(rhs); - log_status("symex assign in symex_mem"); - symex_assign(code_assign2tc(lhs, rhs), true); + ptr_rhs = rhs; + } - expr2tc ptr_obj = pointer_object2tc(pointer_type2(), ptr_rhs); - track_new_pointer(ptr_obj, new_type); - dynamic_memory.emplace_back( - rhs_copy, alloc_guard, !is_malloc, symbol.name.as_string()); + if (rhs->type != lhs->type) + rhs = typecast2tc(lhs->type, rhs); + + cur_state->rename(rhs); + expr2tc rhs_copy(rhs); + log_status("symex assign in symex_mem: lhs = &allocated_array[index0]"); + symex_assign(code_assign2tc(lhs, rhs), true); + + expr2tc ptr_obj = pointer_object2tc(pointer_type2(), ptr_rhs); + track_new_pointer(ptr_obj, new_type); + dynamic_memory.emplace_back( + rhs_copy, alloc_guard, !is_malloc, symbol.name.as_string()); + + return to_address_of2t(rhs_addrof).ptr_obj; + + } else { + unsigned int &dynamic_counter = get_dynamic_counter(); + dynamic_counter++; + + // value + symbolt symbol; + symbol.name = "dynamic_heaplet_"+ i2string(dynamic_counter); + + symbol.id = std::string("symex_dynamic::") + (!is_malloc ? "alloca::" : "") + + id2string(symbol.name); + symbol.lvalue = true; + + symbol.type = typet(typet::t_intheap); + symbol.type.size(migrate_expr_back(size)); + + symbol.type.dynamic(true); + symbol.mode = "C"; + new_context.add(symbol); + + type2tc heap_type = get_intheap_type(); + expr2tc allocated_heap = symbol2tc(heap_type, symbol.id); + std::vector pts; + expr2tc size_simplified = size.simplify(); + guardt alloc_guard = cur_state->guard; + // TODO SLHV: add size simplification later + if(!is_constant_int2t(size_simplified)) { + log_error("Currently does not support constant size"); + assert(false); + } + log_status("dump alloc size: "); + size_simplified->dump(); + constant_int2t constant_size = to_constant_int2t(size_simplified); + unsigned usize = constant_size.as_ulong(); + log_status("Unsiged size: {}", usize); + + expr2tc alloc_base_addr = lhs; + expr2tc heaplet; + bool need_heap_assignment = false; + if(usize == 0) { + log_status("zero size"); + // We can do nothing + expr2tc null_loc = constant_intloc2tc(get_intloc_type(), BigInt(0)); + + + } else if(usize == 1) { + log_status("single byte points_to"); + need_heap_assignment = true; + expr2tc addr = alloc_base_addr; + expr2tc fresh_data_symbol = sideeffect2tc( + get_int8_type(), + expr2tc(), + expr2tc(), + std::vector(), + type2tc(), + sideeffect2t::nondet); + heaplet = points_to2tc(get_intheap_type(), addr, fresh_data_symbol, false); + } else { + std::vector pt_vec; + expr2tc first_addr = alloc_base_addr; + expr2tc first_fresh_data = sideeffect2tc( + get_int8_type(), + expr2tc(), + expr2tc(), + std::vector(), + type2tc(), + sideeffect2t::nondet); + expr2tc first_pt = points_to2tc(get_intheap_type(), first_addr, first_fresh_data, false); + pt_vec.push_back(first_pt); + for(unsigned i = 1; i < usize; i ++) { + expr2tc offset = constant_int2tc(int_type2(), BigInt(i)); + expr2tc addr_i = locadd2tc(get_intloc_type(), first_addr, offset); + expr2tc fresh_data_i = sideeffect2tc( + get_int8_type(), + expr2tc(), + expr2tc(), + std::vector(), + type2tc(), + sideeffect2t::nondet); + expr2tc pt_i = points_to2tc(get_intheap_type(), addr_i, fresh_data_i, false); + pt_vec.push_back(pt_i); + } + + heaplet = uplus2tc(get_intheap_type(), pt_vec); + log_status("multi byte points_to"); + need_heap_assignment = true; + } + cur_state->rename(alloc_base_addr); + expr2tc alloc_base_addr_copy(alloc_base_addr); + if(need_heap_assignment) { + log_status("symex assign in symex_mem: allocated_heap = heaplet"); + symex_assign(code_assign2tc(allocated_heap, heaplet)); + } + + // TODO: modify the pointer tracker here + expr2tc ptr_obj = pointer_object2tc(pointer_type2(), alloc_base_addr); + track_new_pointer(ptr_obj, get_intheap_type(), size_simplified); + dynamic_memory.emplace_back( + alloc_base_addr_copy, + alloc_guard, + !is_malloc, + symbol.name.as_string() + ); + + return expr2tc(); + } - return to_address_of2t(rhs_addrof).ptr_obj; + } void goto_symext::track_new_pointer( @@ -248,29 +358,40 @@ void goto_symext::track_new_pointer( const type2tc &new_type, const expr2tc &size) { + bool is_old_encoding = !options.get_bool_option("z3-slhv"); // Also update all the accounting data. // Mark that object as being dynamic, in the __ESBMC_is_dynamic array - type2tc sym_type = array_type2tc(get_bool_type(), expr2tc(), true); - expr2tc sym = symbol2tc(sym_type, dyn_info_arr_name); - - expr2tc idx = index2tc(get_bool_type(), sym, ptr_obj); - expr2tc truth = gen_true_expr(); - symex_assign(code_assign2tc(idx, truth), true); - - expr2tc valid_sym = symbol2tc(sym_type, valid_ptr_arr_name); - expr2tc valid_index_expr = index2tc(get_bool_type(), valid_sym, ptr_obj); - truth = gen_true_expr(); - symex_assign(code_assign2tc(valid_index_expr, truth), true); - - type2tc sz_sym_type = array_type2tc(size_type2(), expr2tc(), true); - expr2tc sz_sym = symbol2tc(sz_sym_type, alloc_size_arr_name); - expr2tc sz_index_expr = index2tc(size_type2(), sz_sym, ptr_obj); - - expr2tc object_size_exp = - is_nil_expr(size) ? type_byte_size_expr(new_type) : size; - - symex_assign(code_assign2tc(sz_index_expr, object_size_exp), true); + if(is_old_encoding) { + type2tc sym_type = array_type2tc(get_bool_type(), expr2tc (), true); + expr2tc sym = symbol2tc(sym_type, dyn_info_arr_name); + + expr2tc idx = index2tc(get_bool_type(), sym, ptr_obj); + expr2tc truth = gen_true_expr(); + symex_assign(code_assign2tc(idx, truth), true); + + expr2tc valid_sym = symbol2tc(sym_type, valid_ptr_arr_name); + expr2tc valid_index_expr = index2tc(get_bool_type(), valid_sym, ptr_obj); + truth = gen_true_expr(); + symex_assign(code_assign2tc(valid_index_expr, truth), true); + + type2tc sz_sym_type = array_type2tc(size_type2(), expr2tc(), true); + expr2tc sz_sym = symbol2tc(sz_sym_type, alloc_size_arr_name); + expr2tc sz_index_expr = index2tc(size_type2(), sz_sym, ptr_obj); + + expr2tc object_size_exp = + is_nil_expr(size) ? type_byte_size_expr(new_type) : size; + + symex_assign(code_assign2tc(sz_index_expr, object_size_exp), true); + } else { + type2tc allocsize_heap_type = get_intheap_type(); + expr2tc allocsize_symbol = symbol2tc(allocsize_heap_type, alloc_size_heap_name); + // TODO SLHV: add non-constant size later + assert(is_constant_int2t(size)); + + expr2tc updated_heap = heap_update2tc(allocsize_heap_type, allocsize_symbol, ptr_obj, size, 4); + symex_assign(code_assign2tc(allocsize_symbol, updated_heap), true); + } } void goto_symext::symex_free(const expr2tc &expr) diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 01829f55..71e2513b 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -834,6 +834,8 @@ class goto_symext * modelling what pointers are active, which are freed, and so forth. They * can change between C and C++, unfortunately. */ irep_idt valid_ptr_arr_name, alloc_size_arr_name, dyn_info_arr_name; + /* Symbol names for modelling auxillary heap*/ + irep_idt alloc_size_heap_name; /** List of all allocated objects. * Used to track what we should level memory-leak-assertions against when the * program execution has finished */ diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 1832263c..6ad44963 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -66,6 +66,7 @@ goto_symext::goto_symext( valid_ptr_arr_name = "c:@__ESBMC_alloc"; alloc_size_arr_name = "c:@__ESBMC_alloc_size"; dyn_info_arr_name = "c:@__ESBMC_is_dynamic"; + alloc_size_heap_name = "c:@__ESBMC_heap_alloc_size"; symbolt sym; sym.id = "symex_throw::thrown_obj"; @@ -167,20 +168,22 @@ void goto_symext::symex_assign( // printf expression that has lhs if (is_code_printf2t(rhs)) { - symex_printf(lhs, rhs); + log_error("does not support code printf in assign"); + // symex_printf(lhs, rhs); } if (is_sideeffect2t(rhs)) { // check what symex_mem represent - log_status("is side effect rhs "); + log_status("is side effect rhs::::::::::::::::: "); const sideeffect2t &effect = to_sideeffect2t(rhs); - // effect.dump(); + effect.dump(); switch (effect.kind) { case sideeffect2t::cpp_new: case sideeffect2t::cpp_new_arr: - symex_cpp_new(lhs, effect); + log_error("does not support va_arg cpp new"); + // symex_cpp_new(lhs, effect); break; case sideeffect2t::realloc: symex_realloc(lhs, effect); @@ -192,7 +195,8 @@ void goto_symext::symex_assign( symex_alloca(lhs, effect); break; case sideeffect2t::va_arg: - symex_va_arg(lhs, effect); + log_error("does not support va_arg sideeffect"); + // symex_va_arg(lhs, effect); break; case sideeffect2t::printf2: // do nothing here diff --git a/src/irep2/irep2.h b/src/irep2/irep2.h index 4a8439d3..26403957 100644 --- a/src/irep2/irep2.h +++ b/src/irep2/irep2.h @@ -103,8 +103,10 @@ BOOST_PP_LIST_CONS(with, \ BOOST_PP_LIST_CONS(member, \ BOOST_PP_LIST_CONS(index, \ - BOOST_PP_LIST_CONS(points_to, \ + BOOST_PP_LIST_CONS(points_to, \ BOOST_PP_LIST_CONS(uplus, \ + BOOST_PP_LIST_CONS(locadd, \ + BOOST_PP_LIST_CONS(heap_update, \ BOOST_PP_LIST_CONS(isnan, \ BOOST_PP_LIST_CONS(overflow, \ BOOST_PP_LIST_CONS(overflow_cast, \ @@ -145,7 +147,7 @@ BOOST_PP_LIST_CONS(signbit, \ BOOST_PP_LIST_CONS(concat, \ BOOST_PP_LIST_CONS(extract, \ - BOOST_PP_LIST_NIL)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + BOOST_PP_LIST_NIL)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) #define ESBMC_LIST_OF_TYPES \ BOOST_PP_LIST_CONS(bool, \ diff --git a/src/irep2/irep2_expr.cpp b/src/irep2/irep2_expr.cpp index 55dd0ca8..0b1efc5b 100644 --- a/src/irep2/irep2_expr.cpp +++ b/src/irep2/irep2_expr.cpp @@ -76,6 +76,8 @@ static const char *expr_names[] = { "index", "points_to", "uplus", + "locadd", + "heap_update", "isnan", "overflow", "overflow_cast", diff --git a/src/irep2/irep2_expr.h b/src/irep2/irep2_expr.h index cf2d65ad..6a9f4523 100644 --- a/src/irep2/irep2_expr.h +++ b/src/irep2/irep2_expr.h @@ -956,6 +956,63 @@ class uplus_data : public expr2t }; +class locadd_data : public expr2t +{ +public: + locadd_data( + const type2tc &t, + datatype_ops::expr_ids id, + expr2tc base_addr, + expr2tc added) : expr2t(t, id), base_addr(base_addr), added_num(added) + { + + } + expr2tc base_addr; + expr2tc added_num; + + // Type mangling: + typedef esbmct::field_traits + locadd_base_addr_field; + typedef esbmct::field_traits + locadd_added_num_field; + typedef esbmct::expr2t_traits traits; + +}; + +class heap_update_data : public expr2t +{ +public: + heap_update_data( + const type2tc &t, + datatype_ops::expr_ids id, + expr2tc source_val, + expr2tc start_addr, + expr2tc updated_val, + unsigned int byte_len + ) : expr2t(t, id), src_heap(source_val), start_addr(start_addr), updated_val(updated_val), byte_len(byte_len){} + + expr2tc src_heap; + expr2tc start_addr; + expr2tc updated_val; + unsigned int byte_len; + + + // Type mangling: + typedef esbmct::field_traits + heap_update_data_src_heap_field; + typedef esbmct::field_traits + heap_update_data_start_addr_field; + typedef esbmct::field_traits + heap_update_data_updated_val_field; + typedef esbmct::field_traits + heap_update_data_byte_len_field; + typedef esbmct::expr2t_traits + < + heap_update_data_src_heap_field, heap_update_data_start_addr_field, heap_update_data_updated_val_field, heap_update_data_byte_len_field + > traits; + +}; + class string_ops : public expr2t { public: @@ -1584,6 +1641,8 @@ irep_typedefs(member, member_data); irep_typedefs(index, index_data); irep_typedefs(points_to, points_to_data); irep_typedefs(uplus, uplus_data); +irep_typedefs(locadd, locadd_data); +irep_typedefs(heap_update, heap_update_data); irep_typedefs(isnan, bool_1op); irep_typedefs(overflow, overflow_ops); irep_typedefs(overflow_cast, overflow_cast_data); @@ -3068,6 +3127,26 @@ class uplus2t : public uplus_expr_methods }; +class locadd2t : public locadd_expr_methods +{ +public: + locadd2t(const type2tc &type, expr2tc base_addr, expr2tc added) : locadd_expr_methods(type, locadd_id, base_addr, added) {} + locadd2t(const locadd2t &ref) = default; + + + + static std::string field_names[esbmct::num_type_fields]; +}; + +class heap_update2t : public heap_update_expr_methods +{ + public: + heap_update2t(const type2tc &type, expr2tc source_heap, expr2tc start_addr, expr2tc updated_val, unsigned int byte_len) : heap_update_expr_methods(type, heap_update_id, source_heap, start_addr, updated_val, byte_len){} + heap_update2t(const heap_update2t &ref) = default; + + static std::string field_names[esbmct::num_type_fields]; +}; + /** Is operand not-a-number. Used to implement C library isnan function for * float/double values. Boolean result. @extends arith_1op */ class isnan2t : public isnan_expr_methods diff --git a/src/irep2/templates/irep2_templates.cpp b/src/irep2/templates/irep2_templates.cpp index 7ed3de87..059d10f0 100644 --- a/src/irep2/templates/irep2_templates.cpp +++ b/src/irep2/templates/irep2_templates.cpp @@ -160,6 +160,14 @@ std::string member2t::field_names[esbmct::num_type_fields] = {"source_value", "member_name", "", "", ""}; std::string index2t::field_names[esbmct::num_type_fields] = {"source_value", "index", "", "", ""}; +std::string uplus2t::field_names[esbmct::num_type_fields] = +{"uplus_members", "uplus_num", "", "", ""}; +std::string points_to2t::field_names[esbmct::num_type_fields] = +{"addr", "content", "is_loc", "", ""}; +std::string locadd2t::field_names[esbmct::num_type_fields] = +{"baseaddr", "added_num", "", "", ""}; +std::string heap_update2t::field_names[esbmct::num_type_fields] = +{"src_heap", "start_addr", "updated_val", "byte_len", ""}; std::string isnan2t::field_names[esbmct::num_type_fields] = {"value", "", "", "", ""}; std::string overflow2t::field_names[esbmct::num_type_fields] = diff --git a/src/irep2/templates/irep2_templates_expr_data.cpp b/src/irep2/templates/irep2_templates_expr_data.cpp index a6437569..49fb11a9 100644 --- a/src/irep2/templates/irep2_templates_expr_data.cpp +++ b/src/irep2/templates/irep2_templates_expr_data.cpp @@ -1,6 +1,7 @@ #include expr_typedefs1(constant_int, constant_int_data); +expr_typedefs1(constant_intloc, constant_intloc_data); expr_typedefs1(constant_fixedbv, constant_fixedbv_data); expr_typedefs1(constant_floatbv, constant_floatbv_data); expr_typedefs1(constant_struct, constant_datatype_data); @@ -27,6 +28,10 @@ expr_typedefs4(byte_update, byte_update_data); expr_typedefs3(with, with_data); expr_typedefs2(member, member_data); expr_typedefs2(index, index_data); +expr_typedefs3(points_to, points_to_data); +expr_typedefs2(uplus, uplus_data); +expr_typedefs2(locadd, locadd_data); +expr_typedefs4(heap_update, heap_update_data); expr_typedefs2(overflow_cast, overflow_cast_data); expr_typedefs3(dynamic_object, dynamic_object_data); expr_typedefs2(dereference, dereference_data); diff --git a/src/util/migrate.cpp b/src/util/migrate.cpp index a66d495b..b96bc0e9 100644 --- a/src/util/migrate.cpp +++ b/src/util/migrate.cpp @@ -145,6 +145,12 @@ static type2tc migrate_type0(const typet &type) if (type.id() == typet::t_empty) return get_empty_type(); + + if (type.id() == typet::t_intheap) + return get_intheap_type(); + + if (type.id() == typet::t_intloc) + return get_intloc_type(); if (type.id() == typet::t_symbol) return symbol_type2tc(type.identifier()); @@ -1827,6 +1833,10 @@ typet migrate_type_back(const type2tc &ref) return bool_typet(); case type2t::empty_id: return empty_typet(); + case type2t::intheap_id: + return intheap_typet(); + case type2t::intloc_id: + return intloc_typet(); case type2t::symbol_id: { const symbol_type2t &ref2 = to_symbol_type(ref); @@ -2579,6 +2589,47 @@ exprt migrate_expr_back(const expr2tc &ref) migrate_expr_back(ref2.source_value), migrate_expr_back(ref2.index)); return index; } + case expr2t::uplus_id: + { + const uplus2t & ref2 = to_uplus2t(ref); + typet thetype = migrate_type_back(ref->type); + exprt uplus("uplus", thetype); + for(expr2tc op2 : ref2.uplus_members) { + uplus.copy_to_operands(migrate_expr_back(op2)); + } + return uplus; + } + case expr2t::locadd_id: + { + const locadd2t &ref2 = to_locadd2t(ref); + typet thetype = migrate_type_back(ref->type); + exprt locadd("locadd", thetype); + locadd.copy_to_operands(migrate_expr_back(ref2.base_addr)); + locadd.copy_to_operands(migrate_expr_back(ref2.added_num)); + return locadd; + } + case expr2t::heap_update_id: + { + const heap_update2t &ref2 = to_heap_update2t(ref); + typet thetype = migrate_type_back(ref->type); + exprt heap_update("heap_update", thetype); + heap_update.copy_to_operands(migrate_expr_back(ref2.src_heap)); + heap_update.copy_to_operands(migrate_expr_back(ref2.start_addr)); + heap_update.copy_to_operands(migrate_expr_back(ref2.updated_val)); + heap_update.set("byte_len", irep_idt(std::to_string(ref2.byte_len))); + return heap_update; + } + case expr2t::points_to_id: + { + const points_to2t &ref2 = to_points_to2t(ref); + typet thetype = migrate_type_back(ref->type); + exprt pt("points_to", thetype); + pt.copy_to_operands( + migrate_expr_back(ref2.addr), + migrate_expr_back(ref2.content) + ); + return pt; + } case expr2t::isnan_id: { const isnan2t &ref2 = to_isnan2t(ref); diff --git a/src/util/std_types.h b/src/util/std_types.h index 1672a7ac..85d6b1ad 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -24,6 +24,28 @@ class empty_typet : public typet } }; + +class intheap_typet : public typet +{ +public: + intheap_typet() + { + id(t_intheap); + } +}; + + +class intloc_typet : public typet +{ +public: + intloc_typet() + { + id(t_intloc); + } +}; + + + class symbol_typet : public typet { public: