Merge pull request #1621 from tautschnig/fix-1620

Use stable data structure for BV refinement approximations

Author: kroening

regression/cbmc/Float-div1-refine/main.c

@@ -0,0 +1,50 @@
+#include <assert.h>
+#include <math.h>
+
+#ifdef __GNUC__
+void inductiveStepHunt (float startState)
+{
+  float target = 0x1.fffffep-3f;
+
+  __CPROVER_assume((0 < startState) && (fpclassify(startState) == FP_NORMAL) && (0x1p-126f <= startState));
+
+  float secondPoint = (target / startState);
+
+  float nextState = (startState + secondPoint) / 2;
+
+  float oneAfter = (target / nextState);
+
+  assert(oneAfter > 0);
+}
+
+void simplifiedInductiveStepHunt (float nextState)
+{
+  float target = 0x1.fffffep-3f;
+
+  // Implies nextState == 0x1p+124f;
+  __CPROVER_assume((0x1.fffffep+123f < nextState) && (nextState < 0x1.000002p+124f));
+
+  float oneAfter = (target / nextState);
+
+  // Is true and correctly proven by constant evaluation
+  // Note that this is the smallest normal number
+  assert(0x1.fffffep-3f / 0x1p+124f == 0x1p-126f);
+
+  assert(oneAfter > 0);
+}
+#endif
+
+int main (void)
+{
+  #ifdef __GNUC__
+  //  inductiveStepHunt(0x1p+125f);
+  //  simplifiedInductiveStepHunt(0x1p+124f);
+
+  float f, g;
+
+  inductiveStepHunt(f);
+  simplifiedInductiveStepHunt(g);
+  #endif
+
+  return 0;
+}

regression/cbmc/Float-div1-refine/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--floatbv --refine
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/solvers/refinement/bv_refinement.h

@@ -108,7 +108,7 @@ class bv_refinementt:public bv_pointerst
   // MEMBERS
 
   bool progress;
-  std::vector<approximationt> approximations;
+  std::list<approximationt> approximations;
   bvt parent_assumptions;
 protected:
   // use gui format

src/solvers/refinement/refine_arithmetic.cpp

@@ -487,7 +487,7 @@ bv_refinementt::add_approximation(
   const exprt &expr, bvt &bv)
 {
   approximations.push_back(approximationt(approximations.size()));
-  approximationt &a=approximations.back(); // stable!
+  approximationt &a=approximations.back();
 
   std::size_t width=boolbv_width(expr.type());
   PRECONDITION(width!=0);