Handle representation clause address #233

xbauch · 2019-05-17T12:33:39Z

Ada allows specifying the memory address for variables (which do not have to be pointers). To replicate it in C (without relying on some special compilers) we introduce a new variable of type pointer-to-original-type, change its address, and then redirect every reference to the original variable to the new pointer-to variable. The redirection takes place after the tree-walk parsing, on the irep-level, in a similar fashion as the follow_irep.

hannes-steffenhagen-diffblue · 2019-05-20T14:48:29Z

gnat2goto/driver/tree_walk.adb

+            --
+            --  Produce this C code:
+            --------------------
+            --  &Var = (VarType*)system__to_address(hex_address);


Is the system__to_address here necessary? Seems to me that just casting the hex address directly to a pointer should work just as well.

I also don't really know what this means, addresses aren't assignable in C proper. Are addresses assignable in GOTO code?

You mean like this?:

#include <assert.h> int main() { int *var = (int*)0x40001000; *var = 4; assert(*(int*)0x40001000==4); assert(var==0x40001000); assert(*var==4); return 0; }

hannes-steffenhagen-diffblue

I think this may be reasonable

hannes-steffenhagen-diffblue · 2019-06-06T15:26:27Z

gnat2goto/driver/goto_utils.adb

@@ -503,14 +498,25 @@ package body GOTO_Utils is
      return False;
   end Has_GNAT2goto_Annotation;

+   function Integer_Constant_To_BV_Expr


I don't quite understand, are there non-bitvector types to which this is applicable?

Also, seems like this could be its own PR

The CPROVER_Size_T is not a bit-vector type.

hannes-steffenhagen-diffblue · 2019-06-06T15:29:43Z

gnat2goto/driver/tree_walk.adb

