Symex: Simplify left-hand side

regression/cbmc/simplify-array-size/main.c

@@ -0,0 +1,36 @@
+#include <stdlib.h>
+#include <string.h>
+
+struct state
+{
+  size_t size;
+  int slots[];
+};
+
+struct hash_table
+{
+  struct state *p_impl;
+};
+
+void main(void)
+{
+  struct hash_table map;
+  size_t num_entries;
+  __CPROVER_assume(num_entries <= 8ul);
+  size_t required_bytes = num_entries * sizeof(int) + sizeof(struct state);
+  struct state *impl = malloc(required_bytes);
+  if(impl != NULL)
+  {
+    impl->size = num_entries;
+    map.p_impl = impl;
+  }
+  else
+    map.p_impl = NULL;
+
+  if(impl != NULL)
+  {
+    // keep this line even though it is never read
+    struct state *state = impl;
+    memset(impl->slots, 0, sizeof(int) * map.p_impl->size);
+  }
+}

regression/cbmc/simplify-array-size/test.desc

@@ -0,0 +1,12 @@
+CORE broken-smt-backend
+main.c
+--malloc-may-fail --malloc-fail-null
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^Invariant check failed
+^warning: ignoring
+--
+Simplification of array sizes must be applied consistently and must not result
+in value-set assignment invariant failures.

src/goto-symex/goto_symex_state.cpp

@@ -84,6 +84,8 @@ renamedt<ssa_exprt, L2> goto_symex_statet::assignment(
 
   // the type might need renaming
   rename<L2>(lhs.type(), l1_identifier, ns);
+  if(rhs_is_simplified)
+    simplify(lhs, ns);
   lhs.update_type();
   if(run_validation_checks)
   {