Testsuite/arrays #83

xbauch · 2018-11-28T13:41:37Z

Building on #79 (thus only the last commit is new) this fixes the arrays test to the point that CBMC parses it. The symex takes a lot of time though.

sonodtt

Approved with remarks. - update: blocked -

sonodtt · 2018-12-04T08:18:39Z

gnat2goto/driver/tree_walk.adb

+         Alloc_Symbol.Name := Intern (Alloc_Name);
+         Alloc_Symbol.PrettyName := Alloc_Symbol.Name;
+         Alloc_Symbol.BaseName := Alloc_Symbol.Name;
+         Alloc_Symbol.Mode := Intern ("C");


I don't see any use of Alloc_Symbol.Value (so no body?) - or further use of Alloc_Symbol.
Just flagging this.
Not enough gnat2goto experience to say if this is likely a problem going forward.

Here CBMC was complaining that __new__array is not in the symbol table, but it only needed declaration: the definition is in the builtin functions. So I thought the body would be ignored anyway.

FYI. Mostly for future stuff. No big deal - but I get this on the cbmc side:
"**** WARNING: no body for function __new_array"
I think an empty body will do? (this will pass the goto-program validation) - what happens is that if a function is declared but not called (no fn pointer taken etc), then it would not go into the goto-program function_map (nb I havent' verified symbol-table but I think this points to same behaviour). When it is used in any fashion (not just called, e.g. function address is taken to initialise a fn pointer) - then an empty body gets created even when there is only a declaration visible in the sourcecode.
Just a FYI for context - of behaviour that I came across in goto-program validation. So empty body should suffice (fingers crossed).
I'd say this can be fixed later - it is just a warning. ( /opinion )

Empty body might do, but I'm not sure how to create one in gnat2goto. Make_Nil results in the same warning and New_Irep (I_Code_Block) breaks CBMC.

Ok. Thanks for extra effort + info - will look into it as part of the array epic.

sonodtt · 2018-12-04T08:20:30Z

gnat2goto/driver/tree_walk.adb

         Set_Cond (Body_Loop, Loop_Test);
+         Set_Init (I     => Body_Loop,
+                   Value => Make_Nil (Sloc (RHS_Element_Type)));


Have not seen use of aligned name parameters elsewhere - and surprised this passes the compiler?
If it passes, fine, but there's no precedent for this code style.
Nitpick.

Not sure, but GPS provides this layout as a part of it's auto-completion. I mostly like it, but it can get very verbose sometimes.

I've seen this code style in other parts of GNAT.

sonodtt · 2018-12-04T08:33:11Z

gnat2goto/driver/tree_walk.adb

@@ -3870,6 +3882,8 @@ package body Tree_Walk is
         Append_Argument (Call_Args, Param_Symbol (Ptr_Arg));
         Append_Argument (Call_Args, Param_Symbol (Len_Arg));
         Set_Arguments (Call_Inst, Call_Args);
+         Set_Lhs (I     => Call_Inst,


Lhs_fun_call is set to the LHS of the returned duplicator function. Not sure why it needs that on top of the function return value (?) It's all a bit voodoo...

I though about it a bit, and it sort of makes sense, i.e. to require function calls to have left-hand sides. Even if a function has a return value, if we didn't store it in the lhs, it would get lost.

Hmm. You're saying as a temporary. I think this could therefore be implicit in the make_code_function_call bla bla function.
The return value would be assigned at the call location - or the function can be called for its side effects (temporary not needed).
But nevermind. If that's how it is - that's how it is.

I find it unfortunate that the relevant Irep does not require the lhs given that CBMC will fail. I'm not sure if make-function-call is the only place a function can be created, but yes: you are right.

NlightNFotis · 2018-12-11T16:43:54Z

testsuite/gnat2goto/tests/arrays/test.out

@@ -0,0 +1,2 @@
+VERIFICATION SUCCESSFUL
+q


What is q here?

It's probably an emacs thing.

sonodtt

PR will require additional work to fix the non-terminating loop unrolling in goto-symex. This is WIP by @sonodtt.

sonodtt · 2019-01-08T10:54:31Z

PR will require additional work to investigate and fix issue w.r. to error
"raised CONSTRAINT_ERROR : Symbol_Table_Info.Symbol_Maps.Insert: attempt to insert key already in map"
Minimal reproduction: define an array of int and also an array of floats.
Investigation WIP by @sonodtt - as part of the general 'fix array stuff' https://diffblue.atlassian.net/browse/ADA-223

xbauch · 2019-01-17T09:30:21Z

Now builds on #91 --> only review the last two commits.

hannes-steffenhagen-diffblue

This needs a lot of cleanup before being merged, i.e. removing "note" type comments, removing unrelated changes, removing commented out code and getting changes into a logical order.

hannes-steffenhagen-diffblue · 2019-01-18T11:21:01Z

testsuite/gnat2goto/tests/func_args/func_args.adb

@@ -7,6 +7,6 @@ procedure Func_Args is
   end;
 begin
   C := Assign2 (A + B, B);
-   pragma Assert (C = 7);
+   pragma Assert (C = 5);


This appears to be unrelated to arrays?

hannes-steffenhagen-diffblue · 2019-01-18T11:22:25Z

gnat2goto/driver/tree_walk.adb

@@ -803,6 +805,7 @@ package body Tree_Walk is
      end if;
      LHS_Idx_Type := Get_Array_Index_Type (Name (N));
      RHS_Idx_Type := Get_Array_Index_Type (Expression (N));
+      --  LHS_Length := Make_Integer_Constant (2, LHS_Idx_Type);


why is commented out code being added here?

Sorry, removed.

hannes-steffenhagen-diffblue · 2019-01-18T12:51:39Z

gnat2goto/driver/driver.adb

+         Builtin   : Symbol;
+         Type_Irep : constant Irep := New_Irep (I_Unsignedbv_Type);
+      begin
+         Set_Width (Type_Irep, 64);


Probably shouldn't be a magic number, but for now we're probably alright in most circumstances. I can think of a few ways to make this more robust, but none of them are particularly nice. I'd just keep a reminder comment in here for now pointing out that this is an assumption, and moreover one that doesn't necessarily hold for target platforms...

hannes-steffenhagen-diffblue · 2019-01-18T13:20:40Z

gnat2goto/driver/tree_walk.adb

-            Alloc_Symbol.Mode := Intern ("C");
-            Global_Symbol_Table.Insert (Intern (Alloc_Name), Alloc_Symbol);
-         end if;
+--           if not (Global_Symbol_Table.Contains (Intern (Alloc_Name)))


Commented out code?

hannes-steffenhagen-diffblue · 2019-01-18T13:20:59Z

gnat2goto/driver/tree_walk.adb

+                              Source_Location => Source_Loc)),
+                                  Body_Block, 0);
+         --  --------------------------------------------------
+         --  TYPECAST VERSION


Commented out code?

Well there were two versions and we wanted to get opinions as to which would be better. I removed the less generic version.

hannes-steffenhagen-diffblue · 2019-01-18T13:23:07Z

gnat2goto/driver/driver.adb

@@ -248,6 +248,7 @@ package body Driver is

         Global_Symbol_Table.Insert (Start_Name, Start_Symbol);
         Follow_Type_Declarations (Global_Symbol_Table, Followed_Symbol_Table);
+         --  Followed_Symbol_Table.Exclude (Intern ("malloc"));


Commented out code?

hannes-steffenhagen-diffblue · 2019-01-18T13:26:08Z

gnat2goto/driver/tree_walk.adb

@@ -1114,6 +1276,7 @@ package body Tree_Walk is
      U           : constant Node_Id := Unit (N);
      Unit_Symbol : Symbol;
   begin
+      Add_Malloc_Symbol;


No, this should probably go into driver.adb or something. I don't think it makes sense to do this once per compilation unit.

hannes-steffenhagen-diffblue · 2019-01-18T13:52:18Z

gnat2goto/driver/tree_walk.adb

+                               Range_Check     => False,
+                               Value           =>
+                    Convert_Uint_To_Hex (Value     => Esize (Element_Type) / 8,
+                                         Bit_Width => 32));


Why 32 if we hardcoded size_t to 64 bits?

hannes-steffenhagen-diffblue · 2019-01-18T14:27:20Z

testsuite/gnat2goto/tests/arrays/arrays.adb

-   Actual3 (13 .. 16) := Actual3 (11 .. 12) & Actual3 (15 .. 16);
-   Array_Attribs := Actual3'First + Actual3'Last + Actual3'Length;
+   Actual7(1) := 2;
+--   pragma Assert(Actual7(1) =2);


What does this fail with?

Somewhere in symex flattening. #108

xbauch · 2019-01-18T15:34:48Z

@hannes-steffenhagen-diffblue I split it a bit more meaningfully (the last 7 commits belong here).

xbauch · 2019-01-24T12:57:55Z

@sonodtt and @hannes-steffenhagen-diffblue this is now ready for another set of review. I've only added the malloc size fix and a failing test.

sonodtt · 2019-01-25T10:23:08Z

testsuite/gnat2goto/tests/arrays_access/arrays_access.adb

@@ -0,0 +1,7 @@
+procedure Arrays_Access is
+   type Arr7 is array (1 .. 3) of Integer;


Nitpick. Rename to Arr3 and Actual3? (or just Arr and Actual)

sonodtt · 2019-01-25T10:28:06Z

I'm not sure we should be removing the body of the old array tests, which documents what was intended to pass as a minimal based on expected state of gnat2goto.
Sure, it fails, in multiple locations, atm. But we can keep it around as a failing test?
You'll need a test that passes - which you have now have so I'd suggest naming the new test e.g. "write_to_array_element.adb"

sonodtt

Approved - subject to consensus on tests.

chrisr-diffblue

I agree with @sonodtt - we shouldn't be removing tests which currently fail. A better approach would be to split the tests into several parts, then XFAIL the ones that currently fail.

sonodtt · 2019-01-25T11:55:55Z

gnat2goto/driver/tree_walk.adb

+           Make_Code_Return (Return_Value    => Array_Copy,
+                             Source_Location => Source_Loc);
+
+         --  NEW VARS FOR MALLOC ALLOCATION


If we preserve this line (I'm in favour), then lowercase (and remove 'new')?

hannes-steffenhagen-diffblue

This is dealing with the main problem we've been having

hannes-steffenhagen-diffblue · 2019-01-25T12:01:19Z

gnat2goto/driver/tree_walk.adb

+
+      --  Build a functions:
+      --  n.b.: the typecast is optional
+      --  void copy_array(lhs_type* out, rhs_type* in, int len) {


I've been wondering - isn't this basically just memcpy? We do model that, for instance a C-program like this:

#include <string.h> #include <assert.h> #include <stdlib.h> int main(void) { const int array_size = 10; int *arr = malloc(sizeof(int) * array_size); int *arr_copy = malloc(sizeof(int) * array_size); for(int i = 0; i < array_size; ++i) { arr[i] = i; } memcpy(arr_copy, arr, sizeof(int)*array_size); for(int i = 0; i < array_size; ++i) { assert(arr_copy[i] == i); } }

can be verified just fine. I understand you were having troubles with this function, so maybe that can be mitigated this way? (i.e. you should be able to just call it the same way you deal with malloc)

will try, ta.

hannes-steffenhagen-diffblue · 2019-01-25T12:04:22Z

testsuite/gnat2goto/tests/arrays_access/arrays_access.adb

@@ -0,0 +1,7 @@
+procedure Arrays_Access is
+   type Arr7 is array (1 .. 3) of Integer;
+   Actual7 : Arr7 := (1,2,3);


Is this the bit that's triggering your problems with array_copy on the assign/read task? What if you leave it off, i.e. leave Actual7 uninitialized like this: Actual7 : Arr7;?

It helped a bit, ta.

Use wrappers for creating parameters and function symbols.

Use wrappers for calling malloc, param creation, etc.

Test tries to write and read from and array index.

xbauch · 2019-01-25T17:06:05Z

@chrisr-diffblue I've reverted the removal of the original test, adding a new, passing one.

sonodtt approved these changes Dec 4, 2018

View reviewed changes

xbauch force-pushed the testsuite/arrays branch 2 times, most recently from 7a485c3 to 4abda44 Compare December 4, 2018 13:39

xbauch added bug Do not merge and removed Do not merge bug labels Dec 4, 2018

xbauch force-pushed the testsuite/arrays branch from 034d29b to 642030c Compare December 6, 2018 16:10

sonodtt mentioned this pull request Dec 11, 2018

Replace cpp new with malloc call sonodtt/gnat2goto#2

Open

NlightNFotis reviewed Dec 11, 2018

View reviewed changes

xbauch force-pushed the testsuite/arrays branch from 642030c to 43d51fc Compare December 11, 2018 16:59

sonodtt added the Do not merge label Dec 14, 2018

sonodtt suggested changes Dec 14, 2018

View reviewed changes

xbauch force-pushed the testsuite/arrays branch from 43d51fc to 154dac8 Compare January 17, 2019 09:28

xbauch force-pushed the testsuite/arrays branch 3 times, most recently from 58b3137 to 3bc2d5a Compare January 18, 2019 11:11

hannes-steffenhagen-diffblue suggested changes Jan 18, 2019

View reviewed changes

xbauch force-pushed the testsuite/arrays branch 2 times, most recently from 3136897 to e4c0de6 Compare January 18, 2019 15:33

xbauch force-pushed the testsuite/arrays branch 2 times, most recently from dd7abf0 to 1cae3dc Compare January 21, 2019 09:59

chrisr-diffblue removed the Do not merge label Jan 24, 2019

chrisr-diffblue assigned chrisr-diffblue, sonodtt and hannes-steffenhagen-diffblue Jan 24, 2019

xbauch force-pushed the testsuite/arrays branch from 1cae3dc to 4dc8bd5 Compare January 24, 2019 12:43

xbauch force-pushed the testsuite/arrays branch from 4dc8bd5 to 8f9d75b Compare January 24, 2019 12:52

sonodtt reviewed Jan 25, 2019

View reviewed changes

sonodtt approved these changes Jan 25, 2019

View reviewed changes

chrisr-diffblue suggested changes Jan 25, 2019

View reviewed changes

sonodtt reviewed Jan 25, 2019

View reviewed changes

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

View reviewed changes

Sonny Martin and others added 7 commits January 25, 2019 16:42

Introduce malloc building function

7aac448

Add lhs to function call

e9f1851

Rewrite get_array_copy_function

930cd1a

Use wrappers for creating parameters and function symbols.

Rewrite get_array_dup_function

bbb6646

Use wrappers for calling malloc, param creation, etc.

Add precondition where appropriate

e98f7c7

Add malloc and size_t symbols

9437f0d

Add failing test

5241db6

Test tries to write and read from and array index.

xbauch force-pushed the testsuite/arrays branch 2 times, most recently from 3dd023f to 965aa1a Compare January 25, 2019 17:05

Add succeeding test

007a82c

xbauch force-pushed the testsuite/arrays branch from 965aa1a to 007a82c Compare January 28, 2019 08:17

chrisr-diffblue approved these changes Jan 28, 2019

View reviewed changes

chrisr-diffblue merged commit c61cba5 into diffblue:master Jan 28, 2019

xbauch deleted the testsuite/arrays branch March 14, 2019 10:24

		@@ -0,0 +1,7 @@
		procedure Arrays_Access is
		type Arr7 is array (1 .. 3) of Integer;

Testsuite/arrays #83

Testsuite/arrays #83

Uh oh!

Conversation

xbauch commented Nov 28, 2018

Uh oh!

sonodtt left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

sonodtt Dec 7, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

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!

sonodtt left a comment

Choose a reason for hiding this comment

Uh oh!

sonodtt commented Jan 8, 2019

Uh oh!

xbauch commented Jan 17, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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

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!

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

sonodtt left a comment •

edited

Loading

sonodtt Dec 7, 2018 •

edited

Loading

xbauch commented Jan 17, 2019 •

edited

Loading

sonodtt Jan 25, 2019 •

edited

Loading

sonodtt commented Jan 25, 2019 •

edited

Loading

sonodtt Jan 25, 2019 •

edited

Loading