Remove Assert query by ivanazuzic · Pull Request #251 · goblint/analyzer

ivanazuzic · 2021-06-15T15:54:43Z

Closes #238.

Asked queries are tracked to prevent cycles, which return top result.
Queries now has BigInt in the integer result domain.
IntDomain.Integers are now a functor which takes IntOps. This way we can choose if we want them with int64 or BigInt.

src/analyses/apron/poly.apron.ml

src/analyses/arinc.ml

src/analyses/flagModes.ml

src/analyses/mCP.ml

sim642

This PR now contains both the generalization of Queries.ID from int64 to big ints and the query cycle check, which isn't actually used.

There are three options:

Also do assert query removal and extend this PR to merge it all together.
Remove the MCP2.query change for now and merge the domain change on its own.
Keep it as is. I suppose the query cycle detection is also working but not used yet, so I think this would also be fine.

src/cdomains/intDomain.ml

src/domains/queries.ml

src/transform/expressionEvaluation.ml

ivanazuzic · 2021-06-16T00:42:58Z

This PR now contains both the generalization of Queries.ID from int64 to big ints and the query cycle check, which isn't actually used.

There are three options:

Also do assert query removal and extend this PR to merge it all together.

Remove the MCP2.query change for now and merge the domain change on its own.

Keep it as is. I suppose the query cycle detection is also working but not used yet, so I think this would also be fine.

I vote for option 1.

src/domains/queries.ml

…cle detection" This reverts commit e03b253.

sim642 · 2021-07-07T10:41:19Z

I think I managed to finally switch Queries.ID to IntDomTuple and make base's eval_rv go through EvalInt for integer expressions without having to exponentially fall back to the normal case. It solves the issue of deep expressions.

The result of all this refactoring of eval_rv is that it no longer even requires the query cycle check. For best possible performance, when base answers EvalInt, it directly jumps to eval_rv_no_ask_evalint to avoid asking for the exact same query, that due to cycle would return a useless top anyway. Still, we can leave the query cycle mechanism in.

I think we can do a new comparison benchmark to see if this hopefully behaves the same as the old master.

michael-schwarz · 2021-07-08T11:33:12Z

I think we can do a new comparison benchmark to see if this hopefully behaves the same as the old master.

I'll start one 😄

michael-schwarz · 2021-07-08T16:40:52Z

I guess this looks a lot more reasonable now 😄

rm_assert_query_3.zip

sim642 · 2021-07-08T17:38:30Z

Indeed, although I might try to look into the 15 benchmarks that go from true to unknown. Seems a bit surprising that it's less precise.

Could also be that we were unsound before. Maybe due to sub-asks in patched_ask still being based off the old local state or something that I might have fixed.

sim642 · 2021-07-09T09:08:24Z

I just tried one locally and it still outputted true, so I was confused about the unknown result in the table.
But apparently the output can sometimes get mixed up like this:

../sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-32_7a-drivers--net--arcnet--arcnet.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.iSV-COMP result: true
:6576: Bug: typeOffset: Field on a non-compound

The benchexec tool-info module for Goblint doesn't account for this possibility. I'm not sure it should either because there's no reason SV-COMP result: true couldn't be split up by arbitrary garbage output as well.

In this case it seems like we now get tons of these typeOffset errors while previously we didn't, so there might be something to still fix here.

sim642 · 2021-07-09T09:14:20Z

Actually, maybe not. They just appear because I do an extra typeOf call to determine whether EvalInt should be queried: https://github.com/goblint/analyzer/pull/251/files#diff-969b2ca0b7175f19daa5deae1308a02718e8cd1927a4d8e160541a35e57c31dbR565-R577.

sim642 · 2021-07-09T10:00:12Z

Honestly, I don't know how to fix this other than fixing the complete trash error handling strategy in CIL. It prints error text directly and raises an argumentless Errormsg.Error. So it's impossible not to have the output because catching the exception doesn't undo printing. The sane thing would be to not print errors directly but return the text as an argument to the exception (you know, like Failure does). But I think that's well beyond the scope of this PR.

I guess I could call our copy-pasted Cilfacade.typeOf instead, which doesn't print garbage:

analyzer/src/util/cilfacade.ml

