diff --git a/goblint.opam b/goblint.opam index 26d33c1475..986258fbf4 100644 --- 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 index 9946ac7b25..b68b488a0d 100644 --- 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 index 5813c9f0ae..c354675c4f 100644 --- 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 index 02f6a4eb7a..ab77905da2 100644 --- 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 index d2476f97c4..c2e340aae6 100644 --- 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 index 83721d802b..d5c7360fa0 100644 --- 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 index 1fe25355c6..16fb3f0585 100644 --- a/src/analyses/uninit.ml +++ b/src/analyses/uninit.ml @@ -49,8 +49,11 @@ 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 *) @@ -58,14 +61,19 @@ struct 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 index bc226248a2..6bda0f0da3 100644 --- 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 index 05d1a05ba7..55b1b8802a 100644 --- 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 index 45a2dac307..d2c5f2b3be 100644 --- 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 diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml index 051f4a743d..cc4eff434a 100644 --- a/src/cdomains/intDomain.ml +++ b/src/cdomains/intDomain.ml @@ -830,7 +830,7 @@ struct let invariant c x = failwith "unimplemented" let invariant_ikind c ik x = - let c = Cil.(Lval (BatOption.get c.Invariant.lval)) in + let c = Cil.(mkCast ~e:(Lval (BatOption.get c.Invariant.lval)) ~newt:(TInt (ik, []))) in match x with | Some (x1, x2) when Ints_t.compare x1 x2 = 0 -> let x1 = Ints_t.to_bigint x1 in @@ -1599,7 +1599,7 @@ struct let lognot ik = eq ik (of_int ik BigInt.zero) let invariant_ikind c ik (x:t) = - let c = Cil.(Lval (BatOption.get c.Invariant.lval)) in + let c = Cil.(mkCast ~e:(Lval (BatOption.get c.Invariant.lval)) ~newt:(TInt (ik, []))) in match x with | `Definite x -> Invariant.of_exp Cil.(BinOp (Eq, c, kintegerCilint ik x, intType)) | `Excluded (s, _) -> @@ -2005,7 +2005,7 @@ module Enums : S with type int_t = BigInt.t = struct let ne ik x y = lognot ik (eq ik x y) let invariant_ikind c ik x = - let c = Cil.(Lval (Option.get c.Invariant.lval)) in + let c = Cil.(mkCast ~e:(Lval (BatOption.get c.Invariant.lval)) ~newt:(TInt (ik, []))) in match x with | Inc ps -> List.fold_left (fun a x -> @@ -2448,7 +2448,7 @@ struct res let invariant_ikind ctxt ik x = - let l = Cil.(Lval (BatOption.get ctxt.Invariant.lval)) in + let l = Cil.(mkCast ~e:(Lval (BatOption.get ctxt.Invariant.lval)) ~newt:(TInt (ik, []))) in match x with | Some (c, m) when m =: Ints_t.zero -> let c = Ints_t.to_bigint c in @@ -2894,7 +2894,7 @@ module IntDomTupleImpl = struct match to_int x with | Some v -> (* If definite, output single equality instead of every subdomain repeating same equality *) - let c_exp = Cil.(Lval (Option.get c.Invariant.lval)) in + let c_exp = Cil.(mkCast ~e:(Lval (BatOption.get c.Invariant.lval)) ~newt:(TInt (ik, []))) in Invariant.of_exp Cil.(BinOp (Eq, c_exp, kintegerCilint ik v, intType)) | None -> let is = to_list (mapp { fp = fun (type a) (module I:S with type t = a) -> I.invariant_ikind c ik } x) diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml index f9ce44d91d..3cdf39a2c6 100644 --- a/src/cdomains/lockDomain.ml +++ b/src/cdomains/lockDomain.ml @@ -119,7 +119,11 @@ struct | Const _ | AlignOfE _ | UnOp _ - | BinOp _ -> S.empty () + | BinOp _ + | Question _ + | Real _ + | Imag _ + | AddrOfLabel _ -> S.empty () | AddrOf (Var _,_) | StartOf (Var _,_) | Lval (Var _,_) -> S.singleton e @@ -127,8 +131,7 @@ struct | StartOf (Mem e,ofs) -> S.map (fun e -> StartOf (Mem e,ofs)) (eq_set ask e) | Lval (Mem e,ofs) -> S.map (fun e -> Lval (Mem e,ofs)) (eq_set ask e) | CastE (_,e) -> eq_set ask e - | Question _ -> failwith "Logical operations should be compiled away by CIL." - | _ -> failwith "Unmatched pattern.") + ) let add (ask: Queries.ask) e st = let no_casts = S.map Expcompare.stripCastsDeepForPtrArith (eq_set ask e) in diff --git a/src/cdomains/symbLocksDomain.ml b/src/cdomains/symbLocksDomain.ml index 8126c5d729..08a3642037 100644 --- a/src/cdomains/symbLocksDomain.ml +++ b/src/cdomains/symbLocksDomain.ml @@ -18,8 +18,11 @@ struct | SizeOfStr _ | AlignOf _ | Const _ - | AlignOfE _ -> false - | UnOp (_,e,_) -> cv deref e + | AlignOfE _ + | AddrOfLabel _ -> false (* TODO: some may contain vars? *) + | UnOp (_,e,_) + | Real e + | Imag e -> cv deref e | BinOp (_,e1,e2,_) -> cv deref e1 || cv deref e2 | AddrOf (Mem e,o) | StartOf (Mem e,o) @@ -31,8 +34,7 @@ struct if deref then CilType.Varinfo.equal v v2 || offs_contains o else offs_contains o - | Question _ -> failwith "Logical operations should be compiled away by CIL." - | _ -> failwith "Unmatched pattern." + | Question (b, t, f, _) -> cv deref b || cv deref t || cv deref f in cv false e @@ -87,6 +89,10 @@ struct | UnOp _ | BinOp _ | Const _ + | Question _ + | Real _ + | Imag _ + | AddrOfLabel _ | Lval (Var _,_) | AddrOf (Var _,_) | StartOf (Var _,_) -> exp @@ -97,8 +103,6 @@ struct | StartOf (Mem e,o) when simple_eq e q -> StartOf (Var v, addOffset o (Lval.CilLval.to_ciloffs offs)) | StartOf (Mem e,o) -> StartOf (Mem (replace_base (v,offs) q e), o) | CastE (t,e) -> CastE (t, replace_base (v,offs) q e) - | Question _ -> failwith "Logical operations should be compiled away by CIL." - | _ -> failwith "Unmatched pattern." let rec conc i = @@ -206,14 +210,16 @@ struct | UnOp _ | BinOp _ | StartOf _ - | Const _ -> raise NotSimpleEnough + | Const _ + | Question _ + | Real _ + | Imag _ + | AddrOfLabel _ -> raise NotSimpleEnough | Lval (Var v, os) -> EVar v :: conv_o os | Lval (Mem e, os) -> helper e @ [EDeref] @ conv_o os | AddrOf (Var v, os) -> EVar v :: conv_o os @ [EAddr] | AddrOf (Mem e, os) -> helper e @ [EDeref] @ conv_o os @ [EAddr] | CastE (_,e) -> helper e - | Question _ -> failwith "Logical operations should be compiled away by CIL." - | _ -> failwith "Unmatched pattern." in try helper exp with NotSimpleEnough -> [] diff --git a/src/domains/access.ml b/src/domains/access.ml index 821ab55dfc..3c20fdcc1b 100644 --- a/src/domains/access.ml +++ b/src/domains/access.ml @@ -111,7 +111,11 @@ let rec get_type (fb: typ) : exp -> acc_typ = function `Struct (s1, o1) | _ -> `Type t end - | _ -> `Type fb + | Const _ + | Lval _ + | Real _ + | Imag _ -> + `Type fb (* TODO: is this right? *) let get_type fb e = (* printf "e = %a\n" d_plainexp e; *) @@ -260,8 +264,12 @@ and distribute_access_exp f kind r c = function distribute_access_exp f kind r c arg1; distribute_access_exp f kind r c arg2 - (* Unary operators *) - | UnOp (op,arg1,typ) -> distribute_access_exp f kind r c arg1 + | UnOp (_,e,_) + | Real e + | Imag e + | SizeOfE e + | AlignOfE e -> + distribute_access_exp f kind r c e (* The address operators, we just check the accesses under them *) | AddrOf lval | StartOf lval -> @@ -277,7 +285,12 @@ and distribute_access_exp f kind r c = function distribute_access_exp f `Read r c b; distribute_access_exp f kind r c t; distribute_access_exp f kind r c e - | _ -> () + | Const _ + | SizeOf _ + | SizeOfStr _ + | AlignOf _ + | AddrOfLabel _ -> + () let add side e kind conf vo oo a = let ty = get_val_type e vo oo in diff --git a/src/domains/invariantCil.ml b/src/domains/invariantCil.ml index 1306dfed65..ed9e7d6ddd 100644 --- a/src/domains/invariantCil.ml +++ b/src/domains/invariantCil.ml @@ -39,13 +39,26 @@ let exp_is_in_scope scope e = let tmp_var_regexp = Str.regexp "^\\(tmp\\(___[0-9]+\\)?\\|cond\\|RETURN\\)$" (* let var_is_tmp {vname; _} = Str.string_match tmp_var_regexp vname 0 *) let var_is_tmp vi = Option.is_none (Cilfacade.find_original_name vi) -(* TODO: use visitor for this *) -let rec exp_contains_tmp = function - | Lval (Var vi, _) -> var_is_tmp vi - | UnOp (_, e, _) -> exp_contains_tmp e - | BinOp (_, e1, e2, _) -> exp_contains_tmp e1 || exp_contains_tmp e2 - | CastE (_, e) -> exp_contains_tmp e - | exp -> exp = MyCFG.unknown_exp +class exp_contains_tmp_visitor (acc: bool ref) = object + inherit nopCilVisitor as super + method! vvrbl (vi: varinfo) = + if var_is_tmp vi then + acc := true; + SkipChildren + + method! vexpr (e: exp) = + if e = MyCFG.unknown_exp then ( + acc := true; + SkipChildren + ) + else + super#vexpr e +end +let exp_contains_tmp e = + let acc = ref false in + let visitor = new exp_contains_tmp_visitor acc in + ignore (visitCilExpr visitor e); + !acc (* TODO: synchronize magic constant with BaseDomain *) let var_is_heap {vname; _} = BatString.starts_with vname "(alloc@" diff --git a/src/framework/control.ml b/src/framework/control.ml index 2e8c5fafa0..2da81712de 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -678,6 +678,11 @@ struct YWitness.write lh gh ); + if get_string "witness.yaml.validate" <> "" then ( + let module YWitness = YamlWitness.Validator (Spec) (EQSys) (LHT) (GHT) in + YWitness.validate lh gh file + ); + let marshal = Spec.finalize () in (* copied from solve_and_postprocess *) let gobview = get_bool "gobview" in diff --git a/src/incremental/compareAST.ml b/src/incremental/compareAST.ml index b4e1a7b7f4..0a57bf0f7d 100644 --- a/src/incremental/compareAST.ml +++ b/src/incremental/compareAST.ml @@ -41,6 +41,10 @@ and eq_exp (a: exp) (b: exp) = match a,b with | CastE (typ1, exp1), CastE (typ2, exp2) -> eq_typ typ1 typ2 && eq_exp exp1 exp2 | AddrOf lv1, AddrOf lv2 -> eq_lval lv1 lv2 | StartOf lv1, StartOf lv2 -> eq_lval lv1 lv2 + | Real exp1, Real exp2 -> eq_exp exp1 exp2 + | Imag exp1, Imag exp2 -> eq_exp exp1 exp2 + | Question (b1, t1, f1, typ1), Question (b2, t2, f2, typ2) -> eq_exp b1 b2 && eq_exp t1 t2 && eq_exp f1 f2 && eq_typ typ1 typ2 + | AddrOfLabel _, AddrOfLabel _ -> false (* TODO: what to do? *) | _, _ -> false and eq_lhost (a: lhost) (b: lhost) = match a, b with diff --git a/src/transform/evalAssert.ml b/src/transform/evalAssert.ml index 71f4a40769..000ae48b53 100644 --- a/src/transform/evalAssert.ml +++ b/src/transform/evalAssert.ml @@ -100,14 +100,6 @@ module EvalAssert = struct instrument_instructions il in - let rec get_vars e = - match e with - | Lval (Var v, _) -> [v] - | UnOp (_, e, _) -> get_vars e - | BinOp (_, e1, e2, _) -> (get_vars e1) @ (get_vars e2) - | _ -> [] - in - let instrument_join s = match s.preds with | [p1; p2] when emit_other -> @@ -126,7 +118,7 @@ module EvalAssert = struct s.skind <- Instr (instrument_instructions il s); s | If (e, b1, b2, l,l2) -> - let vars = get_vars e in + let vars = Basetype.CilExp.get_vars e in let asserts loc vs = if full then make_assert loc None else List.map (fun x -> make_assert loc (Some (Var x,NoOffset))) vs |> List.concat in let add_asserts block = if block.bstmts <> [] then diff --git a/src/util/messageCategory.ml b/src/util/messageCategory.ml index 6ec026fa83..cf51baacc1 100644 --- a/src/util/messageCategory.ml +++ b/src/util/messageCategory.ml @@ -35,6 +35,7 @@ type category = | Analyzer | Unsound | Imprecise + | Witness [@@deriving eq, ord, hash] type t = category [@@deriving eq, ord, hash] @@ -169,6 +170,7 @@ let should_warn e = | Analyzer -> "analyzer" | Unsound -> "unsound" | Imprecise -> "imprecise" + | Witness -> "witness" in get_bool ("warn." ^ (to_string e)) let path_show e = @@ -184,6 +186,7 @@ let path_show e = | Analyzer -> ["Analyzer"] | Unsound -> ["Unsound"] | Imprecise -> ["Imprecise"] + | Witness -> ["Witness"] let show x = String.concat " > " (path_show x) @@ -208,6 +211,7 @@ let categoryName = function | Analyzer -> "Analyzer" | Unsound -> "Unsound" | Imprecise -> "Imprecise" + | Witness -> "Witness" | Behavior x -> behaviorName x | Integer x -> match x with @@ -229,6 +233,7 @@ let from_string_list (s: string list) = | "analyzer" -> Analyzer | "unsound" -> Unsound | "imprecise" -> Imprecise + | "witness" -> Witness | _ -> Unknown let to_yojson x = `List (List.map (fun x -> `String x) (path_show x)) diff --git a/src/util/options.schema.json b/src/util/options.schema.json index aea3a7284e..78049f8bf2 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -1580,6 +1580,12 @@ "type": "boolean", "default": true }, + "witness": { + "title": "warn.witness", + "description": "Witness messages", + "type": "boolean", + "default": true + }, "unknown": { "title": "warn.unknown", "description": "Unknown (of string) warnings", @@ -1804,6 +1810,18 @@ "description": "YAML witness output path", "type": "string", "default": "witness.yml" + }, + "validate": { + "title": "witness.yaml.validate", + "description": "YAML witness input path", + "type": "string", + "default": "" + }, + "certificate": { + "title": "witness.yaml.certificate", + "description": "YAML witness certificate output path", + "type": "string", + "default": "witness.certificate.yml" } }, "additionalProperties": false diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 80f3e534e0..a62a4366e7 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -2,6 +2,87 @@ open Analyses let uuid_random_state = Random.State.make_self_init () +let sha256_file f = Sha256.(to_hex (file f)) +let sha256_file_cache = BatCache.make_ht ~gen:sha256_file ~init_size:5 +let sha256_file = sha256_file_cache.get + +module Entry = +struct + (* yaml_conf is too verbose *) + (* let yaml_conf: Yaml.value = Json_repr.convert (module Json_repr.Yojson) (module Json_repr.Ezjsonm) (!GobConfig.json_conf) in *) + let yaml_producer = `O [ + ("name", `String "Goblint"); + ("version", `String Version.goblint); + (* TODO: configuration *) + (* ("configuration", yaml_conf); *) (* yaml_conf is too verbose *) + ("command_line", `String Goblintutil.command_line); + (* TODO: description *) + ] + + let yaml_metadata ?(extra=[]) () = + let uuid = Uuidm.v4_gen uuid_random_state () in + let creation_time = TimeUtil.iso8601_now () in + `O ([ + ("format_version", `String "0.1"); + ("uuid", `String (Uuidm.to_string uuid)); + ("creation_time", `String creation_time); + ("producer", yaml_producer); + ] @ extra) + + let yaml_task ~input_files ~data_model ~specification = + `O ([ + ("input_files", `A (List.map Yaml.Util.string input_files)); + ("input_file_hashes", `O (List.map (fun file -> + (file, `String (sha256_file file)) + ) input_files)); + ("data_model", `String data_model); + ("language", `String "C"); + ] @ match specification with + | Some specification -> [ + ("specification", `String specification) + ] + | None -> + [] + ) + + let yaml_loop_invariant ~yaml_task ~location:(loc:Cil.location) ~location_function ~invariant = + `O [ + ("entry_type", `String "loop_invariant"); + ("metadata", yaml_metadata ~extra:[ + ("task", yaml_task); + ] ()); + ("location", `O [ + ("file_name", `String loc.file); + ("file_hash", `String (sha256_file loc.file)); + ("line", `Float (float_of_int loc.line)); + ("column", `Float (float_of_int (loc.column - 1))); + ("function", `String location_function); + ]); + ("loop_invariant", `O [ + ("string", `String invariant); + ("type", `String "assertion"); + ("format", `String "C"); + ]); + ] + + let yaml_loop_invariant_certificate ~target_uuid ~target_file_name ~verdict = + `O [ + ("entry_type", `String "loop_invariant_certificate"); + ("metadata", yaml_metadata ()); + ("target", `O [ + ("uuid", `String target_uuid); + ("type", `String "loop_invariant"); (* TODO: check *) + ("file_hash", `String (sha256_file target_file_name)); + ]); + ("certification", `O [ + ("string", `String (if verdict then "confirmed" else "rejected")); + ("type", `String "verdict"); + ("format", `String "confirmed | rejected"); + ]); + ] +end + + module Make (File: WitnessUtil.File) (Cfg: MyCFG.CfgBidir) @@ -27,40 +108,17 @@ struct nh let write lh gh = - (* yaml_conf is too verbose *) - (* let yaml_conf: Yaml.value = Json_repr.convert (module Json_repr.Yojson) (module Json_repr.Ezjsonm) (!GobConfig.json_conf) in *) - let yaml_creation_time = `String (TimeUtil.iso8601_now ()) in - let yaml_producer = `O [ - ("name", `String "Goblint"); - ("version", `String Version.goblint); - (* TODO: configuration *) - (* ("configuration", yaml_conf); *) (* yaml_conf is too verbose *) - ("command_line", `String Goblintutil.command_line); - (* TODO: description *) - ] + let input_files = GobConfig.get_string_list "files" in + let data_model = match GobConfig.get_string "exp.architecture" with + | "64bit" -> "LP64" + | "32bit" -> "ILP32" + | _ -> failwith "invalid architecture" in - let files = GobConfig.get_string_list "files" in - let sha256_file f = Sha256.(to_hex (file f)) in - let sha256_file_cache = BatCache.make_ht ~gen:sha256_file ~init_size:5 in - let sha256_file = sha256_file_cache.get in - let yaml_task = `O ([ - ("input_files", `A (List.map Yaml.Util.string files)); - ("input_file_hashes", `O (List.map (fun file -> - (file, `String (sha256_file file)) - ) files)); - ("data_model", `String (match GobConfig.get_string "exp.architecture" with - | "64bit" -> "LP64" - | "32bit" -> "ILP32" - | _ -> failwith "invalid architecture")); - ("language", `String "C"); - ] @ match !Svcomp.task with - | Some (module Task) -> [ - ("specification", `String (Svcomp.Specification.to_string Task.specification)) - ] - | None -> - [] - ) + let specification = Option.map (fun (module Task: Svcomp.Task) -> + Svcomp.Specification.to_string Task.specification + ) !Svcomp.task in + let yaml_task = Entry.yaml_task ~input_files ~data_model ~specification in let nh = join_contexts lh in @@ -80,30 +138,9 @@ struct let loc = Node.location n in let invs = WitnessUtil.InvariantExp.process_exp inv in List.fold_left (fun acc inv -> - let uuid = Uuidm.v4_gen uuid_random_state () in - let entry = `O [ - ("entry_type", `String "loop_invariant"); - ("metadata", `O [ - ("format_version", `String "0.1"); - ("uuid", `String (Uuidm.to_string uuid)); - ("creation_time", yaml_creation_time); - ("producer", yaml_producer); - ("task", yaml_task); - ]); - ("location", `O [ - ("file_name", `String loc.file); - ("file_hash", `String (sha256_file loc.file)); - ("line", `Float (float_of_int loc.line)); - ("column", `Float (float_of_int (loc.column - 1))); - ("function", `String (Node.find_fundec n).svar.vname); - ]); - ("loop_invariant", `O [ - ("string", `String (CilType.Exp.show inv)); - ("type", `String "assertion"); - ("format", `String "C"); - ]); - ] - in + let location_function = (Node.find_fundec n).svar.vname in + let invariant = CilType.Exp.show inv in + let entry = Entry.yaml_loop_invariant ~yaml_task ~location:loc ~location_function ~invariant in entry :: acc ) acc invs | None -> @@ -117,3 +154,195 @@ struct let yaml = `A yaml_entries in Yaml_unix.to_file_exn (Fpath.v (GobConfig.get_string "witness.yaml.path")) yaml end + + +module ValidationResult = +struct + (* constructor order is important for the chain lattice *) + type result = + | Confirmed + | Unconfirmed + | Refuted + | ParseError + [@@deriving enum, show] + + module ChainParams = + struct + let n = max_result - 1 + let names i = show_result (Option.get (result_of_enum i)) + end + include Lattice.Chain (ChainParams) +end + +module Validator + (Spec : Spec) + (EQSys : GlobConstrSys with module LVar = VarF (Spec.C) + and module GVar = GVarF (Spec.V) + and module D = Spec.D + and module G = Spec.G) + (LHT : BatHashtbl.S with type key = EQSys.LVar.t) + (GHT : BatHashtbl.S with type key = EQSys.GVar.t) = +struct + + module FileH = BatHashtbl.Make (Basetype.RawStrings) + module LocM = BatMap.Make (CilType.Location) + module LvarS = BatSet.Make (EQSys.LVar) + + let validate lh gh (file: Cil.file) = + (* for each file, locations (of lvar nodes) have total order, so LocM essentially does binary search *) + let file_loc_lvars: LvarS.t LocM.t FileH.t = FileH.create 100 in + LHT.iter (fun ((n, _) as lvar) _ -> + let loc = Node.location n in + FileH.modify_def LocM.empty loc.file ( + LocM.modify_def LvarS.empty loc (LvarS.add lvar) + ) file_loc_lvars + ) lh; + + let global_vars = List.filter_map (function + | Cil.GVar (v, _, _) -> Some v + | _ -> None + ) file.globals + in + + let ask_local (lvar:EQSys.LVar.t) local = + (* build a ctx for using the query system *) + let rec ctx = + { ask = (fun (type a) (q: a Queries.t) -> Spec.query ctx q) + ; emit = (fun _ -> failwith "Cannot \"emit\" in witness context.") + ; node = fst lvar + ; prev_node = MyCFG.dummy_node + ; control_context = Obj.repr (fun () -> snd lvar) + ; context = (fun () -> snd lvar) + ; edge = MyCFG.Skip + ; local = local + ; global = GHT.find gh + ; presub = (fun _ -> raise Not_found) + ; spawn = (fun v d -> failwith "Cannot \"spawn\" in witness context.") + ; split = (fun d es -> failwith "Cannot \"split\" in witness context.") + ; sideg = (fun v g -> failwith "Cannot \"sideg\" in witness context.") + } + in + Spec.query ctx + in + + let yaml = Yaml_unix.of_file_exn (Fpath.v (GobConfig.get_string "witness.yaml.validate")) in + let yaml_entries = match yaml with + | `A yaml_entries -> yaml_entries + | _ -> failwith "invalid YAML" + in + + let yaml_entries' = List.fold_left (fun yaml_entries' yaml_entry -> + let yaml_metadata = Yaml.Util.(yaml_entry |> find_exn "metadata" |> Option.get) in + let uuid = Yaml.Util.(yaml_metadata |> find_exn "uuid" |> Option.get |> to_string_exn) in + let yaml_location = Yaml.Util.(yaml_entry |> find_exn "location" |> Option.get) in + let file = Yaml.Util.(yaml_location |> find_exn "file_name" |> Option.get |> to_string_exn) in + let line = Yaml.Util.(yaml_location |> find_exn "line" |> Option.get |> to_float_exn |> int_of_float) in + let column = Yaml.Util.(yaml_location |> find_exn "column" |> Option.get |> to_float_exn |> int_of_float) + 1 in + let inv = Yaml.Util.(yaml_entry |> find_exn "loop_invariant" |> Option.get |> find_exn "string" |> Option.get |> to_string_exn) in + let loc: Cil.location = { + file; + line; + column; + byte = -1; + endLine = -1; + endColumn = -1; + endByte = -1; + } + in + + match Frontc.parse_standalone_exp inv with + | inv_cabs -> + + let lvars_opt: LvarS.t option = + let (let*) = Option.bind in (* TODO: move to general library *) + let* loc_lvars = FileH.find_option file_loc_lvars loc.file in + (* for each file, locations (of lvar nodes) have total order, so LocM essentially does binary search *) + let* (_, lvars) = LocM.find_first_opt (fun loc' -> + CilType.Location.compare loc loc' <= 0 (* allow inexact match *) + ) loc_lvars + in + if LvarS.is_empty lvars then + None + else + Some lvars + in + + begin match lvars_opt with + | Some lvars -> + let module VR = ValidationResult in + + let result = LvarS.fold (fun ((n, _) as lvar) (acc: VR.t) -> + let d = LHT.find lh lvar in + let fd = Node.find_fundec n in + let vars = fd.sformals @ fd.slocals @ global_vars in + + let genv = Cabs2cil.genvironment in + let env = Hashtbl.copy genv in + List.iter (fun (v: Cil.varinfo) -> + Hashtbl.replace env v.vname (Cabs2cil.EnvVar v, v.vdecl) + ) (fd.sformals @ fd.slocals); + + let inv_exp_opt = + Cil.currentLoc := loc; + Cil.currentExpLoc := loc; + Cabs2cil.currentFunctionFDEC := fd; + let old_locals = fd.slocals in + let old_useLogicalOperators = !Cil.useLogicalOperators in + Fun.protect ~finally:(fun () -> + fd.slocals <- old_locals; (* restore locals, Cabs2cil may mangle them by inserting temporary variables *) + Cil.useLogicalOperators := old_useLogicalOperators + ) (fun () -> + Cil.useLogicalOperators := true; + Cabs2cil.convStandaloneExp ~genv ~env inv_cabs + ) + in + + let result: VR.result = match inv_exp_opt with + | Some inv_exp when Check.checkStandaloneExp ~vars inv_exp -> + begin match ask_local lvar d (Queries.EvalInt inv_exp) with + | x when Queries.ID.is_bool x -> + let verdict = Option.get (Queries.ID.to_bool x) in + if verdict then + Confirmed + else + Refuted + | _ -> + Unconfirmed + end + | _ -> + ParseError + in + VR.join acc (VR.result_to_enum result) + ) lvars (VR.bot ()) + in + + begin match Option.get (VR.result_of_enum result) with + | Confirmed -> + M.success ~category:Witness ~loc "invariant confirmed: %s" inv; + let certificate_entry = Entry.yaml_loop_invariant_certificate ~target_uuid:uuid ~target_file_name:loc.file ~verdict:true in + certificate_entry :: yaml_entry :: yaml_entries' + | Unconfirmed -> + M.warn ~category:Witness ~loc "invariant unconfirmed: %s" inv;yaml_entry :: yaml_entries' + | Refuted -> + M.error ~category:Witness ~loc "invariant refuted: %s" inv;let certificate_entry = Entry.yaml_loop_invariant_certificate ~target_uuid:uuid ~target_file_name:loc.file ~verdict:false in + certificate_entry :: yaml_entry :: yaml_entries' + | ParseError -> + M.error ~category:Witness ~loc "CIL couldn't parse invariant: %s" inv; + M.info ~category:Witness ~loc "invariant has undefined variables or side effects: %s" inv; + yaml_entry :: yaml_entries' + end + | None -> + M.warn ~category:Witness ~loc "couldn't locate invariant: %s" inv; + yaml_entry :: yaml_entries' + end + | exception Frontc.ParseError _ -> + Errormsg.log "\n"; (* CIL prints garbage without \n before *) + M.error ~category:Witness ~loc "Frontc couldn't parse invariant: %s" inv; + M.info ~category:Witness ~loc "invariant has invalid syntax: %s" inv; + yaml_entry :: yaml_entries' + ) [] yaml_entries + in + + let yaml' = `A (List.rev yaml_entries') in + Yaml_unix.to_file_exn (Fpath.v (GobConfig.get_string "witness.yaml.certificate")) yaml' +end