intheap and intloc added, uplus, points-to and emp added

benchmark/case_0.c

@@ -1,12 +1,11 @@
 #include <stdlib.h>
 
 int main(){
-    int whatever;
+    // int whatever;
     int * data = malloc(sizeof(int));
-    int data2[10];
-    *(data + 1) = whatever;
-    int n = *(data + 1);
-    if(n > 0) {
-        free(data);
-    }
+    // // *(data + 1) = whatever;
+    // int n = *data;
+    // if(n > 0) {
+    //     free(data);
+    // }
 }

src/goto-symex/builtin_functions.cpp

@@ -237,7 +237,6 @@ expr2tc goto_symext::symex_mem(
 
   expr2tc ptr_obj = pointer_object2tc(pointer_type2(), ptr_rhs);
   track_new_pointer(ptr_obj, new_type);
-  ptr_obj->dump();
   dynamic_memory.emplace_back(
     rhs_copy, alloc_guard, !is_malloc, symbol.name.as_string());
 

src/goto-symex/symex_assign.cpp

@@ -169,15 +169,11 @@ void goto_symext::symex_assign(
   {
     symex_printf(lhs, rhs);
   }
-  // log_status("ZZZZZZZZZZ assign lhs after dereference and replace: ");
-  // lhs->dump();
-  // log_status("ZZZZZZZZZZ assign rhs after dereference and replace: ");
-  // rhs->dump();
   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();
     switch (effect.kind)
@@ -235,46 +231,57 @@ void goto_symext::symex_assign_rec(
 {
   if (is_symbol2t(lhs))
   {
+    log_status("symex_assign_symbol");
     symex_assign_symbol(lhs, full_lhs, rhs, full_rhs, guard, hidden);
   }
   else if (is_index2t(lhs))
   {
+    log_status("symex_assign_array");
     symex_assign_array(lhs, full_lhs, rhs, full_rhs, guard, hidden);
   }
   else if (is_member2t(lhs))
   {
+    log_status("symex_assign_member");
     symex_assign_member(lhs, full_lhs, rhs, full_rhs, guard, hidden);
   }
   else if (is_if2t(lhs))
   {
+    log_status("symex_assign_if");
     symex_assign_if(lhs, full_lhs, rhs, full_rhs, guard, hidden);
   }
   else if (is_typecast2t(lhs) || is_bitcast2t(lhs))
   {
+    log_status("symex_assign_typecast");
     symex_assign_typecast(lhs, full_lhs, rhs, full_rhs, guard, hidden);
   }
   else if (is_constant_string2t(lhs) || is_null_object2t(lhs))
   {
+    log_status("is_constant_string2t(lhs) || is_null_object2t(lhs)");
     // ignore
   }
   else if (is_byte_extract2t(lhs))
   {
+    log_status("symex_assign_byte_extract");
     symex_assign_byte_extract(lhs, full_lhs, rhs, full_rhs, guard, hidden);
   }
   else if (is_concat2t(lhs))
   {
+    log_status("symex_assign_concat");
     symex_assign_concat(lhs, full_lhs, rhs, full_rhs, guard, hidden);
   }
   else if (is_constant_struct2t(lhs))
   {
+    log_status("symex_assign_structure");
     symex_assign_structure(lhs, full_lhs, rhs, full_rhs, guard, hidden);
   }
   else if (is_extract2t(lhs))
   {
+    log_status("symex_assign_extract");
     symex_assign_extract(lhs, full_lhs, rhs, full_rhs, guard, hidden);
   }
   else if (is_bitand2t(lhs))
   {
+    log_status("symex_assign_bitfield");
     symex_assign_bitfield(lhs, full_lhs, rhs, full_rhs, guard, hidden);
   }
   else

src/irep2/irep2.h

@@ -40,6 +40,8 @@
 // clang-format off
 #define ESBMC_LIST_OF_EXPRS                                                    \
   BOOST_PP_LIST_CONS(constant_int,                                             \
+  BOOST_PP_LIST_CONS(constant_intloc,                                          \
+  BOOST_PP_LIST_CONS(constant_intheap,                                          \
   BOOST_PP_LIST_CONS(constant_fixedbv,                                         \
   BOOST_PP_LIST_CONS(constant_floatbv,                                         \
   BOOST_PP_LIST_CONS(constant_bool,                                            \
@@ -101,6 +103,8 @@
   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(uplus,                                                    \
   BOOST_PP_LIST_CONS(isnan,                                                    \
   BOOST_PP_LIST_CONS(overflow,                                                 \
   BOOST_PP_LIST_CONS(overflow_cast,                                            \
@@ -141,7 +145,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,                                                     \
@@ -158,8 +162,10 @@
   BOOST_PP_LIST_CONS(fixedbv,                                                  \
   BOOST_PP_LIST_CONS(string,                                                   \
   BOOST_PP_LIST_CONS(cpp_name,                                                 \
-  BOOST_PP_LIST_NIL))))))))))))))
-// clang-format on
+  BOOST_PP_LIST_CONS(intheap,                                                  \
+  BOOST_PP_LIST_CONS(intloc,                                                  \
+  BOOST_PP_LIST_NIL))))))))))))))))
+// clang-format ondata
 
 // Even crazier forward decs,
 namespace esbmct
