[depends: #1330] Interpreter fixes #1274

tautschnig · 2017-08-22T15:52:43Z

None of this is my work - these are commits already merged into develop (test-gen-support).

allredj

I don't know much about this code, but I suppose it's alright if it's taken out directly from develop, and if Travis passes.

tautschnig · 2017-08-22T16:25:28Z

FWIW I just added as reviewers all those that have at least one commit in this series.

tautschnig · 2017-08-22T17:33:29Z

I'm looking at the linter failures and will submit a pull request to develop to address those first.

peterschrammel · 2017-08-22T21:13:02Z

src/goto-programs/interpreter_class.h

    mp_integer value;
+    // Initialized is annotated even during reads
+    // Set to 1 when written-before-read, -1 when read-before-written
+    mutable char initialized;


Probably, this should be turned into a three-valued enum.

This is now #1289.

peterschrammel · 2017-08-22T21:15:27Z

src/goto-programs/interpreter.cpp

 }

+/// retrieves the member at offset
+/// \par parameters: an object and a memory offset


git grep -w '\\par' | wc -l yields 273 -- I'll start fixing this, but it looks like a somewhat larger documentation cleanup.

mgudemann

LGTM, but I have not much insight in the code of the interpreter

mgudemann · 2017-08-23T11:27:28Z

src/goto-programs/interpreter_evaluate.cpp

