Range check via Cprover assert #91

xbauch · 2018-12-11T16:14:09Z

No description provided.

hannes-steffenhagen-diffblue

I think this is going in the right direction but needs some cleanup and some rethinking of how we pass around ranges before it can go in.

There is also no test attached to this.

hannes-steffenhagen-diffblue · 2018-12-11T16:38:59Z

gnat2goto/driver/tree_walk.adb

+   function Uint_To_Integer (Number : Uint) return Integer
+   is
+   begin
+      return Integer (UI_To_Int (Number));


This restricts us to 32 bit bounds (Int is basically a 32 bit signed integer). We need to find a better way around this

@hannes-steffenhagen-diffblue I've added one commit that addresses that.

@xbauch could you reference the commit please.

The commit is gone now, but basically we went from Int to Uint (which is of arbitrary size). It is now in separate package range_check.

hannes-steffenhagen-diffblue · 2018-12-11T16:39:55Z

gnat2goto/driver/tree_walk.adb

+   function Do_Assert (N : Node_Id; Assertion : Irep; Description : Irep)
+                       return Irep;
+
+   function Do_Range_Assert (N : Node_Id; Value : Irep; Value_Type : Irep)


These 3 functions actually generate code, but they're using the naming scheme of the functions that handle an AST node. I think we need to come up with less confusing names for these.

hannes-steffenhagen-diffblue · 2018-12-11T16:51:42Z

gnat2goto/driver/tree_walk.adb

@@ -928,8 +1029,10 @@ package body Tree_Walk is
      end if;
      return R : constant Irep := New_Irep (I_Bounded_Signedbv_Type) do
         Set_Width (R, Get_Width (Resolved_Underlying));
