Fixing simplification of LHS

src/analyses/ai.cpp

@@ -57,29 +57,33 @@ bool ai_domain_baset::ai_simplify_lhs(
   if(condition.id()==ID_index)
   {
     index_exprt ie=to_index_expr(condition);
-    bool changed=ai_simplify(ie.index(), ns);
-    if(changed)
+    bool no_simplification=ai_simplify(ie.index(), ns);
+    if(!no_simplification)
       condition=simplify_expr(ie, ns);
 
-    return !changed;
+    return no_simplification;
   }
   else if(condition.id()==ID_dereference)
   {
     dereference_exprt de=to_dereference_expr(condition);
-    bool changed=ai_simplify(de.pointer(), ns);
-    if(changed)
+    bool no_simplification=ai_simplify(de.pointer(), ns);
+    if(!no_simplification)
       condition=simplify_expr(de, ns);  // So *(&x) -> x
 
-    return !changed;
+    return no_simplification;
   }
   else if(condition.id()==ID_member)
   {
     member_exprt me=to_member_expr(condition);
-    bool changed=ai_simplify_lhs(me.compound(), ns); // <-- lhs!
-    if(changed)
+    // Since simplify_ai_lhs is required to return an addressable object
+    // (so remains a valid left hand side), to simplify
+    // `(something_simplifiable).b` we require that `something_simplifiable`
+    // must also be addressable
+    bool no_simplification=ai_simplify_lhs(me.compound(), ns);
+    if(!no_simplification)
       condition=simplify_expr(me, ns);
 
-    return !changed;
+    return no_simplification;
   }
   else
     return true;

unit/Makefile

@@ -7,6 +7,7 @@ SRC = src/expr/require_expr.cpp \
 
 # Test source files
 SRC += unit_tests.cpp \
+       analyses/ai/ai_simplify_lhs.cpp \
        analyses/does_remove_const/does_expr_lose_const.cpp \
        analyses/does_remove_const/does_type_preserve_const_correctness.cpp \
        analyses/does_remove_const/is_type_at_least_as_const_as.cpp \

unit/analyses/ai/ai_simplify_lhs.cpp

@@ -0,0 +1,168 @@
+/*******************************************************************\
+
+ Module: Unit tests for ai_domain_baset::ai_simplify_lhs
+
+ Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+/// \file
+/// Unit tests for ai_domain_baset::ai_simplify_lhs
+
+#include <catch.hpp>
+
+#include <analyses/ai.h>
+
+#include <ansi-c/ansi_c_language.h>
+
+#include <util/arith_tools.h>
+#include <util/config.h>
+#include <util/namespace.h>
+#include <util/ui_message.h>
+#include <util/simplify_expr.h>
+
+class constant_simplification_mockt:public ai_domain_baset
+{
+public:
+  void transform(locationt, locationt, ai_baset &, const namespacet &) override
+  {}
+  void make_bottom() override
+  {}
+  void make_top() override
+  {}
+  void make_entry() override
+  {}
+
+  bool ai_simplify(exprt &condition, const namespacet &ns) const override;
+};
+
+bool constant_simplification_mockt::ai_simplify(
+  exprt &condition, const namespacet &ns) const
+{
+  exprt simplified_expr=simplify_expr(condition, ns);
+  // no simplification
+  if(simplified_expr==condition)
+  {
+    return true;
+  }
+  // a simplification has occurred
+  condition=simplified_expr;
+  return false;
+}
+
+SCENARIO("ai_domain_baset::ai_simplify_lhs",
+  "[core][analyses][ai][ai_simplify_lhs]")
+{
+  ui_message_handlert message_handler;
+  ansi_c_languaget language;
+  language.set_message_handler(message_handler);
+
+  symbol_tablet symbol_table;
+  namespacet ns(symbol_table);
+
+  constant_simplification_mockt mock_ai_domain;
+
+  config.set_arch("none");
+
+  GIVEN("A index_exprt")
+  {
+    // Construct an expression that the simplify_expr can simplify
+    exprt simplifiable_expression;
+    bool compile_failed=
+      language.to_expr("1 + 1", "", simplifiable_expression, ns);
+
+    const unsigned int array_size=5;
+    array_typet array_type(
+      signedbv_typet(32), constant_exprt::integer_constant(array_size));
+
+    // Verify the results of the setup
+    REQUIRE_FALSE(compile_failed);\
+    REQUIRE(simplifiable_expression.id()==ID_plus);
+    exprt simplified_version=simplify_expr(simplifiable_expression, ns);
+    REQUIRE(simplified_version.id()==ID_constant);
+
+    WHEN(
+      "Simplifying an index expression with constant index but variable array")
+    {
+      const index_exprt &index_expr=
+        index_exprt(symbol_exprt("a", array_type), simplifiable_expression);
+
+      THEN("Then only the index of the part of the expression should be "
+        "simplified")
+      {
+        exprt out_expr=index_expr;
+        bool no_simplification=mock_ai_domain.ai_simplify_lhs(out_expr, ns);
+        REQUIRE_FALSE(no_simplification);
+        REQUIRE(index_expr.id()==ID_index);
+
+        index_exprt simplified_index_expr=to_index_expr(out_expr);
+        REQUIRE(simplified_index_expr.index().id()==ID_constant);
+
+        constant_exprt constant_index=
+          to_constant_expr(simplified_index_expr.index());
+
+        mp_integer out_index;
+        bool failed_to_integer=to_integer(constant_index, out_index);
+        REQUIRE_FALSE(failed_to_integer);
+        REQUIRE(out_index==2);
+      }
+    }
+    WHEN("Simplifying an index expression with variable index and array")
+    {
+      // a[i]
+      const index_exprt &index_expr=
+        index_exprt(
+          symbol_exprt("a", array_type), symbol_exprt("i", signedbv_typet(32)));
+
+      THEN("Then no simplification should occur")
+      {
+        exprt out_expr=index_expr;
+        bool no_simplification=mock_ai_domain.ai_simplify_lhs(out_expr, ns);
+        REQUIRE(no_simplification);
+        REQUIRE(index_expr.id()==ID_index);
+
+        index_exprt simplified_index_expr=to_index_expr(out_expr);
+        REQUIRE(simplified_index_expr.index().id()==ID_symbol);
+      }
+    }
+
+    // This fails since the implementation does do a constant simplification
+    // on the array part. It isn't clear to me if this is correct
+#if 0
+    WHEN(
+      "Simplifying an index expression with constant index in a constant array")
+    {
+      array_exprt constant_array=array_exprt(array_type);
+      for(unsigned int i=0; i<array_size; ++i)
+      {
+        REQUIRE(constant_array.operands().size()==i);
+        constant_array.operands().push_back(
+          constant_exprt::integer_constant(i));
+      }
+
+      const index_exprt &index_expr=
+        index_exprt(constant_array, simplifiable_expression);
+
+      THEN("Then only the index of the part of the expression should be "
+        "simplified")
+      {
+        exprt out_expr=index_expr;
+        bool no_simplification=mock_ai_domain.ai_simplify_lhs(out_expr, ns);
+        REQUIRE_FALSE(no_simplification);
+        REQUIRE(out_expr.id()==ID_index);
+
+        index_exprt simplified_index_expr=to_index_expr(out_expr);
+        REQUIRE(simplified_index_expr.index().id()==ID_constant);
+
+        constant_exprt constant_index=
+          to_constant_expr(simplified_index_expr.index());
+
+        mp_integer out_index;
+        bool failed_to_integer=to_integer(constant_index, out_index);
+        REQUIRE_FALSE(failed_to_integer);
+        REQUIRE(out_index==2);
+      }
+    }
+#endif
+  }
+}