+  mp_vectort &dest) const
+{
+  // copy memory region
+  std::size_t address_val=integer2size_t(address);


could be const, too

I have added this to #1289.

mgudemann · 2017-08-23T11:28:14Z

src/goto-programs/interpreter_evaluate.cpp

+
+/// reserves memory block of size at address
+void interpretert::allocate(
+  mp_integer address,


const reference ?

I have added this to #1289.

smowton · 2017-08-23T14:41:24Z

Happy with the smaller commits (perhaps consider folding the final bugfix commit into the appropriate sparse-vector commit?), the first one is too big to review meaningfully though. It looks like it is itself a big merge -- any chance of finding the original commits that constituted it?

tautschnig · 2017-08-23T15:15:32Z

@smowton Thanks a lot for the feedback; are you referring to ac2e5b3 as the big one? @mgudemann would you have any input on where this has come from?

…entifier

…o trace

to_ulong() will negate a negative number, rather than returning its two's complement representation as an unsigned type as we might reasonably suppose. Instead use to_long() everywhere to preserve the bitwise representation and then use sign-bit filling to make sure the value is correctly re-encoded as mp_integer.

This adds some checks about the operands for mp_arith operations. These are used mainly in the interpreter and the chosen limit is the size of signed/unsigned long long int types.

Sparse vectors represent a 2^64 sized space while allocating only space that is used.

This will allow large address reservations for unbounded-sized objects, with actual cells allocated on demand. Original patch: From: Chris Smowton <chris@smowton.net> Date: Tue, 21 Mar 2017 15:24:03 +0000 Subject: [PATCH 1/3] Interpreter: switch to sparse vector memory map

They get allocated 2^32 address space each (of a 2^64 sized space) using the sparse-vector memory representation to keep the actual storage requirements sensible. Original patch: From: Chris Smowton <chris@smowton.net> Date: Tue, 21 Mar 2017 17:13:43 +0000 Subject: [PATCH 2/3] Add support for unbounded-size objects Corrected linting issues Using empty, and comments on get_size

Fixes a build issue with testgen

This is only used in derivative out-of-repo classes, and therefore should be moved there.

Make "Infinite size arrays not supported" and "Failed to concretize variable array" warnings rather than errors.

This could previously overestimate object sizes, potentially by including all other objects in the address space in the size estimate. That could lead to overly long variable-length arrays, with performance cost though most likely no correctness problems in Java, since all arrays have an explicit length.

Use from_integer, everywhere.

smowton · 2017-10-04T16:19:19Z

Dismissed stale review request

tautschnig · 2018-02-23T07:24:58Z

I believe we are not going ahead with a selective develop->master transition, thus closing.

tautschnig requested review from smowton, mgudemann, cristina-david, romainbrenguier, allredj and owen-mc-diffblue August 22, 2017 15:52

allredj approved these changes Aug 22, 2017

View reviewed changes

peterschrammel reviewed Aug 22, 2017

View reviewed changes

tautschnig self-assigned this Aug 23, 2017

tautschnig changed the title ~~[develop->master] Interpreter fixes~~ [depends: #1281, develop->master] Interpreter fixes Aug 23, 2017

mgudemann approved these changes Aug 23, 2017

View reviewed changes

tautschnig force-pushed the interpreter branch from ef9d2d1 to 6862fc3 Compare August 23, 2017 15:10

tautschnig changed the title ~~[depends: #1281, develop->master] Interpreter fixes~~ [depends: #1281, #1290, develop->master] Interpreter fixes Aug 23, 2017

tautschnig changed the title ~~[depends: #1281, #1290, develop->master] Interpreter fixes~~ [depends: #1281, #1289, #1290, develop->master] Interpreter fixes Aug 23, 2017

tautschnig changed the title ~~[depends: #1281, #1289, #1290, develop->master] Interpreter fixes~~ [depends: #1289, #1290, develop->master] Interpreter fixes Sep 1, 2017

tautschnig changed the title ~~[depends: #1289, #1290, develop->master] Interpreter fixes~~ [depends: #1289, develop->master] Interpreter fixes Sep 1, 2017

tautschnig added the develop->master label Sep 2, 2017

tautschnig changed the title ~~[depends: #1289, develop->master] Interpreter fixes~~ [depends: #1289] Interpreter fixes Sep 2, 2017

tautschnig changed the title ~~[depends: #1289] Interpreter fixes~~ [depends: #1289,#1330] Interpreter fixes Sep 2, 2017

tautschnig force-pushed the interpreter branch from 2bd6781 to 4a11fbd Compare September 3, 2017 13:27

tautschnig changed the title ~~[depends: #1289,#1330] Interpreter fixes~~ [depends: #1330] Interpreter fixes Sep 3, 2017

tautschnig changed the title ~~[depends: #1330] Interpreter fixes~~ [depends: #1330,#1338] Interpreter fixes Sep 3, 2017

tautschnig changed the title ~~[depends: #1330,#1338] Interpreter fixes~~ [depends: #1330] Interpreter fixes Sep 4, 2017

dcattaruzza added 2 commits September 4, 2017 07:53

Get symbol of member expression

e3e7bb8

Auxiliary function to check if the ssa has enough data to build an id…

3c8bcb9

…entifier

dcattaruzza and others added 17 commits September 4, 2017 07:53

Bitwise operators for mpinteger

1c9ace0

Auxiliary function to retrieve tail of trace and added dead command t…

74ade14

…o trace

Add size/value checks to bitwise mp_arith operations

4cc9e72

This adds some checks about the operands for mp_arith operations. These are used mainly in the interpreter and the chosen limit is the size of signed/unsigned long long int types.

update interpreter

5d8884f

New class for sparse vectors in util

a2628d7

Sparse vectors represent a 2^64 sized space while allocating only space that is used.

Add includes to sparse_vector.h

46a87bb

Fixes a build issue with testgen

Remove trace_stackt

e63a8c6

This is only used in derivative out-of-repo classes, and therefore should be moved there.

Handle typecast when evaluating addresses in the interpreter

8e9937e

Change two errors to warnings

346ef12

Make "Infinite size arrays not supported" and "Failed to concretize variable array" warnings rather than errors.

Remove constant_exprt::integer_constant

fcf6ffa

Use from_integer, everywhere.

Interpreter: replace assert by invariants

a0b4094

Replace 3-valued char by enum

61639a1

Interpreter: constify mp_integer typed address parameters

fdbb38e

tautschnig force-pushed the interpreter branch from 4a11fbd to fdbb38e Compare September 4, 2017 06:53

smowton removed their request for review October 4, 2017 16:19

tautschnig closed this Feb 23, 2018

tautschnig deleted the interpreter branch February 23, 2018 07:25

[depends: #1330] Interpreter fixes #1274

[depends: #1330] Interpreter fixes #1274

Uh oh!

Conversation

tautschnig commented Aug 22, 2017

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Aug 22, 2017

Uh oh!

tautschnig commented Aug 22, 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!

mgudemann 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!

smowton commented Aug 23, 2017

Uh oh!

tautschnig commented Aug 23, 2017

Uh oh!

smowton commented Oct 4, 2017

Uh oh!

tautschnig commented Feb 23, 2018

Uh oh!

Uh oh!