Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use AddressDomain for queries #1144

Merged
merged 21 commits into from
Sep 27, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
95 changes: 47 additions & 48 deletions src/analyses/base.ml
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 @@ -2400,34 +2392,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 @@ -2442,9 +2438,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 @@ -2459,7 +2455,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
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
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
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
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
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
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
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