Lines 249 to 317 in e9e71ae

    
           let rec typeOf (e: exp) : typ = 
        
             match e with 
        
             | Const(CInt64 (_, ik, _)) -> TInt(ik, []) 
        
             (* Character constants have type int.  ISO/IEC 9899:1999 (E), 
        
              * section 6.4.4.4 [Character constants], paragraph 10, if you 
        
              * don't believe me. *) 
        
             | Const(CChr _) -> intType 
        
             (* The type of a string is a pointer to characters ! The only case when 
        
              * you would want it to be an array is as an argument to sizeof, but we 
        
              * have SizeOfStr for that *) 
        
             | Const(CStr s) -> charPtrType 
        
             | Const(CWStr s) -> TPtr(!wcharType,[]) 
        
             | Const(CReal (_, fk, _)) -> TFloat(fk, []) 
        
             | Const(CEnum(tag, _, ei)) -> typeOf tag 
        
             | Lval(lv) -> typeOfLval lv 
        
             | SizeOf _ | SizeOfE _ | SizeOfStr _ -> !typeOfSizeOf 
        
             | AlignOf _ | AlignOfE _ -> !typeOfSizeOf 
        
             | UnOp (_, _, t) -> t 
        
             | BinOp (_, _, _, t) -> t 
        
             | CastE (t, _) -> t 
        
             | AddrOf (lv) -> TPtr(typeOfLval lv, []) 
        
             | StartOf (lv) -> begin 
        
                 match unrollType (typeOfLval lv) with 
        
                   TArray (t,_, a) -> TPtr(t, a) 
        
                 | _ -> raise Not_found 
        
               end 
        
             | Question _ -> failwith "Logical operations should be compiled away by CIL." 
        
             | _ -> failwith "Unmatched pattern." 
        
           and typeOfInit (i: init) : typ = 
        
             match i with 
        
               SingleInit e -> typeOf e 
        
             | CompoundInit (t, _) -> t 
        
           and typeOfLval = function 
        
               Var vi, off -> typeOffset vi.vtype off 
        
             | Mem addr, off -> begin 
        
                 match unrollType (typeOf addr) with 
        
                   TPtr (t, _) -> typeOffset t off 
        
                 | _ -> raise Not_found 
        
               end 
        
           and typeOffset basetyp = 
        
             let blendAttributes baseAttrs = 
        
               let (_, _, contageous) = 
        
                 partitionAttributes ~default:(AttrName false) baseAttrs in 
        
               typeAddAttributes contageous 
        
             in 
        
             function 
        
               NoOffset -> basetyp 
        
             | Index (_, o) -> begin 
        
                 match unrollType basetyp with 
        
                   TArray (t, _, baseAttrs) -> 
        
                   let elementType = typeOffset t o in 
        
                   blendAttributes baseAttrs elementType 
        
                 | t -> raise Not_found 
        
               end 
        
             | Field (fi, o) -> 
        
               match unrollType basetyp with 
        
                 TComp (_, baseAttrs) -> 
        
                 let fieldType = typeOffset fi.ftype o in 
        
                 blendAttributes baseAttrs fieldType 
        
               | _ -> raise Not_found

But every use of typeOf in Goblint uses Cil.typeOf directly (except a single one in osek) and this problem would in no way be limited to the typeOf call I added here (base has 69 others, which all could just as easily cause this problem) as any other CIL functions may do the same crap error handling.

michael-schwarz · 2021-07-09T11:21:44Z

I guess I could call our copy-pasted Cilfacade.typeOf instead

That funnily enough slightly differs from Cil.typeOf e.g. in that it doesn't handle Real and Imagand handles Question different.

Also, the entire typeOf logic in CIL seems to be in need of a rewrite, e.g. it uses two slightly different mechanisms of reporting errors E.s (bug "typeOfLval: Mem on a non-pointer (%a)" !pd_exp addr) vs E.s (E.bug "typeOffset: Index on a non-array")
https://github.com/goblint/cil/blob/d61cfa6a403f4d278c86344091bc07dccd8b549b/src/cil.ml#L1963

Maybe we can work some super dirty workaround that temporarily sets Errormsg.logChannel to something different (assuming we patch the uses of bug to be uses of E.bug)?

sim642 · 2021-07-09T11:41:10Z

That funnily enough slightly differs from Cil.typeOf e.g. in that it doesn't handle Real and Imagand handles Question different.

I noticed that too when I copied the CIL implementation over Cilfacade's to see if it's out of date.

Maybe we can work some super dirty workaround that temporarily sets Errormsg.logChannel to something different (assuming we patch the uses of bug to be uses of E.bug)?

I tried to do that, but it didn't work: there was still output. Now I know why: Cil.bug doesn't use logChannel. I didn't even notice this difference, I just thought Errormsg was opened there...
Also, there's no null out_channel AFAIK, so one would have to open_out "/dev/null", which is just so bad...

Given that we already have Cilfacade.typeOf, I think I'll update it and change all errors to a custom descriptive exception types (instead of Not_found) and make all Cil.typeOf calls go to Cilfacade.typeOf instead. I'll do this in a separate PR because this one is already overwhelming enough and otherwise seems to now behave as needed.

src/analyses/base.ml

sim642 · 2021-07-12T07:57:32Z

It seems like this might finally be in merge-able condition although there is one more subtlety about this change regarding the extra eval_rv wrapper which turns Bot and ArithmeticOnIntegerBot into top values.
Previously this was applied also to EvalInt responses.
Now it's not applied to those, only direct eval_rv calls in base itself. I could change the new EvalInt to also do that, but then it would also do that conversion at every subexpression level, whereas previously it was only done at the outermost level, which would change some intermediate values from Bot to top.

I don't completely understand this weird conversion mechanism (seems non-monotonic), so I don't really know what the expected behavior should be.

sim642 · 2021-07-12T12:18:29Z

In the process of making #278 work, I answered my own question: the query response also needs to change bottoms into tops to supply sound values to other analyses. That then happens at every subexpression, not just the outermost, and nothing seemed to break because of this, so hopefully it's good.

michael-schwarz · 2021-07-14T07:33:13Z

src/cdomains/intDomain.ml

-  let shift_right n1 n2 = Int64.shift_right n1 (Int64.to_int n2)
+  let bitnot = Ints_t.lognot
+  let bitand = Ints_t.logand
+  let bitor  = Ints_t.logor


Is this correct ?!

For int64:

val logor : int64 -> int64 -> int64 (* Bitwise logical or. *)

But for Ints_t we have bitnot etc.

Ivana Zuzic added 5 commits June 9, 2021 13:12

Track asked queries

a8b0acf

Remove unnecessary match branches

dbb20ec

Add the query to asked set outside of ask lambda

e5398e8

Make Integers a functor and use BigInts for queries

393ce5c

Implement arbitrary for IntDomain.Integers

8b499ff

ivanazuzic added cleanup Refactoring, clean-up precision labels Jun 15, 2021

sim642 self-requested a review June 15, 2021 16:10

michael-schwarz self-requested a review June 15, 2021 16:13