+            begin
+               New_Object_Symbol_Entry
+                 (Object_Name       =>
+                    Intern ("Ptr_" & Get_Identifier (Target_Name)),


This name could conceivably already exist in the symbol table, how about Get_Identifier (Target_Name) & "$Ptr? Names with $ in them are valid in cbmc, but I don't think they're valid in Ada.

The dollar sounds like a good idea, I wasn't sure what decoration would be safe.

Here: 43c5e3f.

hannes-steffenhagen-diffblue · 2019-06-06T16:08:56Z

testsuite/gnat2goto/tests/representation_clause_address/test.adb

+   for Device_Input_Value'Address use System'To_Address (16#8000_05C4#);
+begin
+   Device_Input_Value := 5;
+   pragma Assert (Device_Input_Value + 1 = 6);


Can you also do pragma Assert (Device_Input_Value'Address = System'To_Address (16#8000_05C4#));

This one is a bit more tricky: bb7f3ad -- f2356d1.

Had a conversation with @martin-cs OOB: that will require diffblue/cbmc#1086 to be completed and merged first.

NlightNFotis

LGTM overall, minor comments.

NlightNFotis · 2019-06-07T13:55:08Z

gnat2goto/ireps/ireps-wrap_pointer.adb

+--  Ireps were disappearing when new list was created (even if it was filled
+--  with the same ireps).
+-------------------------------------------------------------------------------
+separate (Ireps)


Oh nice, didn't even know what this was or what it could do.

Well neither did I initially, but it was used before in ireps.

NlightNFotis · 2019-06-07T13:59:07Z

gnat2goto/driver/goto_utils.adb

@@ -153,6 +153,7 @@ package body GOTO_Utils is



Slightly confused with the commit message here. Should it read "Add default body for some subprograms and add that to those that have identity-like type"?

Sorry about the confusion, no: the commit body only specifies which are the some subprogram for which we generate the default body (those that have identity-like type, etc.).

We now have three wrappers: 1: takes values (results has type cprover_size_t) 2: takes value, type (type is assumed to be bit-vector) 3: takes value, type, bit-width.

We handle it by 1: declaring a new variable with type one pointer deeper 2: assign the address to it 3: store the name (we'll need to replace it in the symbol table -- next commit)

And that those for which the address was specified (via clause). We chase them using the same idea as follow_irep and replace their symbol expression with dereference expression to the newly introduced pointer-to symbol.

into the symbol table. Since it was missing and CBMC need it for pointer analysis.

with dollar sign and via a helper function.

by returning address-of expression.

and that to those that have identity-like type: A -> A. The default body is exactly that identity. And their name starts with "system".

chrisr-diffblue · 2019-06-07T16:51:06Z

I slightly worry that this mechanism might change the semantics of the Ada program, just because what was a bunch of straight forward assignments or reads to/from variables now includes dereference operations. I don't honestly know what other options we have though. Is it worth looking at the linker script stuff in CBMC and see if there is any code you can either piggy back on, or something you can copy to use here? e.g. If your compiler doesn't support something like __atttribute__((at(0xabcde))) but does support linker scripts (e.g. gcc) then typically what you'd do is declare your variable as something like:
int foo __attribute__((section ("FOOSEC"))) and then have a linker script that places section "FOOSEC" at a specific address, e.g.

SECTIONS
{
.fooSecRange 0xABCDEF :
{
KEEP (*(.FOOSEC))
}
}

paraphrasing slightly as I'm going mostly by memory - don't trust the actual syntax there... It looks like CBMC has some support for this sort of thing in src/goto-cc/linker_script_merge.cpp - so there might be some clues there?

chrisr-diffblue · 2019-06-13T13:23:51Z

@martin-cs - would be good to have some input from you here too as you may have other thoughts about how this could be implemented.

martin-cs · 2019-06-13T14:04:23Z

I know Michael and Kareem were working on similar things; I will have a chat with them.

xbauch · 2019-06-25T08:45:18Z

Hello @tjj2017, have you seen this PR? Chris said you might be working on something related to address clause. Just wanted to avoid duplicating effort.

xbauch added the Do not merge label May 17, 2019

hannes-steffenhagen-diffblue reviewed May 20, 2019

View reviewed changes

chrisr-diffblue added the draft label Jun 4, 2019

chrisr-diffblue changed the title ~~Handle representation clause address [depends-on: #218]~~ Handle representation clause address Jun 4, 2019

xbauch self-assigned this Jun 5, 2019

xbauch force-pushed the feature/representation-clause-address branch 2 times, most recently from 4c4708d to 512e734 Compare June 6, 2019 13:45

xbauch changed the title ~~Handle representation clause address~~ Handle representation clause address [depends-on: #231, #251] Jun 6, 2019

xbauch marked this pull request as ready for review June 6, 2019 13:47

xbauch removed the draft label Jun 6, 2019

xbauch removed their assignment Jun 6, 2019

hannes-steffenhagen-diffblue approved these changes Jun 6, 2019

View reviewed changes

xbauch force-pushed the feature/representation-clause-address branch from f8b4bdd to e2d420f Compare June 7, 2019 11:40

xbauch changed the title ~~Handle representation clause address [depends-on: #231, #251]~~ Handle representation clause address Jun 7, 2019

xbauch removed the Do not merge label Jun 7, 2019

xbauch changed the title ~~Handle representation clause address~~ Handle representation clause address [depends-on: #237] Jun 7, 2019

xbauch added the Do not merge label Jun 7, 2019

xbauch force-pushed the feature/representation-clause-address branch from 89d770a to 94ef023 Compare June 7, 2019 12:11

NlightNFotis approved these changes Jun 7, 2019

View reviewed changes

petr-bauch added 11 commits June 7, 2019 17:03

Unify creating integer constants

b1567bc

We now have three wrappers: 1: takes values (results has type cprover_size_t) 2: takes value, type (type is assumed to be bit-vector) 3: takes value, type, bit-width.

Implement representation clause address

1f7f49a

We handle it by 1: declaring a new variable with type one pointer deeper 2: assign the address to it 3: store the name (we'll need to replace it in the symbol table -- next commit)

Wrap selected symbol in a dereference expression

2db62c7

And that those for which the address was specified (via clause). We chase them using the same idea as follow_irep and replace their symbol expression with dereference expression to the newly introduced pointer-to symbol.

Introduce cprover_memory

3f2cd54

into the symbol table. Since it was missing and CBMC need it for pointer analysis.

Testcase for representation clause address

22d8f04

Decorate addressed variables

a80baf8

with dollar sign and via a helper function.

Implement handling the address attribute

1b3ba7f

by returning address-of expression.

Implement checking string prefix

2e228e2

Add default body for some subprograms

35808eb

and that to those that have identity-like type: A -> A. The default body is exactly that identity. And their name starts with "system".

Extend the test to check the address

0c60e2b

Update golden results

743d8d9

xbauch force-pushed the feature/representation-clause-address branch from 94ef023 to 743d8d9 Compare June 7, 2019 16:03

xbauch removed the Do not merge label Jun 7, 2019

xbauch changed the title ~~Handle representation clause address [depends-on: #237]~~ Handle representation clause address Jun 7, 2019

xbauch added Do not merge Work in progress labels Jun 10, 2019

chrisr-diffblue assigned martin-cs and xbauch Jun 13, 2019

martin-cs mentioned this pull request Jun 27, 2019

Address clause #260

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Handle representation clause address #233

Handle representation clause address #233

xbauch commented May 17, 2019 •

edited

Loading

hannes-steffenhagen-diffblue May 20, 2019

xbauch May 20, 2019

hannes-steffenhagen-diffblue left a comment

hannes-steffenhagen-diffblue Jun 6, 2019

xbauch Jun 6, 2019

hannes-steffenhagen-diffblue Jun 6, 2019

xbauch Jun 6, 2019

xbauch Jun 7, 2019 •

edited

Loading

hannes-steffenhagen-diffblue Jun 6, 2019

xbauch Jun 7, 2019 •

edited

Loading

tautschnig Jun 14, 2019

NlightNFotis left a comment

NlightNFotis Jun 7, 2019

xbauch Jun 7, 2019

NlightNFotis Jun 7, 2019

xbauch Jun 7, 2019

chrisr-diffblue commented Jun 7, 2019

chrisr-diffblue commented Jun 13, 2019

martin-cs commented Jun 13, 2019

xbauch commented Jun 25, 2019

Handle representation clause address #233

Are you sure you want to change the base?

Handle representation clause address #233

Conversation

xbauch commented May 17, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

xbauch Jun 7, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

xbauch Jun 7, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NlightNFotis left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

chrisr-diffblue commented Jun 7, 2019

chrisr-diffblue commented Jun 13, 2019

martin-cs commented Jun 13, 2019

xbauch commented Jun 25, 2019

xbauch commented May 17, 2019 •

edited

Loading

xbauch Jun 7, 2019 •

edited

Loading

xbauch Jun 7, 2019 •

edited

Loading