[QUESTION] How to be sure to retrieve the correct boolean for a variable (ex.: int) ?

[PeterMacGonagan]

Hello,

I use CBMC to generate CNF from little math problems (--dimacs).
I use external solver to find the solutions. CBMC is able to compute the correct solution (with minisat). I use --trace-compact to see the solutions.

I would like to get the equivalent boolean of my variables. --compact-trace is able to do it.

I can observe that at the end of dimacs file there are some lines of this kind:

c main::1::b2!0@1#2 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197

which derives from:
int b2;

We can observe 32 booleans (=4 bytes).

c main::1::b2!0@1#2
166 167 168 169 170 171 172 173
174 175 176 177 178 179 180 181
182 183 184 185 186 187 188 189
190 191 192 193 194 195 196 197

Could you confirm me that there are expressed from LSB (166) to MSB (197) (Left to Right)?
Could you tell me how to be sure to retrieve the correct boolean for my variables? Note: I just have 16 integers to retrieve. I'll write a little parser.

In fact, I'm a little confused about the fact that b2 has two "equivalences":

[line 10010] c main::1::b2!0@1#2 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197

[line 10186] c main::1::b2!0@1#1 3058 3059 3060 3061 3062 3063 3064 3065 3066 3067 3068 3069 3070 3071 3072 3073 3074 3075 3076 3077 3078 3079 3080 3081 3082 3083 3084 3085 3086 3087 3088 3089

Does it means that: 166=3058, 167=3059, etc. ?

What' is the meaning of: c main::1::b2!0@1#2
It's was in c langage
function main
Thread 1???
Variable b2
!0@1#2 or !0@1#1

Thank you in advance.

[tautschnig]

CBMC uses static single assignment form (SSA) to produce an equation system. You can read more about why and what is happening here in our documentation at http://cprover.diffblue.com/background-concepts.html#SSA_section. So your parser will need to be aware of this in order to identify the correct instantiation of the program variable.

You are right that, at present, the MSB will have the higher variable index than the LSB. I don't think we've ever changed this, but also it is possible that this would change without notice.

[PeterMacGonagan]

Thank you for the link to the documentation but I'm not sure I really understood...

While control flow graphs are already quite useful for static analysis, some techniques benefit from a further transformation to a representation known as static single assignment, short SSA. The point of this step is to ensure that we can talk about the entire history of assignments to a given variable. This is **achieved by **renaming variables again: whenever we assign to a variable, we clone this variable by giving it a new name. This ensures that each variable appearing in the resulting program is written to exactly once (but it may be read arbitrarily many times). In this way, we can refer to earlier values of the variable by just referencing the name of an older incarnation of the variable.

What's the difference between main::1::b2!0@1#1 main::1::b2!0@1#2?
It's equivalent to b2.1 and b2.2 ?
It's the history of assignments to b2?

I've declared b2 like this:
uint32_t b2 = nondet_int();

I don't specify b2 in my code. So, I don't understand why there are two assignments to b2?

[tautschnig]

You are right in that it is the history of assignments to a variable. In your specific case you are seeing that we treat the declaration and the initial value as two separate values. So "#1" is the unassigned/unconstrained value, "#2" is the result of the assignment.

[tautschnig]

@PeterMacGonagan Would you have further requests on this case or is it ok for us to close this issue?

[tautschnig]

Closing, please do not hesitate to re-open if further questions arise.

[PeterMacGonagan]

You are right in that it is the history of assignments to a variable. In your specific case you are seeing that we treat the declaration and the initial value as two separate values. So "#1" is the unassigned/unconstrained value, "#2" is the result of the assignment.

Thank you for your answer. I was on another projects.

What's the meaning of !0@1, please? Is it thread?

[tautschnig]

[...]

What's the meaning of !0@1, please? Is it thread?

With apologies for this being buried among other documentation: http://cprover.diffblue.com/group__goto-symex.html#static-single-assignment briefly explains these levels; yes, this is the thread and the function, respectively.