@@ -424,6 +430,8 @@ class type2t : public irep2t
     fixedbv_id,
     floatbv_id,
     cpp_name_id,
+    intheap_id,
+    intloc_id,
     end_type_id
   };
 

src/irep2/irep2_expr.cpp

@@ -11,6 +11,8 @@
 
 static const char *expr_names[] = {
   "constant_int",
+  "constant_intloc",
+  "constant_intheap",
   "constant_fixedbv",
   "constant_floatbv",
   "constant_bool",
@@ -72,6 +74,8 @@ static const char *expr_names[] = {
   "with",
   "member",
   "index",
+  "points_to",
+  "uplus",
   "isnan",
   "overflow",
   "overflow_cast",

src/irep2/irep2_expr.h

@@ -48,6 +48,48 @@ class constant_int_data : public constant2t
   typedef esbmct::expr2t_traits<value_field> traits;
 };
 
+
+
+class constant_intloc_data : public constant2t 
+{
+
+public:
+  constant_intloc_data(const type2tc &t, expr2t::expr_ids id, const BigInt &bint)
+    : constant2t(t, id), value(bint)
+  {
+  }
+  constant_intloc_data(const constant_intloc_data &ref) = default;
+
+  BigInt value;
+
+  // Type mangling:
+  typedef esbmct::
+    field_traits<BigInt, constant_intloc_data, &constant_intloc_data::value>
+      value_field;
+  typedef esbmct::expr2t_traits<value_field> traits;
+};
+
+
+class constant_intheap_data : public constant2t 
+{
+
+public:
+  constant_intheap_data(const type2tc &t, expr2t::expr_ids id, const bool e)
+    : constant2t(t, id), is_emp(e)
+  {
+  }
+  constant_intheap_data(const constant_intheap_data &ref) = default;
+
+  bool is_emp;
+
+  // Type mangling:
+  typedef esbmct::
+    field_traits<bool, constant_intheap_data, &constant_intheap_data::is_emp>
+      value_field;
+  typedef esbmct::expr2t_traits<value_field> traits;
+};
+
+
 class constant_fixedbv_data : public constant2t
 {
 public:
@@ -857,6 +899,63 @@ class index_data : public datatype_ops
   typedef esbmct::expr2t_traits<source_value_field, index_field> traits;
 };
 
+class points_to_data : public expr2t 
+{
+public:
+  points_to_data(
+    const type2tc &t,
+    datatype_ops::expr_ids id,
+    const expr2tc &addrloc,
+    const expr2tc &content,
+    bool is_loc) : expr2t(t, id), addr(addrloc), content(content), is_loc_content(is_loc) {
+
+    }
+  points_to_data(const points_to_data& ref) = default;
+
+
+  expr2tc addr;
+  expr2tc content;
+  bool is_loc_content;
+
+  // Type mangling:
+  typedef esbmct::field_traits<expr2tc, points_to_data, &points_to_data::addr>
+    addr_field;
+  typedef esbmct::field_traits<expr2tc, points_to_data, &points_to_data::content>
+    content_field;
+  typedef esbmct::field_traits<bool, points_to_data, &points_to_data::is_loc_content>
+    is_loc_content_field;
+  typedef esbmct::expr2t_traits<addr_field, content_field, is_loc_content_field> traits;
+
+};
+
+
+class uplus_data : public expr2t
+{
+public:
+
+  uplus_data(
+    const type2tc &t,
+    datatype_ops::expr_ids id,
+    std::vector<expr2tc> members, 
+    unsigned int m_num) : expr2t(t, id), uplus_members(std::move(members)), member_num(m_num) 
+    {
+
+    }
+  uplus_data(const uplus_data& ref) = default;
+
+
+  std::vector<expr2tc> uplus_members;
+  unsigned int member_num;
+
+  // Type mangling:
+  typedef esbmct::field_traits<std::vector<expr2tc>, uplus_data, &uplus_data::uplus_members>
+    uplus_members_field;
+  typedef esbmct::field_traits<unsigned int, uplus_data, &uplus_data::member_num>
+    member_num_field;
+  typedef esbmct::expr2t_traits<uplus_members_field, member_num_field> traits;
+
+};
+
 class string_ops : public expr2t
 {
 public:
@@ -1423,6 +1522,8 @@ class extract_data : public expr2t
 // magic because the mapping between top level expr class and it's data holding
 // object isn't regular: the data class depends on /what/ the expression /is/.
 irep_typedefs(constant_int, constant_int_data);
+irep_typedefs(constant_intloc, constant_intloc_data);
+irep_typedefs(constant_intheap, constant_intheap_data);
 irep_typedefs(constant_fixedbv, constant_fixedbv_data);
 irep_typedefs(constant_floatbv, constant_floatbv_data);
 irep_typedefs(constant_struct, constant_datatype_data);
@@ -1481,6 +1582,8 @@ irep_typedefs(byte_update, byte_update_data);
 irep_typedefs(with, with_data);
 irep_typedefs(member, member_data);
 irep_typedefs(index, index_data);
+irep_typedefs(points_to, points_to_data);
+irep_typedefs(uplus, uplus_data);
 irep_typedefs(isnan, bool_1op);
 irep_typedefs(overflow, overflow_ops);
 irep_typedefs(overflow_cast, overflow_cast_data);
@@ -1552,6 +1655,28 @@ class constant_int2t : public constant_int_expr_methods
   static std::string field_names[esbmct::num_type_fields];
 };
 
+class constant_intloc2t : public constant_intloc_expr_methods
+{
+  public:
+  constant_intloc2t(const type2tc &type, const BigInt &input)
+    : constant_intloc_expr_methods(type, constant_intloc_id, input)
+  {
+  }
+  unsigned long as_ulong() const;
+  static std::string field_names[esbmct::num_type_fields];
+};
+
+class constant_intheap2t : public constant_intheap_expr_methods
+{
+  public:
+  constant_intheap2t(const type2tc &type, bool is_emp)
+    : constant_intheap_expr_methods(type, constant_intheap_id, is_emp)
+  {
+  }
+  bool get_is_emp() const;
+  static std::string field_names[esbmct::num_type_fields];
+};
+
 /** Constant fixedbv class. Records a fixed-width number in what I assume
  *  to be mantissa/exponent form, but which is described throughout CBMC code
  *  as fraction/integer parts. Stored in a fixedbvt.
@@ -2915,6 +3040,34 @@ class index2t : public index_expr_methods
   static std::string field_names[esbmct::num_type_fields];
 };
 
+class points_to2t : public points_to_expr_methods
+{
+public:
+  points_to2t(const type2tc &type, const expr2tc addr, const expr2tc& content, bool is_loc) : points_to_expr_methods(type, points_to_id, addr, content, is_loc) {
+
+  }
+  points_to2t(const points_to2t &ref) = default;
+
+
+  static std::string field_names[esbmct::num_type_fields];
+
+};
+
+
+class uplus2t : public uplus_expr_methods
+{
+public:
+  uplus2t(const type2tc &type, 
+  std::vector<expr2tc> uplus_members) : uplus_expr_methods(type, uplus_id, std::move(uplus_members), uplus_members.size()) {
+
+  }
+  uplus2t(const uplus2t &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

src/irep2/irep2_type.cpp

@@ -27,6 +27,8 @@ static const char *type_names[] = {
   "signedbv",
   "fixedbv",
   "floatbv",
+  "intheap",
+  "intloc",
   "cpp_name"};
 // If this fires, you've added/removed a type id, and need to update the list
 // above (which is ordered according to the enum list)
@@ -181,6 +183,14 @@ unsigned int empty_type2t::get_width() const
 {
   throw symbolic_type_excp();
 }
+unsigned int intheap_type2t::get_width() const
+{
+  throw symbolic_type_excp();
+}
+unsigned int intloc_type2t::get_width() const
+{
+  throw symbolic_type_excp();
+}
 
 unsigned int symbol_type2t::get_width() const
 {