Domain pruning for < and <= assumptions.

Implemented for intervals and value-sets which are not top.

Author: jezhiggins

regression/goto-analyzer/pruning-le/main.c

@@ -0,0 +1,13 @@
+int main()
+{
+  int x = 0;
+  if(nondet())
+  {
+    x = 30;
+  }
+
+  if(x < 10)
+  {
+    assert(x < 20);
+  }
+}

regression/goto-analyzer/pruning-le/test-constants.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values constants --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line .* assertion x < 20: UNKNOWN
+
+--

regression/goto-analyzer/pruning-le/test-intervals.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values intervals --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line .* assertion x < 20: SUCCESS
+--

regression/goto-analyzer/pruning-le/test-value-sets.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values set-of-constants --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line .* assertion x < 20: SUCCESS
+--

src/analyses/variable-sensitivity/abstract_environment.cpp

@@ -553,6 +553,19 @@ exprt invert_expr(const exprt &expr)
     relation_expr.lhs(), inverse_op, relation_expr.rhs());
 }
 
+void prune_assign(
+  abstract_environmentt &env,
+  const exprt &destination,
+  abstract_object_pointert obj,
+  const namespacet &ns)
+{
+  auto context_value =
+    std::dynamic_pointer_cast<const context_abstract_objectt>(obj);
+  if(context_value == nullptr)
+    obj = env.add_object_context(obj);
+  env.assign(destination, obj, ns);
+}
+
 exprt assume_not(
   abstract_environmentt &env,
   const exprt &expr,
@@ -623,9 +636,9 @@ exprt assume_eq(
     return false_exprt();
 
   if(is_lvalue(equal_expr.lhs()))
-    env.assign(equal_expr.lhs(), meet, ns);
+    prune_assign(env, equal_expr.lhs(), meet, ns);
   if(is_lvalue(equal_expr.rhs()))
-    env.assign(equal_expr.rhs(), meet, ns);
+    prune_assign(env, equal_expr.rhs(), meet, ns);
   return true_exprt();
 }
 
@@ -654,6 +667,8 @@ exprt assume_noteq(
 
 struct left_and_right_valuest
 {
+  exprt lhs;
+  exprt rhs;
   abstract_value_pointert left;
   abstract_value_pointert right;
 
@@ -679,13 +694,15 @@ left_and_right_valuest eval_operands_as_values(
 {
   auto const &relationship_expr = to_binary_expr(expr);
 
-  auto left = env.eval(relationship_expr.lhs(), ns);
-  auto right = env.eval(relationship_expr.rhs(), ns);
+  auto lhs = relationship_expr.lhs();
+  auto rhs = relationship_expr.rhs();
+  auto left = env.eval(lhs, ns);
+  auto right = env.eval(rhs, ns);
 
   if(left->is_top() || right->is_top())
     return {};
 
-  return {as_value(left), as_value(right)};
+  return {lhs, rhs, as_value(left), as_value(right)};
 }
 
 exprt assume_less_than(
@@ -697,12 +714,33 @@ exprt assume_less_than(
   if(!operands.are_good())
     return nil_exprt();
 
-  auto left_lower = operands.left_interval().get_lower();
-  auto right_upper = operands.right_interval().get_upper();
+  auto left_interval = operands.left_interval();
+  auto right_interval = operands.right_interval();
+
+  const auto &left_lower = left_interval.get_lower();
+  const auto &right_upper = right_interval.get_upper();
 
   auto reduced_le_expr =
     binary_relation_exprt(left_lower, expr.id(), right_upper);
-  return env.eval(reduced_le_expr, ns)->to_constant();
+  auto result = env.eval(reduced_le_expr, ns)->to_constant();
+  if(result.is_true())
+  {
+    if(is_lvalue(operands.lhs))
+    {
+      auto pruned_upper = constant_interval_exprt::get_min(
+        left_interval.get_upper(), right_upper);
+      auto constrained = operands.left->constrain(left_lower, pruned_upper);
+      prune_assign(env, operands.lhs, constrained, ns);
+    }
+    if(is_lvalue(operands.rhs))
+    {
+      auto pruned_lower = constant_interval_exprt::get_max(
+        left_lower, right_interval.get_lower());
+      auto constrained = operands.right->constrain(pruned_lower, right_upper);
+      prune_assign(env, operands.rhs, constrained, ns);
+    }
+  }
+  return result;
 }
 
 exprt assume_greater_than(

src/analyses/variable-sensitivity/abstract_value_object.cpp

@@ -694,3 +694,9 @@ static abstract_object_pointert value_set_expression_transform(
   auto evaluator = value_set_evaluator(expr, operands, environment, ns);
   return evaluator();
 }
+
+abstract_value_pointert
+abstract_value_objectt::as_value(const abstract_object_pointert &obj) const
+{
+  return std::dynamic_pointer_cast<const abstract_value_objectt>(obj);
+}

src/analyses/variable-sensitivity/abstract_value_object.h

@@ -287,12 +287,18 @@ class abstract_value_objectt : public abstract_objectt,
     const abstract_environmentt &environment,
     const namespacet &ns) const final;
 
+  virtual sharing_ptrt<const abstract_value_objectt>
+  constrain(const exprt &lower, const exprt &upper) const = 0;
+
 protected:
   virtual index_range_implementation_ptrt
   index_range_implementation(const namespacet &ns) const = 0;
 
   virtual value_range_implementation_ptrt
   value_range_implementation() const = 0;
+
+  sharing_ptrt<const abstract_value_objectt>
+  as_value(const abstract_object_pointert &obj) const;
 };
 
 using abstract_value_pointert = sharing_ptrt<const abstract_value_objectt>;

src/analyses/variable-sensitivity/constant_abstract_value.cpp

@@ -158,6 +158,13 @@ abstract_object_pointert constant_abstract_valuet::meet_with_value(
   return abstract_objectt::meet(other);
 }
 
+abstract_value_pointert constant_abstract_valuet::constrain(
+  const exprt &lower,
+  const exprt &upper) const
+{
+  return as_value(mutable_clone());
+}
+
 void constant_abstract_valuet::get_statistics(
   abstract_object_statisticst &statistics,
   abstract_object_visitedt &visited,

src/analyses/variable-sensitivity/constant_abstract_value.h

@@ -37,6 +37,9 @@ class constant_abstract_valuet : public abstract_value_objectt
   exprt to_constant() const override;
   constant_interval_exprt to_interval() const override;
 
+  abstract_value_pointert
+  constrain(const exprt &lower, const exprt &upper) const override;
+
   void output(
     std::ostream &out,
     const class ai_baset &ai,

src/analyses/variable-sensitivity/interval_abstract_value.cpp

@@ -446,6 +446,19 @@ interval_abstract_valuet::value_range_implementation() const
   return make_single_value_range(shared_from_this());
 }
 
+abstract_value_pointert interval_abstract_valuet::constrain(
+  const exprt &lower,
+  const exprt &upper) const
+{
+  auto lower_bound =
+    constant_interval_exprt::get_max(lower, interval.get_lower());
+  auto upper_bound =
+    constant_interval_exprt::get_min(upper, interval.get_upper());
+
+  return as_value(
+    make_interval(constant_interval_exprt(lower_bound, upper_bound)));
+}
+
 void interval_abstract_valuet::get_statistics(
   abstract_object_statisticst &statistics,
   abstract_object_visitedt &visited,