Introduce temporary stack variables for getfield/-static and ?load by mgudemann · Pull Request #931 · diffblue/cbmc

mgudemann · 2017-05-16T20:57:43Z

When a value is pushed on the stack, it must be ensured that modification of the
origin will not modify the values on the stack.

mgudemann · 2017-05-16T21:03:25Z

this fixes the obvious cases, regression tests and thinking about possibly other cases is needed

mgudemann · 2017-05-16T21:09:39Z

strong candidates for additional cases:

?aload - returns a reference to an element in an array
dup? - duplicates entries on the stack, only values should be duplicated

peterschrammel

Do you have tests that expose the bug?

mgudemann · 2017-05-17T07:57:02Z

one is the code in #926 where the assert currently still succeeds (which is shouldn't) but the accessed index is the correct one now

mgudemann · 2017-05-17T07:58:58Z

instead of

        n = n + (int)1;
        // 63 file incr.java line 7 function java::incr.f:(I)V bytecode_index 8
        ASSERT n >= 0 // Array index < 0
        // 64 file incr.java line 7 function java::incr.f:(I)V
        ASSERT !(this == null) // reference is null in *((struct incr *)(void *)this)
        // 65 file incr.java line 7 function java::incr.f:(I)V
        ASSERT !(this->nums == null) // reference is null in *((struct java::array[int] *)((struct incr *)(void *)this)->nums)
        // 66 file incr.java line 7 function java::incr.f:(I)V bytecode_index 8
        ASSERT n < ((struct java::array[int] *)((struct incr *)(void *)this)->nums)->length // Array index >= length
        // 67 file incr.java line 7 function java::incr.f:(I)V
        ASSERT !(this->nums->data + n == null) // reference is null in this->nums->data[n]
        // 68 file incr.java line 7 function java::incr.f:(I)V bytecode_index 10
        IF this->nums->data[n] == 2 THEN GOTO 1

it's now

        stack_field_tmp2 = ((struct incr *)stack_var_tmp1)->nums;
        // 78 file incr.java line 7 function java::incr.f:(I)V bytecode_index 6
        stack_var_tmp3 = n;
        // 79 file incr.java line 7 function java::incr.f:(I)V bytecode_index 7
        n = n + (int)1;
        // 80 file incr.java line 7 function java::incr.f:(I)V bytecode_index 8
        ASSERT stack_var_tmp3 >= 0 // Array index < 0
        // 81 file incr.java line 7 function java::incr.f:(I)V
        ASSERT !(stack_field_tmp2 == null) // reference is null in *((struct java::array[int] *)stack_field_tmp2)
        // 82 file incr.java line 7 function java::incr.f:(I)V bytecode_index 8
        ASSERT stack_var_tmp3 < ((struct java::array[int] *)stack_field_tmp2)->length // Array index >= length
        // 83 file incr.java line 7 function java::incr.f:(I)V
        ASSERT !(stack_field_tmp2->data + stack_var_tmp3 == null) // reference is null in stack_field_tmp2->data[stack_var_tmp3]
        // 84 file incr.java line 7 function java::incr.f:(I)V bytecode_index 10
        IF !(stack_field_tmp2->data[stack_var_tmp3] == 2) THEN GOTO 2

smowton

