Define and use an expr_skeletont class

This clarifies the meaning of skeletons, which we use in assignmentt.
This makes sure the skeleton field is always of the correct form for a
skeleton.

Author: romainbrenguier

src/goto-symex/goto_symex.cpp

@@ -80,6 +80,6 @@ void goto_symext::symex_assign(statet &state, const code_assignt &code)
 
     exprt::operandst lhs_if_then_else_conditions;
     symex_assignt{state, assignment_type, ns, symex_config, target}.assign_rec(
-      lhs, nil_exprt(), rhs, lhs_if_then_else_conditions);
+      lhs, expr_skeletont{}, rhs, lhs_if_then_else_conditions);
   }
 }

src/goto-symex/symex_assign.cpp

@@ -31,26 +31,19 @@ constexpr bool use_update()
 #endif
 }
 
-/// Store the \p what expression by recursively descending into the operands
-/// of \p lhs until the first operand \c op0 is _nil_: this _nil_ operand
-/// is then replaced with \p what.
-/// \param lhs: Non-symbol pointed-to expression
-/// \param what: The expression to be added to the \p lhs
-/// \return The resulting expression
-static exprt add_to_lhs(const exprt &lhs, const exprt &what)
+expr_skeletont expr_skeletont::remove_op0(exprt e)
 {
-  PRECONDITION(lhs.id() != ID_symbol);
-  exprt tmp_what=what;
-
-  if(tmp_what.id()!=ID_symbol)
-  {
-    PRECONDITION(tmp_what.operands().size() >= 1);
-    tmp_what.op0().make_nil();
-  }
-
-  exprt new_lhs=lhs;
+  PRECONDITION(e.id() != ID_symbol);
+  PRECONDITION(e.operands().size() >= 1);
+  e.op0().make_nil();
+  return expr_skeletont{std::move(e)};
+}
 
