Towards fixing GobView search: Avoid truncation of very large integers

[stilscher]

When working on goblint/gobview#7 (comment) I tried the following semantic query on the regression test case tests/regression/00-sanity/01-assert.c:
{"kind":["var"],"target":["name","fail"],"find":["uses"],"expression":"fail == 0","mode":["Must"]}

It results in a fixpoint not found. The reason for this is that integers larger than 2³², namely the start id for varinfos created by Goblint and the ids of pseudo return nodes are truncated (OCaml int is converted to a 32bit int in JavaScript with js_of_ocaml) and therefore differ from what was previously stored in the solver data. My proposed easy fix (at least for not too large projects) would be to decrease the start id by a factor of 10.

Todo

• allow for syntactic queries (which are missing the expression field) to be handed to GobView as query
• add test case for the search interface in GobView (requires goblint/gobview@d577fbd)
• update CIL-pin to include Fix syntactic search cil#147 (comment)
• update GobView submodule to include Add alert for unsupported queries gobview#25

[sim642]

Maybe we could just use negative IDs for what we generate in Goblint? Start counting down from -1. That way they don't conflict with anything CIL generates, regardless of imaginable program size and are also small.

Or is there some reason the IDs shouldn't be negative? Maybe @michael-schwarz knows?

[michael-schwarz]

Or is there some reason the IDs shouldn't be negative? Maybe @michael-schwarz knows?

Off the top of my head, I cannot think of any reason against it.

Tbh, I am bit surprised we end up with 32-bit integers on the javascript side, normally this should be 54 bit integers...

[stilscher]

Here it states that OCaml ints are converted to JavaScript 32-bit integers. Also, the truncation occurs for integers >= 2147483648 (2^31). This is observable because an error is thrown when transpiling:
Warning: integer overflow: integer 0x80000000 (2147483648) truncated to 0x80000000 (-2147483648); the generated code might be incorrect.
Where did you find the information that it should be 54 bit integers?

[michael-schwarz]

Very strange. Might have to make some experiments after the holidays...

I still like simmo's idea to go for negative numbers in these cases.

The thing is that JavaScript doesn't really have integers: on that vpage it says they're mapped to number (as is float), which is 64bit IEEE 754 floating points, which would give you 54 bit integers. But maybe they do some bitwise crap with every instruction to make sure it is actually 32 bit operations?.

[sim642]

Just a thought for future: at some point this old expression evaluation should be switched from the odd Format-CIL parser (see goblint-cil issues) to the normal expression parser that's used for witness invariants. That avoids fixing the same issues twice.

At that point one might reconsider this being a transformation altogether, because it isn't. Simply using EvalInt or EvalValue queries directly from GobView should be possible.

[michael-schwarz]

What is the status here?

[sim642]

Looks like this should be good to go now.