A possibility for the future to obtain correctness without dramatic uglification of the code: create the temp variables only when we come across an instruction that writes while there are reads on the stack (e.g. before an astore, for each operand it would not remove from the stack and which is non-constant, now synthesise temporary names to store them; in the common case that there are no such non-constants held over the write op (i.e. the write op drains the stack) we could still produce brief code as we do now.

However this is trickier, so this fix is probably the right way to go for now.

tautschnig · 2017-05-17T11:55:19Z

Can this please not be merged without regression tests being added? (Also all three checks are failing at the moment.)

mgudemann · 2017-05-17T12:00:01Z

@tautschnig the regression tests are fixed, I will add specific ones for this, too
currently I am adapting the variants of dup

mgudemann · 2017-05-19T07:08:50Z

@tautschnig I added regression tests for the bytecode instructions in question

@smowton you are right about polluting the GOTOs, effectively this partially recreates the stack state now, which is sub-optimal.
If I understand correctly, you propose changing the "dual" instructions (?store instead of ?load, ?putfield instead of ?getfield etc.) in a way that saves the variables / references that remain on the stack after the write into temporary variables. Now that regression tests exist to validate the implementation, I will have a look at that.

tautschnig · 2017-05-19T08:13:12Z

regression/cbmc-java/stack_var1/stack_var1.j

@@ -0,0 +1,22 @@
+.class public stack_var1


Why is this file (and the other .j files) included?

these are the source files I used to create the classes. This is very bytecode specific, in particular the dup2_x? are very rare, so I used the jasmin assembler to create the regression tests.

Ah, cool. Would you mind adding information in either the commit message or some extra readme file so that these steps become reproducible? I had naively thought that the .class files had been produced from the accompanying .java.

ok, will do, the stack_test.java is always the entry point and creates an object instance of the class created via jasmin.

tautschnig · 2017-05-19T12:09:33Z

regression/cbmc-java/stack_var1/README

Would it be possible to add as many details as possible, such as the precise command line? This is information that you've now got right at hand, but it will be much more work to reproduce later on. Memory is weak, git is strong!

:-) it is actually jasmin $FILE.j but I'll add this to the READMEs

I added some comments about jasmin, how to get it and how to use it on .j files

mgudemann · 2017-05-23T20:14:44Z

see #951 for an alternative fix working on the write instructions

mgudemann · 2017-05-25T19:59:14Z

superseded by #951 which takes a different approach that creates less temporary variables

mgudemann mentioned this pull request May 16, 2017

array index off by one #926

Closed

peterschrammel requested review from peterschrammel and smowton May 17, 2017 07:35

peterschrammel reviewed May 17, 2017

View reviewed changes

smowton approved these changes May 17, 2017

View reviewed changes

mgudemann force-pushed the fix/bytecode_args_push_on_stack branch 3 times, most recently from 88d5080 to 9f41808 Compare May 18, 2017 09:25

Matthias Güdemann added 6 commits May 18, 2017 20:44

Introduce temporary stack variables for ?load / ?aload

2e4e0b5

Introduce temporary stack variables for dup, dup_x1, dup_x2

d9e3bbc

Introduce temporary stack variable for getfield

319ff01

Introduce temporary stack variable for getstatic

75b770b

Introduce temporary stack variables for dup_2, dup2_x1, dup2_x2

3569806

Adapt existing regression tests

74ac6e1

mgudemann force-pushed the fix/bytecode_args_push_on_stack branch 2 times, most recently from 78ffc65 to 6303a86 Compare May 19, 2017 06:50

Matthias Güdemann added 3 commits May 19, 2017 08:57

Add regression tests for iload, dup, dup_x1, dup_x2

3f5dac8

Add regression tests for dup2, dup2_x1 and dup2_x2

0aec9b1

Add regression test for getfield, getstatic

8cacd7d

mgudemann force-pushed the fix/bytecode_args_push_on_stack branch from 6303a86 to 8cacd7d Compare May 19, 2017 06:58

tautschnig reviewed May 19, 2017

View reviewed changes

Add README to tests pointing to jasmin bytecode assembler

52f522d

mgudemann force-pushed the fix/bytecode_args_push_on_stack branch from 67d361d to 52f522d Compare May 19, 2017 12:30

Do not duplicate constant value as temporary variables

fc1a852

mgudemann mentioned this pull request May 22, 2017

Fix/bytecode args write from stack #951

Merged

mgudemann closed this May 25, 2017

mgudemann mentioned this pull request Jul 2, 2018

fix type inconsistencies when using temporary #2498

Closed

Conversation

mgudemann commented May 16, 2017

Uh oh!

mgudemann commented May 16, 2017

Uh oh!

mgudemann commented May 16, 2017

Uh oh!

peterschrammel left a comment

Choose a reason for hiding this comment

Uh oh!

mgudemann commented May 17, 2017

Uh oh!

mgudemann commented May 17, 2017

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented May 17, 2017

Uh oh!

mgudemann commented May 17, 2017

Uh oh!

mgudemann commented May 19, 2017

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!

mgudemann commented May 23, 2017

Uh oh!

mgudemann commented May 25, 2017

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants