Merge pull request #745 from goblint/yaml-witness-validate

Add YAML witness validation by invariant checking
goblint · May 31, 2022 · d21a2f3 · d21a2f3
2 parents ea01109 + 8b2cccf
commit d21a2f3
Show file tree

Hide file tree

Showing 21 changed files with 487 additions and 135 deletions.
diff --git a/goblint.opam b/goblint.opam
@@ -68,7 +68,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#56f5f9ad58e71908ff66e179e056a22ea71693a2" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#0a37478e08b9ae10587b0355ad2805dfeca1cca9" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # quoter workaround reverted for release, so no pin needed

diff --git a/goblint.opam.locked b/goblint.opam.locked
@@ -124,7 +124,7 @@ version: "dev"
 pin-depends: [
   [
     "goblint-cil.1.8.2"
-    "git+https://github.com/goblint/cil.git#56f5f9ad58e71908ff66e179e056a22ea71693a2"
+    "git+https://github.com/goblint/cil.git#0a37478e08b9ae10587b0355ad2805dfeca1cca9"
   ]
   [
     "apron.v0.9.13"

diff --git a/goblint.opam.template b/goblint.opam.template
@@ -1,7 +1,7 @@
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#56f5f9ad58e71908ff66e179e056a22ea71693a2" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#0a37478e08b9ae10587b0355ad2805dfeca1cca9" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # quoter workaround reverted for release, so no pin needed

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -697,6 +697,7 @@ struct
         let x = Pretty.sprint ~width:80 (d_const () c) in (* escapes, see impl. of d_const in cil.ml *)
         let x = String.sub x 2 (String.length x - 3) in (* remove surrounding quotes: L"foo" -> foo *)
         `Address (AD.from_string x) (* `Address (AD.str_ptr ()) *)
+      | Const _ -> VD.top ()
       (* Variables and address expressions *)
       | Lval (Var v, ofs) -> do_offs (get a gs st (eval_lv a gs st (Var v, ofs)) (Some exp)) ofs
       (*| Lval (Mem e, ofs) -> do_offs (get a gs st (eval_lv a gs st (Mem e, ofs))) ofs*)
@@ -794,7 +795,16 @@ struct
       | CastE  (t, exp) ->
         let v = eval_rv a gs st exp in
         VD.cast ~torg:(Cilfacade.typeOf exp) t v
-      | _ -> VD.top ()
+      | SizeOf _
+      | Real _
+      | Imag _
+      | SizeOfE _
+      | SizeOfStr _
+      | AlignOf _
+      | AlignOfE _
+      | Question _
+      | AddrOfLabel _ ->
+        VD.top ()
     in
     if M.tracing then M.traceu "evalint" "base eval_rv_base %a -> %a\n" d_exp exp VD.pretty r;
     r

diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml
@@ -65,7 +65,12 @@ struct
       | _ -> ()
     in
     match e with
-    | Lval (Var v, offs) -> ()
+    | Const _
+    | SizeOf _
+    | SizeOfStr _
+    | AlignOf _
+    | AddrOfLabel _
+    | Lval (Var _, _) -> ()
     | AddrOf (Var _, _)
     | StartOf (Var _, _) ->  warn_lval_mem e NoOffset
     | AddrOf (Mem e, offs)
@@ -77,9 +82,16 @@ struct
       warn_deref_exp a st e1;
       warn_deref_exp a st e2
     | UnOp (_,e,_)
+    | Real e
+    | Imag e
+    | SizeOfE e
+    | AlignOfE e
     | CastE  (_,e) ->
       warn_deref_exp a st e
-    | _ -> ()
+    | Question (b, t, f, _) ->
+      warn_deref_exp a st b;
+      warn_deref_exp a st t;
+      warn_deref_exp a st f
 
   let may (f: 'a -> 'b) (x: 'a option) : unit =
     match x with

diff --git a/src/analyses/tutorials/taint.ml b/src/analyses/tutorials/taint.ml
@@ -42,7 +42,7 @@ struct
     | CastE (_,e)
     | UnOp (_,e,_) -> is_exp_tainted state e
     | SizeOf _ | SizeOfStr _ | Const _  | AlignOf _ | AddrOfLabel _ -> false
-    | Question _ -> failwith "should be optimized away by CIL"
+    | Question (b, t, f, _) -> is_exp_tainted state b || is_exp_tainted state t || is_exp_tainted state f
   and is_lval_tainted state = function
     | (Var v, _) ->
       (* TODO: Check whether variable v is tainted *)

diff --git a/src/analyses/uninit.ml b/src/analyses/uninit.ml
@@ -49,23 +49,31 @@ struct
 
   let rec access_one_byval a rw (exp:exp) =
     match exp with
-    (* Integer literals *)
-    | Const _ -> []
+    | Const _
+    | SizeOf _
+    | SizeOfStr _
+    | AlignOf _
+    | AddrOfLabel _ -> []
     (* Variables and address expressions *)
     | Lval lval -> access_address a rw lval @ (access_lv_byval a lval)
     (* Binary operators *)
     | BinOp (op,arg1,arg2,typ) ->
       let a1 = access_one_byval a rw arg1 in
       let a2 = access_one_byval a rw arg2 in
       a1 @ a2
-    (* Unary operators *)
-    | UnOp (op,arg1,typ) -> access_one_byval a rw arg1
+    | UnOp (_,e,_)
+    | Real e
+    | Imag e
+    | SizeOfE e
+    | AlignOfE e ->
+      access_one_byval a rw e
     (* The address operators, we just check the accesses under them *)
     | AddrOf lval -> access_lv_byval a lval
     | StartOf lval -> access_lv_byval a lval
     (* Most casts are currently just ignored, that's probably not a good idea! *)
     | CastE  (t, exp) -> access_one_byval a rw exp
-    | _ -> []
+    | Question (b, t, f, _) ->
+      access_one_byval a rw b @ access_one_byval a rw t @ access_one_byval a rw f
   (* Accesses during the evaluation of an lval, not the lval itself! *)
   and access_lv_byval a (lval:lval) =
     let rec access_offset (ofs: offset) =

diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
@@ -118,7 +118,11 @@ struct
     | AlignOf _
     | AlignOfE _
     | UnOp  _
-    | BinOp _ -> false
+    | BinOp _
+    | Question _
+    | Real _
+    | Imag _
+    | AddrOfLabel _ -> false
     | Const _ -> true
     | AddrOf  (Var v2,_)
     | StartOf (Var v2,_)
@@ -127,8 +131,6 @@ struct
     | StartOf (Mem e,_)
     | Lval    (Mem e,_)
     | CastE (_,e)           -> interesting e
-    | Question _ -> failwith "Logical operations should be compiled away by CIL."
-    | _ -> failwith "Unmatched pattern."
 
   (* helper to decide equality *)
   let query_exp_equal ask e1 e2 g s =
@@ -157,8 +159,11 @@ struct
       | SizeOfE _
       | SizeOfStr _
       | AlignOf _
-      | AlignOfE _ -> false
-      | UnOp (_,e,_) -> type_may_change_t e bt
+      | AlignOfE _
+      | AddrOfLabel _ -> false (* TODO: some may contain exps? *)
+      | UnOp (_,e,_)
+      | Real e
+      | Imag e -> type_may_change_t e bt
       | BinOp (_,e1,e2,_) -> type_may_change_t e1 bt || type_may_change_t e2 bt
       | Lval (Var _,o)
       | AddrOf (Var _,o)
@@ -167,8 +172,7 @@ struct
       | AddrOf (Mem e,o)
       | StartOf (Mem e,o) -> may_change_t_offset o || type_may_change_t e bt
       | CastE (t,e) -> type_may_change_t e bt
-      | Question _ -> failwith "Logical operations should be compiled away by CIL."
-      | _ -> failwith "Unmatched pattern."
+      | Question (b, t, f, _) -> type_may_change_t b bt || type_may_change_t t bt || type_may_change_t f bt
     in
     let bt =  unrollTypeDeep (Cilfacade.typeOf b) in
     type_may_change_t a bt
@@ -191,8 +195,11 @@ struct
       | SizeOfE _
       | SizeOfStr _
       | AlignOf _
-      | AlignOfE _ -> false
-      | UnOp (_,e,_) -> lval_may_change_pt e bl
+      | AlignOfE _
+      | AddrOfLabel _ -> false (* TODO: some may contain exps? *)
+      | UnOp (_,e,_)
+      | Real e
+      | Imag e -> lval_may_change_pt e bl
       | BinOp (_,e1,e2,_) -> lval_may_change_pt e1 bl || lval_may_change_pt e2 bl
       | Lval (Var _,o)
       | AddrOf (Var _,o)
@@ -201,8 +208,7 @@ struct
       | AddrOf (Mem e,o)
       | StartOf (Mem e,o) -> may_change_pt_offset o || lval_may_change_pt e bl
       | CastE (t,e) -> lval_may_change_pt e bl
-      | Question _ -> failwith "Logical operations should be compiled away by CIL."
-      | _ -> failwith "Unmatched pattern."
+      | Question (b, t, f, _) -> lval_may_change_pt t bl || lval_may_change_pt t bl || lval_may_change_pt f bl
     in
     let bls = pt b in
     if Queries.LS.is_top bls
@@ -258,8 +264,11 @@ struct
               | SizeOfE _
               | SizeOfStr _
               | AlignOf _
-              | AlignOfE _ -> false
-              | UnOp (_,e,_) -> type_may_change_t deref e
+              | AlignOfE _
+              | AddrOfLabel _ -> false (* TODO: some may contain exps? *)
+              | UnOp (_,e,_)
+              | Real e
+              | Imag e -> type_may_change_t deref e
               | BinOp (_,e1,e2,_) -> type_may_change_t deref e1 || type_may_change_t deref e2
               | Lval (Var _,o)
               | AddrOf (Var _,o)
@@ -268,8 +277,7 @@ struct
               | AddrOf (Mem e,o)  -> (*Messages.warn "Addr" ;*) may_change_t_offset o || type_may_change_t false e
               | StartOf (Mem e,o) -> (*Messages.warn "Start";*) may_change_t_offset o || type_may_change_t false e
               | CastE (t,e) -> type_may_change_t deref e
-              | Question _ -> failwith "Logical operations should be compiled away by CIL."
-              | _ -> failwith "Unmatched pattern."
+              | Question (b, t, f, _) -> type_may_change_t deref b || type_may_change_t deref t || type_may_change_t deref f
 
     and lval_may_change_pt a bl : bool =
       let rec may_change_pt_offset o =
@@ -324,8 +332,11 @@ struct
            | SizeOfE _
            | SizeOfStr _
            | AlignOf _
-           | AlignOfE _ -> false
-           | UnOp (_,e,_) -> lval_may_change_pt e bl
+           | AlignOfE _
+           | AddrOfLabel _ -> false (* TODO: some may contain exps? *)
+           | UnOp (_,e,_)
+           | Real e
+           | Imag e -> lval_may_change_pt e bl
            | BinOp (_,e1,e2,_) -> lval_may_change_pt e1 bl || lval_may_change_pt e2 bl
            | Lval (Var _,o)
            | AddrOf (Var _,o)
@@ -334,8 +345,7 @@ struct
            | AddrOf (Mem e,o)
            | StartOf (Mem e,o) -> may_change_pt_offset o || lval_may_change_pt e bl
            | CastE (t,e) -> lval_may_change_pt e bl
-           | Question _ -> failwith "Logical operations should be compiled away by CIL."
-           | _ -> failwith "Unmatched pattern."
+           | Question (b, t, f, _) -> lval_may_change_pt b bl || lval_may_change_pt t bl || lval_may_change_pt f bl
     in
     let r =
       if Queries.LS.is_top bls || Queries.LS.mem (dummyFunDec.svar, `NoOffset) bls
@@ -373,7 +383,11 @@ struct
     | AlignOf _
     | AlignOfE _
     | UnOp _
-    | BinOp _ -> None
+    | BinOp _
+    | Question _
+    | AddrOfLabel _
+    | Real _
+    | Imag _ -> None
     | Const _ -> Some false
     | Lval (Var v,_) ->
       Some (v.vglob || (ask.f (Queries.IsMultiple v)))
@@ -388,8 +402,6 @@ struct
     | AddrOf lv -> Some false (* TODO: sound?! *)
     | StartOf (Var v,_) ->  Some (ask.f (Queries.IsMultiple v)) (* Taking an address of a global is fine*)
     | StartOf lv -> Some false (* TODO: sound?! *)
-    | Question _ -> failwith "Logical operations should be compiled away by CIL."
-    | _ -> failwith "Unmatched pattern."
 
   (* Set given lval equal to the result of given expression. On doubt do nothing. *)
   let add_eq ask (lv:lval) (rv:Exp.t) st =
@@ -551,6 +563,10 @@ struct
     | AlignOfE _
     | UnOp _
     | BinOp _
+    | Question _
+    | AddrOfLabel _
+    | Real _
+    | Imag _
     | AddrOf  (Var _,_)
     | StartOf (Var _,_)
     | Lval    (Var _,_) -> eq_set e s
@@ -562,8 +578,6 @@ struct
       Queries.ES.map (fun e -> Lval (mkMem ~addr:e ~off:ofs)) (eq_set_clos e s)
     | CastE (t,e) ->
       Queries.ES.map (fun e -> CastE (t,e)) (eq_set_clos e s)
-    | Question _ -> failwith "Logical operations should be compiled away by CIL."
-    | _ -> failwith "Unmatched pattern."
 
 
   let query ctx (type a) (x: a Queries.t): a Queries.result =

diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
@@ -335,7 +335,7 @@ struct
 
 
   let cil_exp_of_lincons1 fundec (lincons1:Lincons1.t) =
-    let zero = Cil.zero in
+    let zero = Cil.kinteger ILongLong 0 in
     try
       let linexpr1 = Lincons1.get_linexpr1 lincons1 in
       let cilexp = cil_exp_of_linexpr1 fundec linexpr1 in

diff --git a/src/cdomains/basetype.ml b/src/cdomains/basetype.ml
@@ -96,10 +96,20 @@ struct
     match e with
     | Lval l -> occurs_lv l
     | AddrOf l -> occurs_lv l
-    | UnOp (_,e,_) -> occurs x e
+    | StartOf l -> occurs_lv l
+    | UnOp (_,e,_)
+    | Real e
+    | Imag e
+    | SizeOfE e
+    | AlignOfE e -> occurs x e
     | BinOp (_,e1,e2,_) -> occurs x e1 || occurs x e2
     | CastE (_,e) -> occurs x e
-    | _ -> false
+    | Question (b, t, f, _) -> occurs x b || occurs x t || occurs x f
+    | Const _
+    | SizeOf _
+    | SizeOfStr _
+    | AlignOf _
+    | AddrOfLabel _ -> false
 
   let replace (x:varinfo) (exp: exp) (e:exp): exp =
     let rec replace_lv (v,offs): lval =
@@ -115,11 +125,21 @@ struct
       match e with
       | Lval (Var y, NoOffset) when Variables.equal x y -> exp
       | Lval l -> Lval (replace_lv l)
-      | AddrOf l -> Lval (replace_lv l)
+      | AddrOf l -> Lval (replace_lv l) (* TODO: should be AddrOf? *)
+      | StartOf l -> StartOf (replace_lv l)
       | UnOp (op,e,t) -> UnOp (op, replace_rv e, t)
       | BinOp (op,e1,e2,t) -> BinOp (op, replace_rv e1, replace_rv e2, t)
       | CastE (t,e) -> CastE(t, replace_rv e)
-      | x -> x
+      | Real e -> Real (replace_rv e)
+      | Imag e -> Imag (replace_rv e)
+      | SizeOfE e -> SizeOfE (replace_rv e)
+      | AlignOfE e -> AlignOfE (replace_rv e)
+      | Question (b, t, f, typ) -> Question (replace_rv b, replace_rv t, replace_rv f, typ)
+      | Const _
+      | SizeOf _
+      | SizeOfStr _
+      | AlignOf _
+      | AddrOfLabel _ -> e
     in
     constFold true (replace_rv e)
 
@@ -134,7 +154,7 @@ struct
     | AlignOf _
     | Question _
     | AddrOf _
-    | StartOf _ -> []
+    | StartOf _ -> [] (* TODO: return not empty, some may contain vars! *)
     | UnOp (_, e, _ )
     | CastE (_, e)
     | Real e