-  exprt *p=&new_lhs;
+exprt expr_skeletont::apply(exprt expr) const
+{
+  PRECONDITION(skeleton.id() != ID_symbol);
+  exprt result = skeleton;
+  exprt *p = &result;
 
   while(p->is_not_nil())
   {
@@ -60,18 +53,23 @@ static exprt add_to_lhs(const exprt &lhs, const exprt &what)
     INVARIANT(
       p->operands().size() >= 1,
       "expected pointed-to expression to have at least one operand");
-    p=&p->op0();
+    p = &p->op0();
   }
 
   INVARIANT(p->is_nil(), "expected pointed-to expression to be nil");
 
-  *p=tmp_what;
-  return new_lhs;
+  *p = std::move(expr);
+  return result;
+}
+
+expr_skeletont expr_skeletont::compose(expr_skeletont other) const
+{
+  return expr_skeletont(apply(other.skeleton));
 }
 
 void symex_assignt::assign_rec(
   const exprt &lhs,
-  const exprt &full_lhs,
+  const expr_skeletont &full_lhs,
   const exprt &rhs,
   exprt::operandst &guard)
 {
@@ -349,7 +347,7 @@ static assignmentt shift_indexed_access_to_lhs(
 /// \param guard: guard conjuncts that must hold for this assignment to be made
 void symex_assignt::assign_from_struct(
   const ssa_exprt &lhs, // L1
-  const exprt &full_lhs,
+  const expr_skeletont &full_lhs,
   const struct_exprt &rhs,
   const exprt::operandst &guard)
 {
@@ -371,7 +369,7 @@ void symex_assignt::assign_from_struct(
 
 void symex_assignt::assign_non_struct_symbol(
   const ssa_exprt &lhs, // L1
-  const exprt &full_lhs,
+  const expr_skeletont &full_lhs,
   const exprt &rhs,
   const exprt::operandst &guard)
 {
@@ -409,8 +407,7 @@ void symex_assignt::assign_non_struct_symbol(
                              .get();
 
   state.record_events.push(false);
-  const exprt l2_full_lhs =
-    state.rename(add_to_lhs(full_lhs, l2_lhs), ns).get();
+  const exprt l2_full_lhs = state.rename(full_lhs.apply(l2_lhs), ns).get();
   state.record_events.pop();
 
   auto current_assignment_type =
@@ -443,7 +440,7 @@ void symex_assignt::assign_non_struct_symbol(
 
 void symex_assignt::assign_symbol(
   const ssa_exprt &lhs, // L1
-  const exprt &full_lhs,
+  const expr_skeletont &full_lhs,
   const exprt &rhs,
   const exprt::operandst &guard)
 {
@@ -456,21 +453,21 @@ void symex_assignt::assign_symbol(
 
 void symex_assignt::assign_typecast(
   const typecast_exprt &lhs,
-  const exprt &full_lhs,
+  const expr_skeletont &full_lhs,
   const exprt &rhs,
   exprt::operandst &guard)
 {
   // these may come from dereferencing on the lhs
   exprt rhs_typecasted = typecast_exprt::conditional_cast(rhs, lhs.op().type());
-
-  exprt new_full_lhs=add_to_lhs(full_lhs, lhs);
-  assign_rec(lhs.op(), new_full_lhs, rhs_typecasted, guard);
+  expr_skeletont new_skeleton =
+    full_lhs.compose(expr_skeletont::remove_op0(lhs));
+  assign_rec(lhs.op(), new_skeleton, rhs_typecasted, guard);
 }
 
 template <bool use_update>
 void symex_assignt::assign_array(
   const index_exprt &lhs,
-  const exprt &full_lhs,
+  const expr_skeletont &full_lhs,
   const exprt &rhs,
   exprt::operandst &guard)
 {
@@ -487,8 +484,9 @@ void symex_assignt::assign_array(
     // into
     //   a'==UPDATE(a, [i], e)
     const update_exprt new_rhs{lhs_array, index_designatort(lhs_index), rhs};
-    const exprt new_full_lhs = add_to_lhs(full_lhs, lhs);
-    assign_rec(lhs_array, new_full_lhs, new_rhs, guard);
+    const expr_skeletont new_skeleton =
+      full_lhs.compose(expr_skeletont::remove_op0(lhs));
+    assign_rec(lhs, new_skeleton, new_rhs, guard);
   }
   else
   {
@@ -497,15 +495,16 @@ void symex_assignt::assign_array(
     // into
     //   a'==a WITH [i:=e]
     const with_exprt new_rhs{lhs_array, lhs_index, rhs};
-    const exprt new_full_lhs = add_to_lhs(full_lhs, lhs);
-    assign_rec(lhs_array, new_full_lhs, new_rhs, guard);
+    const expr_skeletont new_skeleton =
+      full_lhs.compose(expr_skeletont::remove_op0(lhs));
+    assign_rec(lhs_array, new_skeleton, new_rhs, guard);
   }
 }
 
 template <bool use_update>
 void symex_assignt::assign_struct_member(
   const member_exprt &lhs,
-  const exprt &full_lhs,
+  const expr_skeletont &full_lhs,
   const exprt &rhs,
   exprt::operandst &guard)
 {
@@ -546,8 +545,9 @@ void symex_assignt::assign_struct_member(
     //   a'==UPDATE(a, .c, e)
     const update_exprt new_rhs{
       lhs_struct, member_designatort(component_name), rhs};
-    const exprt new_full_lhs = add_to_lhs(full_lhs, lhs);
-    assign_rec(lhs_struct, new_full_lhs, new_rhs, guard);
+    const expr_skeletont new_skeleton =
+      full_lhs.compose(expr_skeletont::remove_op0(lhs));
+    assign_rec(lhs_struct, new_skeleton, new_rhs, guard);
   }
   else
   {
@@ -558,15 +558,15 @@ void symex_assignt::assign_struct_member(
 
     with_exprt new_rhs(lhs_struct, exprt(ID_member_name), rhs);
     new_rhs.where().set(ID_component_name, component_name);
-
-    exprt new_full_lhs = add_to_lhs(full_lhs, lhs);
-    assign_rec(lhs_struct, new_full_lhs, new_rhs, guard);
+    const expr_skeletont new_skeleton =
+      full_lhs.compose(expr_skeletont::remove_op0(lhs));
+    assign_rec(lhs_struct, new_skeleton, new_rhs, guard);
   }
 }
 
 void symex_assignt::assign_if(
   const if_exprt &lhs,
-  const exprt &full_lhs,
+  const expr_skeletont &full_lhs,
   const exprt &rhs,
   exprt::operandst &guard)
 {
@@ -592,7 +592,7 @@ void symex_assignt::assign_if(
 
 void symex_assignt::assign_byte_extract(
   const byte_extract_exprt &lhs,
-  const exprt &full_lhs,
+  const expr_skeletont &full_lhs,
   const exprt &rhs,
   exprt::operandst &guard)
 {
@@ -608,6 +608,7 @@ void symex_assignt::assign_byte_extract(
     UNREACHABLE;
 
   const byte_update_exprt new_rhs{byte_update_id, lhs.op(), lhs.offset(), rhs};
-  exprt new_full_lhs=add_to_lhs(full_lhs, lhs);
-  assign_rec(lhs.op(), new_full_lhs, new_rhs, guard);
+  const expr_skeletont new_skeleton =
+    full_lhs.compose(expr_skeletont::remove_op0(lhs));
+  assign_rec(lhs.op(), new_skeleton, new_rhs, guard);
 }

src/goto-symex/symex_assign.h

@@ -20,6 +20,49 @@ class byte_extract_exprt;
 class ssa_exprt;
 struct symex_configt;
 
+/// Expression in which some part is missing and can be substituted for another
+/// expression.
+///
+/// For instance, a skeleton `☐[index]` where `☐` is the missing part, can be
+/// applied to an expression `x` to get `x[index]` (see
+/// \ref expr_skeletont::apply). It can also be composed with another skeleton,
+/// let say `☐.some_field` which would give the skeleton `☐.some_field[index]`
+/// (see \ref expr_skeletont::compose).
+class expr_skeletont final
+{
+public:
+  /// Empty skeleton. Applying it to an expression would give the same
+  /// expression unchanged
+  expr_skeletont() : skeleton(nil_exprt{})
+  {
+  }
+
+  /// Replace the missing part of the current skeleton by another skeleton,
+  /// ending in a bigger skeleton corresponding to the two combined.
+  expr_skeletont compose(expr_skeletont other) const;
+
+  /// Replace the missing part by the given expression, to end-up with a
+  /// complete expression
+  exprt apply(exprt expr) const;
+
+  /// Create a skeleton by removing the first operand of \p e. For instance,
+  /// remove_op0 on `array[index]` would give a skeleton in which `array` is
+  /// missing, and applying that skeleton to `array2` would give
+  /// `array2[index]`.
+  static expr_skeletont remove_op0(exprt e);
+
+private:
+  /// In \c skeleton, nil_exprt is used to mark the sub expression to be
+  /// substituted. The nil_exprt always appears recursively following the first
+  /// operands because the only way to get a skeleton is by removing the first
+  /// operand.
+  exprt skeleton;
+
+  explicit expr_skeletont(exprt e) : skeleton(std::move(e))
+  {
+  }
+};
+
 /// Functor for symex assignment
 class symex_assignt
 {
@@ -44,13 +87,13 @@ class symex_assignt
   /// respectively.
   void assign_symbol(
     const ssa_exprt &lhs, // L1
-    const exprt &full_lhs,
+    const expr_skeletont &full_lhs,
     const exprt &rhs,
     const exprt::operandst &guard);
 
   void assign_rec(
     const exprt &lhs,
-    const exprt &full_lhs,
+    const expr_skeletont &full_lhs,
     const exprt &rhs,
     exprt::operandst &guard);
 
@@ -63,13 +106,13 @@ class symex_assignt
 
   void assign_from_struct(
     const ssa_exprt &lhs, // L1
-    const exprt &full_lhs,
+    const expr_skeletont &full_lhs,
     const struct_exprt &rhs,
     const exprt::operandst &guard);
 
   void assign_non_struct_symbol(
     const ssa_exprt &lhs, // L1
-    const exprt &full_lhs,
+    const expr_skeletont &full_lhs,
     const exprt &rhs,
     const exprt::operandst &guard);
 
@@ -78,7 +121,7 @@ class symex_assignt
   template <bool use_update>
   void assign_array(
     const index_exprt &lhs,
-    const exprt &full_lhs,
+    const expr_skeletont &full_lhs,
     const exprt &rhs,
     exprt::operandst &guard);
 
@@ -87,25 +130,25 @@ class symex_assignt
   template <bool use_update>
   void assign_struct_member(
     const member_exprt &lhs,
-    const exprt &full_lhs,
+    const expr_skeletont &full_lhs,
     const exprt &rhs,
     exprt::operandst &guard);
 
   void assign_if(
     const if_exprt &lhs,
-    const exprt &full_lhs,
+    const expr_skeletont &full_lhs,
     const exprt &rhs,
     exprt::operandst &guard);
 
   void assign_typecast(
     const typecast_exprt &lhs,
-    const exprt &full_lhs,
+    const expr_skeletont &full_lhs,
     const exprt &rhs,
     exprt::operandst &guard);
 
   void assign_byte_extract(
     const byte_extract_exprt &lhs,
-    const exprt &full_lhs,
+    const expr_skeletont &full_lhs,
     const exprt &rhs,
     exprt::operandst &guard);
 };

src/goto-symex/symex_clean_expr.cpp

@@ -188,7 +188,7 @@ void goto_symext::lift_let(statet &state, const let_exprt &let_expr)
     state, symex_targett::assignment_typet::HIDDEN, ns, symex_config, target}
     .assign_symbol(
       to_ssa_expr(state.rename<L1>(let_expr.symbol(), ns).get()),
-      nil_exprt(),
+      expr_skeletont{},
       let_value,
       value_assignment_guard);
 

src/goto-symex/symex_function_call.cpp

@@ -141,7 +141,7 @@ void goto_symext::parameter_assignments(
 
       exprt::operandst lhs_conditions;
       symex_assignt{state, assignment_type, ns, symex_config, target}
-        .assign_rec(lhs, nil_exprt(), rhs, lhs_conditions);
+        .assign_rec(lhs, expr_skeletont{}, rhs, lhs_conditions);
     }
 
     if(it1!=arguments.end())

src/goto-symex/symex_start_thread.cpp

@@ -89,7 +89,7 @@ void goto_symext::symex_start_thread(statet &state)
     state.record_events.push(false);
     symex_assignt{
       state, symex_targett::assignment_typet::HIDDEN, ns, symex_config, target}
-      .assign_symbol(lhs_l1, nil_exprt(), rhs, lhs_conditions);
+      .assign_symbol(lhs_l1, expr_skeletont{}, rhs, lhs_conditions);
     state.record_events.pop();
   }
 
@@ -122,6 +122,6 @@ void goto_symext::symex_start_thread(statet &state)
     exprt::operandst lhs_conditions;
     symex_assignt{
       state, symex_targett::assignment_typet::HIDDEN, ns, symex_config, target}
-      .assign_symbol(lhs, nil_exprt(), rhs, lhs_conditions);
+      .assign_symbol(lhs, expr_skeletont{}, rhs, lhs_conditions);
   }
 }