added floating-point overflow checks

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3559 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

CHANGELOG

@@ -5,6 +5,8 @@ Added support for Solaris 11.
 
 Bugfixes in partial-order encoding.
 
+Added --float-overflow-check
+
 
 4.6
 ===

regression/cbmc/Float-overflow1/main.c

@@ -0,0 +1,7 @@
+int main()
+{
+  float f=1;
+
+  for(int i=0; i<127; i++)
+    f*=2; // should not overflow
+}

regression/cbmc/Float-overflow1/test.desc

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

regression/cbmc/Float-overflow2/main.c

@@ -0,0 +1,7 @@
+int main()
+{
+  float f=1;
+
+  for(int i=0; i<128; i++)
+    f*=2; // overflows in the last iteration
+}

regression/cbmc/Float-overflow2/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--floatbv --float-overflow-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--

src/analyses/goto_check.cpp

@@ -623,29 +623,117 @@ void goto_checkt::float_overflow_check(
 
   // First, check type.
   const typet &type=ns.follow(expr.type());
-  
-  if(type.id()==ID_floatbv)
+
+  if(type.id()!=ID_floatbv)
     return;
 
   // add overflow subgoal
 
   if(expr.id()==ID_typecast)
   {
+    // Can overflow if casting from larger
+    // to smaller type.
+    assert(expr.operands().size()==1);
+    
+    if(ns.follow(expr.op0().type()).id()==ID_floatbv)
+    {
+      // float-to-float
+      unary_exprt op0_inf(ID_isinf, expr.op0(), bool_typet());
+      unary_exprt new_inf(ID_isinf, expr, bool_typet());
+    
+      or_exprt overflow_check(op0_inf, not_exprt(new_inf));
+    
+      add_guarded_claim(
+        overflow_check,
+        "arithmetic overflow on floating-point typecast",
+        "overflow",
+        expr.find_location(),
+        expr,
+        guard);
+    }
+    else
+    {
+      // non-float-to-float
+      unary_exprt new_inf(ID_isinf, expr, bool_typet());
+    
+      add_guarded_claim(
+        not_exprt(new_inf),
+        "arithmetic overflow on floating-point typecast",
+        "overflow",
+        expr.find_location(),
+        expr,
+        guard);
+    }
+
     return;
   }
   else if(expr.id()==ID_div)
   {
     assert(expr.operands().size()==2);
+
+    // Can overflow if dividing by something small
+    unary_exprt new_inf(ID_isinf, expr, bool_typet());
+    unary_exprt op0_inf(ID_isinf, expr.op0(), bool_typet());
+    
+    or_exprt overflow_check(op0_inf, not_exprt(new_inf));
+
+    add_guarded_claim(
+      overflow_check,
+      "arithmetic overflow on floating-point division",
+      "overflow",
+      expr.find_location(),
+      expr,
+      guard);
+
     return;
   }
   else if(expr.id()==ID_mod)
   {
+    // Can't overflow
     return;
   }
   else if(expr.id()==ID_unary_minus)
   {
+    // Can't overflow
     return;
   }
+  else if(expr.id()==ID_plus || expr.id()==ID_mult ||
+          expr.id()==ID_minus)
+  {
+    if(expr.operands().size()==2)
+    {
+      // Can overflow
+      unary_exprt new_inf(ID_isinf, expr, bool_typet());      
+      unary_exprt op0_inf(ID_isinf, expr.op0(), bool_typet());
+      unary_exprt op1_inf(ID_isinf, expr.op1(), bool_typet());
+      
+      or_exprt overflow_check(op0_inf, op1_inf, not_exprt(new_inf));
+      
+      std::string kind=
+        expr.id()==ID_plus?"addition":
+        expr.id()==ID_minus?"subtraction":
+        expr.id()==ID_mult?"multiplication":"";
+      
+      add_guarded_claim(
+        overflow_check,
+        "arithmetic overflow on floating-point "+kind,
+        "overflow",
+        expr.find_location(),
+        expr,
+        guard);
+
+      return;
+    }
+    else if(expr.operands().size()>=3)
+    {
+      assert(expr.id()!=ID_minus);
+      
+      // break up
+      exprt tmp=make_binary(expr);
+      float_overflow_check(tmp, guard);
+      return;
+    }
+  }
 }
 
 /*******************************************************************\
@@ -1295,7 +1383,9 @@ void goto_checkt::check_rec(
   {
     if(expr.type().id()==ID_signedbv ||
        expr.type().id()==ID_unsignedbv)
+    {
       integer_overflow_check(expr, guard);
+    }
     else if(expr.type().id()==ID_floatbv)
     {
       nan_check(expr, guard);

src/cbmc/cbmc_parseoptions.cpp

@@ -198,6 +198,12 @@ void cbmc_parseoptionst::get_command_line_options(optionst &options)
   else
     options.set_option("unsigned-overflow-check", false);
 
+  // check overflow/underflow
+  if(cmdline.isset("float-overflow-check"))
+    options.set_option("float-overflow-check", true);
+  else
+    options.set_option("float-overflow-check", false);
+
   // check for NaN (not a number)
   if(cmdline.isset("nan-check"))
     options.set_option("nan-check", true);
@@ -850,6 +856,7 @@ void cbmc_parseoptionst::help()
     " --memory-leak-check          enable memory leak checks\n"
     " --signed-overflow-check      enable arithmetic over- and underflow checks\n"
     " --unsigned-overflow-check    enable arithmetic over- and underflow checks\n"
+    " --float-overflow-check       check floating-point for NaN\n"
     " --nan-check                  check floating-point for NaN\n"
     " --all-properties             report status of all properties\n"
     " --show-properties            show the properties\n"

src/cbmc/cbmc_parseoptions.h

@@ -28,7 +28,7 @@ class optionst;
   "D:I:" \
   "(depth):(partial-loops)(no-unwinding-assertions)(unwinding-assertions)" \
   "(bounds-check)(pointer-check)(div-by-zero-check)(memory-leak-check)" \
-  "(signed-overflow-check)(unsigned-overflow-check)(nan-check)" \
+  "(signed-overflow-check)(unsigned-overflow-check)(float-overflow-check)(nan-check)" \
   "(no-assertions)(no-assumptions)" \
   "(xml-ui)(xml-interface)(vcd):" \
   "(cvc)(smt1)(smt2)(boolector)(yices)(z3)(opensmt)(mathsat)(fpa)" \

src/goto-instrument/goto_instrument_parseoptions.cpp

@@ -570,6 +570,12 @@ void goto_instrument_parseoptionst::instrument_goto_program(
   else
     options.set_option("unsigned-overflow-check", false);
 
+  // check overflow/underflow
+  if(cmdline.isset("float-overflow-check"))
+    options.set_option("float-overflow-check", true);
+  else
+    options.set_option("float-overflow-check", false);
+
   // check for NaN (not a number)
   if(cmdline.isset("nan-check"))
     options.set_option("nan-check", true);

src/goto-instrument/goto_instrument_parseoptions.h

@@ -39,7 +39,7 @@ Author: Daniel Kroening, kroening@kroening.com
   "(nondet-volatile)(isr):" \
   "(stack-depth):(nondet-static)" \
   "(function-enter):(function-exit):(branch):" \
-  "(signed-overflow-check)(unsigned-overflow-check)" \
+  "(signed-overflow-check)(unsigned-overflow-check)(float-overflow-check)" \
   "(show-goto-functions)(show-value-sets)(show-local-may-alias)" \
   "(show-local-bitvector-analysis)" \
   "(show-struct-alignment)(interval-analysis)(show-intervals)" \