Deactivating field-sensitivity in Cprover 5.12

[sepideha]

We have a BMC tool (UpProver & HiFrog) relies on Cprover 5.12 framework for generating GOTO-programs/SSA encoding. We recently upgraded the frontend of our tool from CPROVER 5.10 to 5.12. After this upgrade our tool hits a failure in invariant check in verifying programs with struct or array, for e.g.,

Reason: value_sett::assign types should match
rhs.type(): struct_tag but lhs.type(): struct
For our application we'd need to avoid constant-propagation due to preserving local variables inside functions. When verifying a program with struct we would like to disable field-sensitive L2 SSA renaming and constant propagation.

I tried the followings but didn't help:

1. using --no-propagation option or options.set_option("propagation", false)
2. constant_propagation(options.get_bool_option("no-propagation"))
3. commenting #define ENABLE_ARRAY_FIELD_SENSITIVITY
4. setting run_apply = false

I am wondering if there is a way to disable "field-sensitive level-2 SSA renaming" within Cprover5.12 framework and keep the old style of handling structs?
If not, is there a stable point right before introducing field-sensitivity that we can downgrade to? (I hope it's not that distant like v. 5.11 released on in Dec 2018 compared to our current v.512 in Feb 2020)

C example:

struct S{
int x;
int y;
};

struct S s;

f(){
s.x = 0;
}

void main(){
s.x = 1;
s.y = 2;
f();
assert(s.x == 0);
}

[martin-cs]

Paging @tautschnig

[tautschnig]

Hi, Disabling constant propagation was broken up until #5682.

That said, you'll want the following patch to disable field sensitivity in the latest version (if possible, please try to upgrade to a very recent version, lots of bugs have been fixed since February 2020):

diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp
index 15d0415c99..65d23d2d90 100644
--- a/src/goto-symex/field_sensitivity.cpp
+++ b/src/goto-symex/field_sensitivity.cpp
@@ -158,6 +158,7 @@ exprt field_sensitivityt::get_fields(
   goto_symex_statet &state,
   const ssa_exprt &ssa_expr) const
 {
+  return ssa_expr;
   if(ssa_expr.type().id() == ID_struct || ssa_expr.type().id() == ID_struct_tag)
   {
     const struct_typet &type = to_struct_type(ns.follow(ssa_expr.type()));
@@ -349,6 +350,7 @@ void field_sensitivityt::field_assignments_rec(

 bool field_sensitivityt::is_divisible(const ssa_exprt &expr) const
 {
+  return false;
   if(expr.type().id() == ID_struct || expr.type().id() == ID_struct_tag)
     return true;

diff --git a/src/goto-symex/field_sensitivity.h b/src/goto-symex/field_sensitivity.h
index 3beff93480..e2da40339e 100644
--- a/src/goto-symex/field_sensitivity.h
+++ b/src/goto-symex/field_sensitivity.h
@@ -152,7 +152,7 @@ public:

 private:
   /// whether or not to invoke \ref field_sensitivityt::apply
-  bool run_apply = true;
+  bool run_apply = false;

   const std::size_t max_field_sensitivity_array_size;

diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index f533be1085..8366946780 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -224,7 +224,7 @@ void symex_assignt::assign_symbol(
   const exprt::operandst &guard)
 {
   // Shortcut the common case of a whole-struct initializer:
-  if(rhs.id() == ID_struct)
+  if(rhs.id() == ID_struct && state.field_sensitivity.is_divisible(lhs))
     assign_from_struct(lhs, full_lhs, to_struct_expr(rhs), guard);
   else
     assign_non_struct_symbol(lhs, full_lhs, rhs, guard);

The first three hunks are hacks, but it might make sense to come up with a proper patch that follows a similar approach to disable field sensitivity via the command line. The last hunk really is a bugfix as code shouldn't unconditionally assume field sensitivity is enabled.

[sepideha]

Thanks, will try! How about arrays? Could we disable field sensitivity in a similar way?

[tautschnig]

Thanks, will try! How about arrays? Could we disable field sensitivity in a similar way?

I believe the above patch disables field sensitivity entirely, i.e., both for structs and arrays. Let me know if you find an example that shows otherwise!

[tautschnig]

Is any further action required from the CBMC side?