-         Set_Lower_Bound (R, Do_Constant (Low_Bound (Range_Expr)));
-         Set_Upper_Bound (R, Do_Constant (High_Bound (Range_Expr)));
+         Set_Lower_Bound (R, Uint_To_Integer (Intval (Low_Bound


I still don't think it makes much sense for these to be properties on the type; For dynamic bounds at least we'll need to carry around the bounds in variables/hidden parameters anyway

What is keeping us from using unbounded signedbv types for the bounds here by the way?

@hannes-steffenhagen-diffblue I'm not sure what is going to be the best approach for dynamic bounds. As of now, the bounds are Uints (as per the last commit) and the Irep properties are Integer. Having any other numeric type inside Ireps would require changing the schemes, and the generating Python script.

xbauch · 2018-12-14T12:34:47Z

@hannes-steffenhagen-diffblue I've renamed the 3 functions that create code (to Make_*_Expr/Call). Changed the expected output of ranges test (which is intended as a test for this feature). And generalised the bounds to Uints which are stored in a separate hash-table and only indexed from Ireps for bounded types. I squashed it to 1 commit, but can break it again.

hannes-steffenhagen-diffblue · 2018-12-18T15:58:11Z

gnat2goto/driver/tree_walk.adb

+     (Index_Type   => Natural,
+      Element_Type => Uint);
+
+   Integer_Bounds_Table : Integer_Bounds_Vector.Vector;


⛏️ I think I'd be more comfortable if the above were in a separate package, also if the key had its own type (so we'd cast on access, but for here could keep the key something that is distinct from an integer). The latter just to prevent accidental misuse, the former because this package is already very crowded as is.

Moved to a separate package and declared a new type Bound_Type.

hannes-steffenhagen-diffblue · 2018-12-18T16:23:47Z

gnat2goto/driver/tree_walk.adb

-   function Make_Sym_Range_Expression (I : Irep) return Irep
-   with Pre  => Kind (I) = I_Symbol_Expr,
-        Post => Kind (Make_Sym_Range_Expression'Result) in Class_Expr;
+   function Make_Sym_Range_Expression (I : Irep; Val_Type : Irep) return Irep


This is called Sym_Range_Expression but we no longer demand the parameter to be a symbol?

gnat2goto/driver/tree_walk.adb

hannes-steffenhagen-diffblue · 2019-01-08T11:54:35Z

gnat2goto/driver/tree_walk.adb

            declare
               Cast_RHS : constant Irep := New_Irep (I_Op_Typecast);
            begin
               Set_Op0 (Cast_RHS, RHS);
               Set_Type (Cast_RHS, Get_Type (LHS));
-               Set_Range_Check (Cast_RHS, True);
-               Set_Rhs (R, Cast_RHS);
+               Set_Rhs (R, Make_Range_Assert_Expr (N, Cast_RHS,


I think the range checks should happen before the typecast, in case of a cast into a smaller type? Then again, what happens when casting to a larger type?

Swapped. I guess casting to a larger type should simply pass the range check.

hannes-steffenhagen-diffblue · 2019-01-08T12:00:46Z

gnat2goto/driver/tree_walk.adb

+                      Value => Sym_Type);
+            Set_Value (I     => Lower_Bound,
+                       Value => Load_Bound_In_Hex (Get_Lower_Bound (Sym_Type),
+                        Pos (Get_Width (Sym_Type))));


What if the width of the type isn't large enough to hold the value?

Wouldn't that mean that the bound cannot be stored in a variable of that type?

hannes-steffenhagen-diffblue · 2019-01-08T12:02:52Z

testsuite/gnat2goto/tests/ranges/test.out

@@ -1 +1,3 @@
-VERIFICATION SUCCESSFUL
+[assertion.1] Range Check: FAILURE
+[assertion.2] Range Check: FAILURE


It'd probably be better to have a test where both failure and successes happen, and that's also testing some things like casting into a larger or smaller type

I've extended the existing test with a few more cases, making the range check pass as well. I'm not sure it cover all reasonable cases.

hannes-steffenhagen-diffblue

Some preliminary comments, not quite done reviewing yet

gnat2goto/driver/range_check.ads

gnat2goto/driver/tree_walk.adb

hannes-steffenhagen-diffblue · 2019-01-11T14:53:35Z

gnat2goto/driver/tree_walk.adb

+
+      function Build_Assert_Function return Symbol
+      is
+         Func_Type : constant Irep := New_Irep (I_Code_Type);


⛏️ All the ireps in here should have the source location of N attached to them, I don't think this necessarily needs to be done now though

Undone, only Class_Expr ireps can have source location.

hannes-steffenhagen-diffblue · 2019-01-11T15:38:48Z

gnat2goto/driver/tree_walk.adb

+
+      declare
+         R : constant Irep := New_Irep (I_Code_Assign);
+      begin


Why this change from the return to the declare form? AFAICT they're equivalent right?

The return was getting uncomfortably long, other than that I also think they are equivalent.

hannes-steffenhagen-diffblue · 2019-01-11T15:41:12Z

gnat2goto/driver/tree_walk.adb

                      (Intval (N), Pos (Constant_Width)));
+      else
+         Set_Value (Ret, UI_Image (Input  => Intval (N),


This bit is unrelated to the range checks right?

I'm not sure, I might have introduced it because the ranges were integer literals and this function did not handle them correctly. Maybe.

@xbauch this really needs some comments.
This change was prompted by something - please tell us the reason behind the 'else'.
If this is one of those 'this works' kind of things that is hazy - please tell us what didn't work.

@sonodtt I will find out and describe it in the code. It will take a bit longer though.

gnat2goto/driver/range_check.adb

gnat2goto/ireps/irep_specs/bounded_signedbv_type.json

testsuite/gnat2goto/tests/ranges/ranges.adb

hannes-steffenhagen-diffblue

This appears to work now, I still have some (mostly nitpicky) concerns left though

hannes-steffenhagen-diffblue · 2019-01-15T15:45:49Z

gnat2goto/driver/goto_utils.ads

@@ -29,6 +29,15 @@ package GOTO_Utils is
   function Symbol_Expr (Sym : Symbol) return Irep
   with Post => Kind (Symbol_Expr'Result) = I_Symbol_Expr;

+   function Create_Fun_Parameter (Fun_Name : String; Param_Name : String;


I think this should have at least a one line comment explaining what this function does, same with pretty much all the other new functions

hannes-steffenhagen-diffblue · 2019-01-15T15:57:57Z

gnat2goto/driver/goto_utils.adb

+                             Identifier      => Unintern (Func_Param_Id));
+   begin
+      A_Symbol_Table.Insert (Func_Param_Id, Value_Symbol);
+      Set_Type (Value_Arg, Param_Type);


Use the I_Type parameter of Make_Code_Parameter to set this

hannes-steffenhagen-diffblue · 2019-01-15T15:58:15Z

gnat2goto/driver/goto_utils.adb

+      A_Symbol_Table.Insert (Func_Param_Id, Value_Symbol);
+      Set_Type (Value_Arg, Param_Type);
+      Set_Identifier (Value_Arg, Unintern (Func_Param_Id));
+      Set_Base_Name (Value_Arg, "value");


The above two are already set by Make_Code_Parameter

hannes-steffenhagen-diffblue · 2019-01-15T16:02:12Z

gnat2goto/driver/tree_walk.adb

+      New_Symbol.Mode := Intern ("C");
+      New_Symbol.Value := Value;
+
+      if not (Global_Symbol_Table.Contains (Key => Intern (Name))) then


The else keys in this instance seems like it'd be an error

minor nit pick - I lean towards renaming this 'Add_To_Symbol_Table'.
Really happy that we start to have more utility functions - I think of them as good documentation (and they add robustness).
Might be helpful to add a comment w.r. to in which scenario Name and Basename should differ?
(or it will get used that one time it should not)

hannes-steffenhagen-diffblue · 2019-01-15T16:03:29Z

gnat2goto/driver/tree_walk.adb

 package body Tree_Walk is

   procedure Add_Entity_Substitution (E : Entity_Id; Subst : Irep);

   procedure Append_Declare_And_Init
     (Symbol : Irep; Value : Irep; Block : Irep; Source_Loc : Source_Ptr);

+   function Add_To_Table (Name : String; Symbol_Type : Irep; Value : Irep)


Could use a slightly clearer name. Maybe New_Symbol_Table_Entry or something like that?

hannes-steffenhagen-diffblue · 2019-01-15T16:04:57Z

gnat2goto/driver/tree_walk.adb

+         Func_Args : constant Irep := New_Irep (I_Parameter_List);
+         Func_Name : constant String :=
+           Fresh_Var_Name ("range_check");
+         Body_Block : constant Irep := New_Irep (I_Code_Block);


⛏️ I'd prefer Make_XXX functions in place of these

Func_Args => Func_Params (?)
( we do have argument vs parameter list and append_parameter vs append_argument)

hannes-steffenhagen-diffblue · 2019-01-15T16:06:25Z

gnat2goto/driver/tree_walk.adb

+   function Make_Range_Assert_Expr (N : Node_Id; Value : Irep;
+                                                 Value_Type : Irep)
+                                    return Irep
+   is


This could use a comment showing (in pseudocode) what kind of code is being generated here

hannes-steffenhagen-diffblue · 2019-01-15T16:32:14Z

gnat2goto/driver/tree_walk.adb

@@ -1575,25 +1788,12 @@ package body Tree_Walk is
            Sym_Nondet   : constant Irep :=
              Fresh_Var_Symbol_Expr (Type_Irep, Func_Str);
            SE_Call_Expr : constant Irep :=
-              New_Irep (I_Side_Effect_Expr_Function_Call);
+              Make_Assume_Expr (N, Make_Range_Expression (Sym_Nondet,


⛏️ It might make sense to put the definition of Make_Assume_Expr and Make_Assert_Call in a separate commit, although I'd see that as pretty optional

sonodtt · 2019-01-16T08:25:59Z

gnat2goto/driver/tree_walk.adb

+      New_Symbol.Mode := Intern ("C");
+      New_Symbol.Value := Value;
+
+      if not (Global_Symbol_Table.Contains (Key => Intern (Name))) then


minor nit pick - I lean towards renaming this 'Add_To_Symbol_Table'.
Really happy that we start to have more utility functions - I think of them as good documentation (and they add robustness).
Might be helpful to add a comment w.r. to in which scenario Name and Basename should differ?
(or it will get used that one time it should not)

sonodtt · 2019-01-16T08:35:30Z

gnat2goto/driver/tree_walk.adb

+         Func_Args : constant Irep := New_Irep (I_Parameter_List);
+         Func_Name : constant String :=
+           Fresh_Var_Name ("range_check");
+         Body_Block : constant Irep := New_Irep (I_Code_Block);


Func_Args => Func_Params (?)
( we do have argument vs parameter list and append_parameter vs append_argument)

sonodtt · 2019-01-16T08:50:38Z

gnat2goto/driver/tree_walk.adb

+
+         Set_Parameters (Func_Type, Func_Args);
+         Set_Return_Type (Func_Type, Actual_Type);
+         Set_Ellipsis (Func_Type, False);


Just wondering if we know why 'Set_Ellipsis' is required and has value False

It was among the things we thought might fix the parameter-assignment problem. It wasn't, but I think it denotes the use of parameter packs. There should be none, hence false.

sonodtt · 2019-01-16T09:08:47Z

gnat2goto/driver/tree_walk.adb

+   function Make_Assert_Call (N : Node_Id; Assertion : Irep;
+                                           Description : Irep)
+                             return Irep is
+      SE_Call_Expr : constant Irep :=


'SE_Call_Expr' - in particular the SE. This is no longer a side effect call.

xbauch · 2019-01-16T09:29:21Z

Added a commit that follows the comment suggestions (separate now to ease review). Will squash/reorder commits once approved.

NlightNFotis

LGTM

chrisr-diffblue · 2019-01-22T14:27:20Z

Needs a rebase, but otherwise LGTM

Introduces range check bounds stored in a vector and loaded explicitly when building the assertion for checking the range.

Automates creation of function parameters (including appending to arg list).

Slight refactor of the methods for working with assume/assert.

hannes-steffenhagen-diffblue suggested changes Dec 11, 2018

View reviewed changes

xbauch force-pushed the feature/range_check branch from e651ce3 to 0daa8bf Compare December 14, 2018 12:30

hannes-steffenhagen-diffblue reviewed Jan 8, 2019

View reviewed changes

xbauch force-pushed the feature/range_check branch 4 times, most recently from c00213b to 2b05e8a Compare January 11, 2019 14:26

hannes-steffenhagen-diffblue reviewed Jan 11, 2019

View reviewed changes

gnat2goto/ireps/irep_specs/bounded_signedbv_type.json Outdated Show resolved Hide resolved

testsuite/gnat2goto/tests/ranges/ranges.adb Outdated Show resolved Hide resolved

xbauch added bug Do not merge labels Jan 15, 2019

xbauch force-pushed the feature/range_check branch from 4d08f4b to fc32b97 Compare January 15, 2019 15:37

xbauch removed Do not merge bug labels Jan 15, 2019

hannes-steffenhagen-diffblue approved these changes Jan 15, 2019

View reviewed changes

sonodtt reviewed Jan 16, 2019

View reviewed changes

NlightNFotis approved these changes Jan 16, 2019

View reviewed changes

xbauch force-pushed the feature/range_check branch from 728c065 to e25a0cb Compare January 17, 2019 09:26

xbauch mentioned this pull request Jan 17, 2019

Testsuite/arrays #83

Merged

chrisr-diffblue approved these changes Jan 22, 2019

View reviewed changes

Petr Bauch added 4 commits January 22, 2019 16:02

Range Check package

d5b543c

Introduces range check bounds stored in a vector and loaded explicitly when building the assertion for checking the range.

Create Function Parameter + New Entry wrappers

f4c6109

Automates creation of function parameters (including appending to arg list).

Test expansion for range check

8ad8813

Use CProver assert for range checking

f442210

Slight refactor of the methods for working with assume/assert.

xbauch force-pushed the feature/range_check branch from e25a0cb to f442210 Compare January 22, 2019 16:02

xbauch merged commit dfe5c87 into diffblue:master Jan 22, 2019

xbauch deleted the feature/range_check branch March 14, 2019 10:23

Range check via Cprover assert #91

Range check via Cprover assert #91

Uh oh!

Conversation

xbauch commented Dec 11, 2018

Uh oh!

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

xbauch commented Dec 14, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment