Skip to content

Commit

Permalink
Merge pull request #1144 from goblint/queries-ad-cont
Browse files Browse the repository at this point in the history 
Use `AddressDomain` for queries
  • Loading branch information
@sim642
sim642 authored Sep 27, 2023
2 parents 7f9ec9a + e718562 commit f982bc9
Show file tree
Hide file tree
Showing 10 changed files with 113 additions and 139 deletions.
95 changes: 47 additions & 48 deletions src/analyses/base.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1097,20 +1097,15 @@ struct
| Int x -> ValueDomain.ID.to_int x
| _ -> None

let eval_funvar ctx fval: varinfo list =
let exception OnlyUnknown in
try
let fp = eval_fv (Analyses.ask_of_ctx ctx) ctx.global ctx.local fval in
if AD.mem Addr.UnknownPtr fp then begin
let others = AD.to_var_may fp in
if others = [] then raise OnlyUnknown;
M.warn ~category:Imprecise ~tags:[Category Call] "Function pointer %a may contain unknown functions." d_exp fval;
dummyFunDec.svar :: others
end else
AD.to_var_may fp
with SetDomain.Unsupported _ | OnlyUnknown ->
M.warn ~category:Imprecise ~tags:[Category Call] "Unknown call to function %a." d_exp fval;
[dummyFunDec.svar]
let eval_funvar ctx fval: Queries.AD.t =
let fp = eval_fv (Analyses.ask_of_ctx ctx) ctx.global ctx.local fval in
if AD.is_top fp then (
if AD.cardinal fp = 1 then
M.warn ~category:Imprecise ~tags:[Category Call] "Unknown call to function %a." d_exp fval
else
M.warn ~category:Imprecise ~tags:[Category Call] "Function pointer %a may contain unknown functions." d_exp fval
);
fp

(** Evaluate expression as address.
Avoids expensive Apron EvalInt if the Int result would be useless to us anyway. *)
Expand Down Expand Up @@ -1204,10 +1199,7 @@ struct
let query ctx (type a) (q: a Q.t): a Q.result =
match q with
| Q.EvalFunvar e ->
begin
let fs = eval_funvar ctx e in
List.fold_left (fun xs v -> Q.LS.add (v,`NoOffset) xs) (Q.LS.empty ()) fs
end
eval_funvar ctx e
| Q.EvalJumpBuf e ->
begin match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with
| Address jmp_buf ->
Expand Down Expand Up @@ -2411,34 +2403,38 @@ struct
in
if get_bool "sem.noreturn.dead_code" && Cil.hasAttribute "noreturn" f.vattr then raise Deadcode else st

let combine_st ctx (local_st : store) (fun_st : store) (tainted_lvs : Q.LS.t) : store =
let combine_st ctx (local_st : store) (fun_st : store) (tainted_lvs : AD.t) : store =
let ask = (Analyses.ask_of_ctx ctx) in
Q.LS.fold (fun (v, o) st ->
if CPA.mem v fun_st.cpa then
let lval = Mval.Exp.to_cil (v,o) in
let address = eval_lv ask ctx.global st lval in
let lval_type = (AD.type_of address) in
if M.tracing then M.trace "taintPC" "updating %a; type: %a\n" Mval.Exp.pretty (v, o) d_type lval_type;
match (CPA.find_opt v (fun_st.cpa)), lval_type with
| None, _ -> st
(* partitioned arrays cannot be copied by individual lvalues, so if tainted just copy the whole callee value for the array variable *)
| Some (Array a), _ when (CArrays.domain_of_t a) = PartitionedDomain -> {st with cpa = CPA.add v (Array a) st.cpa}
(* "get" returned "unknown" when applied to a void type, so special case void types. This caused problems with some sv-comps (e.g. regtest 64 11) *)
| Some voidVal, TVoid _ -> {st with cpa = CPA.add v voidVal st.cpa}
| _, _ -> begin
let new_val = get ask ctx.global fun_st address None in
if M.tracing then M.trace "taintPC" "update val: %a\n\n" VD.pretty new_val;
let st' = set_savetop ~ctx ask ctx.global st address lval_type new_val in
let partDep = Dep.find_opt v fun_st.deps in
match partDep with
| None -> st'
(* if a var partitions an array, all cpa-info for arrays it may partition are added from callee to caller *)
| Some deps -> {st' with cpa = (Dep.VarSet.fold (fun v accCPA -> let val_opt = CPA.find_opt v fun_st.cpa in
match val_opt with
| None -> accCPA
| Some new_val -> CPA.add v new_val accCPA ) deps st'.cpa)}
end
else st) tainted_lvs local_st
AD.fold (fun addr st ->
match addr with
| Addr.Addr (v,o) ->
if CPA.mem v fun_st.cpa then
let lval = Addr.Mval.to_cil (v,o) in
let address = eval_lv ask ctx.global st lval in
let lval_type = Addr.type_of addr in
if M.tracing then M.trace "taintPC" "updating %a; type: %a\n" Addr.Mval.pretty (v,o) d_type lval_type;
match (CPA.find_opt v (fun_st.cpa)), lval_type with
| None, _ -> st
(* partitioned arrays cannot be copied by individual lvalues, so if tainted just copy the whole callee value for the array variable *)
| Some (Array a), _ when (CArrays.domain_of_t a) = PartitionedDomain -> {st with cpa = CPA.add v (Array a) st.cpa}
(* "get" returned "unknown" when applied to a void type, so special case void types. This caused problems with some sv-comps (e.g. regtest 64 11) *)
| Some voidVal, TVoid _ -> {st with cpa = CPA.add v voidVal st.cpa}
| _, _ -> begin
let new_val = get ask ctx.global fun_st address None in
if M.tracing then M.trace "taintPC" "update val: %a\n\n" VD.pretty new_val;
let st' = set_savetop ~ctx ask ctx.global st address lval_type new_val in
let partDep = Dep.find_opt v fun_st.deps in
match partDep with
| None -> st'
(* if a var partitions an array, all cpa-info for arrays it may partition are added from callee to caller *)
| Some deps -> {st' with cpa = (Dep.VarSet.fold (fun v accCPA -> let val_opt = CPA.find_opt v fun_st.cpa in
match val_opt with
| None -> accCPA
| Some new_val -> CPA.add v new_val accCPA ) deps st'.cpa)}
end
else st
| _ -> st
) tainted_lvs local_st

let combine_env ctx lval fexp f args fc au (f_ask: Queries.ask) =
let combine_one (st: D.t) (fun_st: D.t) =
Expand All @@ -2453,9 +2449,9 @@ struct
let cpa_noreturn = CPA.remove (return_varinfo ()) fun_st.cpa in
let ask = (Analyses.ask_of_ctx ctx) in
let tainted = f_ask.f Q.MayBeTainted in
if M.tracing then M.trace "taintPC" "combine for %s in base: tainted: %a\n" f.svar.vname Q.LS.pretty tainted;
if M.tracing then M.trace "taintPC" "combine for %s in base: tainted: %a\n" f.svar.vname AD.pretty tainted;
if M.tracing then M.trace "taintPC" "combine base:\ncaller: %a\ncallee: %a\n" CPA.pretty st.cpa CPA.pretty fun_st.cpa;
if Q.LS.is_top tainted then
if AD.is_top tainted then
let cpa_local = CPA.filter (fun x _ -> not (is_global ask x)) st.cpa in
let cpa' = CPA.fold CPA.add cpa_noreturn cpa_local in (* add cpa_noreturn to cpa_local *)
if M.tracing then M.trace "taintPC" "combined: %a\n" CPA.pretty cpa';
Expand All @@ -2470,7 +2466,10 @@ struct
let cpa_caller' = CPA.fold CPA.add cpa_new cpa_caller in
if M.tracing then M.trace "taintPC" "cpa_caller': %a\n" CPA.pretty cpa_caller';
(* remove lvals from the tainted set that correspond to variables for which we just added a new mapping from the callee*)
let tainted = Q.LS.filter (fun (v, _) -> not (CPA.mem v cpa_new)) tainted in
let tainted = AD.filter (function
| Addr.Addr (v,_) -> not (CPA.mem v cpa_new)
| _ -> false
) tainted in
let st_combined = combine_st ctx {st with cpa = cpa_caller'} fun_st tainted in
if M.tracing then M.trace "taintPC" "combined: %a\n" CPA.pretty st_combined.cpa;
{ fun_st with cpa = st_combined.cpa }
Expand Down
18 changes: 6 additions & 12 deletions src/analyses/commonPriv.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -60,14 +60,10 @@ struct
ask.f (Q.MustBeProtectedBy {mutex=m; global=x; write=true; protection})

let protected_vars (ask: Q.ask): varinfo list =
let module VS = Set.Make (CilType.Varinfo) in
Q.LS.fold (fun (v, _) acc ->
let m = ValueDomain.Addr.of_var v in (* TODO: don't ignore offsets *)
Q.LS.fold (fun l acc ->
VS.add (fst l) acc (* always `NoOffset from mutex analysis *)
) (ask.f (Q.MustProtectedVars {mutex = m; write = true})) acc
) (ask.f Q.MustLockset) VS.empty
|> VS.elements
Q.AD.fold (fun m acc ->
Q.VS.join (ask.f (Q.MustProtectedVars {mutex = m; write = true})) acc
) (ask.f Q.MustLockset) (Q.VS.empty ())
|> Q.VS.elements
end

module MutexGlobals =
Expand Down Expand Up @@ -126,10 +122,8 @@ struct
if !AnalysisState.global_initialization then
Lockset.empty ()
else
let ls = ask.f Queries.MustLockset in
Q.LS.fold (fun (var, offs) acc ->
Lockset.add (Lock.of_mval (var, Lock.Offs.of_exp offs)) acc
) ls (Lockset.empty ())
let ad = ask.f Queries.MustLockset in
Q.AD.fold (fun mls acc -> Lockset.add mls acc) ad (Lockset.empty ()) (* TODO: use AD as Lockset *)

(* TODO: reversed SetDomain.Hoare *)
module MinLocksets = HoareDomain.Set_LiftTop (MustLockset) (struct let topname = "All locksets" end) (* reverse Lockset because Hoare keeps maximal, but we need minimal *)
Expand Down
20 changes: 7 additions & 13 deletions src/analyses/modifiedSinceLongjmp.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,29 +23,23 @@ struct
(* Only checks for v.vglob on purpose, acessing espaced locals after longjmp is UB like for any local *)
not v.vglob (* *) && not (BaseUtil.is_volatile v) && v.vstorage <> Static

let relevants_from_ls ls =
if Queries.LS.is_top ls then
VS.top ()
else
Queries.LS.fold (fun (v, _) acc -> if is_relevant v then VS.add v acc else acc) ls (VS.empty ())

let relevants_from_ad ad =
let relevants_from_ad ls =
(* TODO: what about AD with both known and unknown pointers? *)
if Queries.AD.is_top ad then
if Queries.AD.is_top ls then
VS.top ()
else
Queries.AD.fold (fun addr vs ->
Queries.AD.fold (fun addr acc ->
match addr with
| Queries.AD.Addr.Addr (v,_) -> if is_relevant v then VS.add v vs else vs
| _ -> vs
) ad (VS.empty ())
| Queries.AD.Addr.Addr (v, _) when is_relevant v -> VS.add v acc
| _ -> acc
) ls (VS.empty ())

(* transfer functions *)
let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
[ctx.local, D.bot ()] (* enter with bot as opposed to IdentitySpec *)

let combine_env ctx lval fexp f args fc au (f_ask: Queries.ask) =
let taintedcallee = relevants_from_ls (f_ask.f Queries.MayBeTainted) in
let taintedcallee = relevants_from_ad (f_ask.f Queries.MayBeTainted) in
add_to_all_defined taintedcallee ctx.local

let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask:Queries.ask) : D.t =
Expand Down
12 changes: 3 additions & 9 deletions src/analyses/mutexAnalysis.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -233,21 +233,15 @@ struct
Mutexes.leq mutex_lockset protecting
| Queries.MustLockset ->
let held_locks = Lockset.export_locks (Lockset.filter snd ls) in
let ls = Mutexes.fold (fun addr ls ->
match Addr.to_mval addr with
| Some (var, offs) -> Queries.LS.add (var, Addr.Offs.to_exp offs) ls
| None -> ls
) held_locks (Queries.LS.empty ())
in
ls
Mutexes.fold (fun addr ls -> Queries.AD.add addr ls) held_locks (Queries.AD.empty ())
| Queries.MustBeAtomic ->
let held_locks = Lockset.export_locks (Lockset.filter snd ls) in
Mutexes.mem (LockDomain.Addr.of_var LF.verifier_atomic_var) held_locks
| Queries.MustProtectedVars {mutex = m; write} ->
let protected = GProtected.get ~write Strong (G.protected (ctx.global (V.protected m))) in
VarSet.fold (fun v acc ->
Queries.LS.add (v, `NoOffset) acc
) protected (Queries.LS.empty ())
Queries.VS.add v acc
) protected (Queries.VS.empty ())
| Queries.IterSysVars (Global g, f) ->
f (Obj.repr (V.protecting g)) (* TODO: something about V.protected? *)
| WarnGlobal g ->
Expand Down
25 changes: 12 additions & 13 deletions src/analyses/poisonVariables.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,12 +15,16 @@ struct

let context _ _ = ()

let check_mval tainted ((v, offset): Queries.LS.elt) =
if not v.vglob && VS.mem v tainted then
M.warn ~category:(Behavior (Undefined Other)) "Reading poisonous variable %a" CilType.Varinfo.pretty v
let check_mval tainted (addr: Queries.AD.elt) =
match addr with
| Queries.AD.Addr.Addr (v,_) ->
if not v.vglob && VS.mem v tainted then
M.warn ~category:(Behavior (Undefined Other)) "Reading poisonous variable %a" CilType.Varinfo.pretty v
| _ -> ()

let rem_mval tainted ((v, offset): Queries.LS.elt) = match offset with
| `NoOffset -> VS.remove v tainted
let rem_mval tainted (addr: Queries.AD.elt) =
match addr with
| Queries.AD.Addr.Addr (v,`NoOffset) -> VS.remove v tainted
| _ -> tainted (* If there is an offset, it is a bit harder to remove, as we don't know where the indeterminate value is *)


Expand Down Expand Up @@ -88,11 +92,8 @@ struct
| ad when Queries.AD.is_top ad && not (VS.is_empty octx.local) ->
M.warn ~category:(Behavior (Undefined Other)) "reading unknown memory location, may be tainted!"
| ad ->
Queries.AD.iter (function
(* Use original access state instead of current with removed written vars. *)
| Queries.AD.Addr.Addr (v,o) -> check_mval octx.local (v, ValueDomain.Offs.to_exp o)
| _ -> ()
) ad
(* Use original access state instead of current with removed written vars. *)
Queries.AD.iter (check_mval octx.local) ad
end;
ctx.local
| Access {ad; kind = Write; _} ->
Expand All @@ -102,9 +103,7 @@ struct
ctx.local
| ad ->
Queries.AD.fold (fun addr vs ->
match addr with
| Queries.AD.Addr.Addr (v,o) -> rem_mval vs (v, ValueDomain.Offs.to_exp o) (* TODO: use unconverted addrs in domain? *)
| _ -> vs
rem_mval vs addr
) ad ctx.local
end
| _ -> ctx.local
Expand Down
42 changes: 16 additions & 26 deletions src/analyses/taintPartialContexts.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,31 +6,19 @@
open GoblintCil
open Analyses

module D = SetDomain.ToppedSet (Mval.Exp) (struct let topname = "All" end)

let to_mvals ad =
(* TODO: should one handle ad with unknown pointers separately like in (all) other analyses? *)
Queries.AD.fold (fun addr mvals ->
match addr with
| Queries.AD.Addr.Addr (v,o) -> D.add (v, ValueDomain.Offs.to_exp o) mvals (* TODO: use unconverted addrs in domain? *)
| _ -> mvals
) ad (D.empty ())
module AD = ValueDomain.AD

module Spec =
struct
include Analyses.IdentitySpec

let name () = "taintPartialContexts"
module D = D
module D = AD
module C = Lattice.Unit

(* Add Lval or any Lval which it may point to to the set *)
let taint_lval ctx (lval:lval) : D.t =
let d = ctx.local in
(match lval with
| (Var v, offs) -> D.add (v, Offset.Exp.of_cil offs) d
| (Mem e, _) -> D.union (to_mvals (ctx.ask (Queries.MayPointTo e))) d
)
D.union (ctx.ask (Queries.MayPointTo (AddrOf lval))) ctx.local

(* this analysis is context insensitive*)
let context _ _ = ()
Expand All @@ -45,14 +33,12 @@ struct
let d_return =
if D.is_top d then
d
else (
else
let locals = f.sformals @ f.slocals in
D.filter (fun (v, _) ->
not (List.exists (fun local ->
CilType.Varinfo.equal v local && not (ctx.ask (Queries.IsMultiple local))
) locals)
D.filter (function
| AD.Addr.Addr (v,_) -> not (List.exists (fun local -> CilType.Varinfo.equal v local && not (ctx.ask (Queries.IsMultiple local))) locals)
| _ -> false
) d
)
in
if M.tracing then M.trace "taintPC" "returning from %s: tainted vars: %a\n without locals: %a\n" f.svar.vname D.pretty d D.pretty d_return;
d_return
Expand Down Expand Up @@ -94,9 +80,10 @@ struct
else
deep_addrs
in
let d = List.fold_left (fun accD addr -> D.union accD (to_mvals (ctx.ask (Queries.MayPointTo addr)))) d shallow_addrs
(* TODO: should one handle ad with unknown pointers separately like in (all) other analyses? *)
let d = List.fold_left (fun accD addr -> D.union accD (ctx.ask (Queries.MayPointTo addr))) d shallow_addrs
in
let d = List.fold_left (fun accD addr -> D.union accD (to_mvals (ctx.ask (Queries.ReachableFrom addr)))) d deep_addrs
let d = List.fold_left (fun accD addr -> D.union accD (ctx.ask (Queries.ReachableFrom addr))) d deep_addrs
in
d

Expand All @@ -111,7 +98,7 @@ struct

let query ctx (type a) (q: a Queries.t) : a Queries.result =
match q with
| MayBeTainted -> (ctx.local : Queries.LS.t)
| MayBeTainted -> (ctx.local : Queries.AD.t)
| _ -> Queries.Result.top q

end
Expand All @@ -122,5 +109,8 @@ let _ =
module VS = SetDomain.ToppedSet(Basetype.Variables) (struct let topname = "All" end)

(* Convert Lval set to (less precise) Varinfo set. *)
let conv_varset (lval_set : Spec.D.t) : VS.t =
if Spec.D.is_top lval_set then VS.top () else VS.of_list (List.map (fun (v, _) -> v) (Spec.D.elements lval_set))
let conv_varset (addr_set : Spec.D.t) : VS.t =
if Spec.D.is_top addr_set then
VS.top ()
else
VS.of_list (Spec.D.to_var_may addr_set)
8 changes: 6 additions & 2 deletions src/analyses/varEq.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -437,10 +437,14 @@ struct
let d_local =
(* if we are multithreaded, we run the risk, that some mutex protected variables got unlocked, so in this case caller state goes to top
TODO: !!Unsound, this analysis does not handle this case -> regtest 63 08!! *)
if Queries.LS.is_top tainted || not (ctx.ask (Queries.MustBeSingleThreaded {since_start = true})) then
if Queries.AD.is_top tainted || not (ctx.ask (Queries.MustBeSingleThreaded {since_start = true})) then
D.top ()
else
let taint_exp = Queries.ES.of_list (List.map Mval.Exp.to_cil_exp (Queries.LS.elements tainted)) in
let taint_exp =
Queries.AD.to_mval tainted
|> List.map Addr.Mval.to_cil_exp
|> Queries.ES.of_list
in
D.filter (fun exp -> not (Queries.ES.mem exp taint_exp)) ctx.local
in
let d = D.meet au d_local in
Expand Down
2 changes: 1 addition & 1 deletion src/cdomains/lockDomain.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ module IdxDom = ValueDomain.IndexDomain

open GoblintCil

module Mutexes = SetDomain.ToppedSet (Addr) (struct let topname = "All mutexes" end) (* TODO HoareDomain? *)
module Mutexes = SetDomain.ToppedSet (Addr) (struct let topname = "All mutexes" end) (* TODO: AD? *)
module Simple = Lattice.Reverse (Mutexes)
module Priorities = IntDomain.Lifted

Expand Down
Loading

0 comments on commit f982bc9

Please sign in to comment.