From b49f0e0553df9b8fc34205636f9559745bd2e690 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 22 Aug 2023 17:50:06 +0300 Subject: [PATCH] Use MayPointToA and ReachableFromA in accessAnalysis Co-authored-by: Simmo Saan --- src/analyses/accessAnalysis.ml | 33 ++++++++++++--------------- src/analyses/modifiedSinceLongjmp.ml | 13 ++++++++++- src/analyses/mutexAnalysis.ml | 34 +++++++++++++--------------- src/analyses/poisonVariables.ml | 17 +++++++++----- src/analyses/raceAnalysis.ml | 32 +++++++++++++------------- src/domains/events.ml | 4 ++-- 6 files changed, 71 insertions(+), 62 deletions(-) diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml index bc5330726c..9c2cc31eda 100644 --- a/src/analyses/accessAnalysis.ml +++ b/src/analyses/accessAnalysis.ml @@ -33,7 +33,7 @@ struct let do_access (ctx: (D.t, G.t, C.t, V.t) ctx) (kind:AccessKind.t) (reach:bool) (e:exp) = if M.tracing then M.trace "access" "do_access %a %a %B\n" d_exp e AccessKind.pretty kind reach; - let reach_or_mpt: _ Queries.t = if reach then ReachableFrom e else MayPointTo e in + let reach_or_mpt: _ Queries.t = if reach then ReachableFromA e else MayPointToA e in let ls = ctx.ask reach_or_mpt in ctx.emit (Access {exp=e; lvals=ls; kind; reach}) @@ -138,24 +138,19 @@ struct let event ctx e octx = match e with | Events.Access {lvals; kind; _} when !collect_local && !AnalysisState.postsolving -> - begin match lvals with - | ls when Queries.LS.is_top ls -> - let access: AccessDomain.Event.t = {var_opt = None; offs_opt = None; kind} in - ctx.sideg ctx.node (G.singleton access) - | ls -> - let events = Queries.LS.fold (fun (var, offs) acc -> - let coffs = Offset.Exp.to_cil offs in - let access: AccessDomain.Event.t = - if CilType.Varinfo.equal var dummyFunDec.svar then - {var_opt = None; offs_opt = (Some coffs); kind} - else - {var_opt = (Some var); offs_opt = (Some coffs); kind} - in - G.add access acc - ) ls (G.empty ()) - in - ctx.sideg ctx.node events - end + let events = Queries.AD.fold (fun addr acc -> + match addr with + | Queries.AD.Addr.Addr (var, offs) -> + let coffs = Offset.Exp.to_cil (ValueDomain.Offs.to_exp offs) in + let access: AccessDomain.Event.t = {var_opt = (Some var); offs_opt = (Some coffs); kind} in + G.add access acc + | UnknownPtr -> + let access: AccessDomain.Event.t = {var_opt = None; offs_opt = None; kind} in + G.add access acc + | _ -> acc + ) lvals (G.empty ()) + in + ctx.sideg ctx.node events | _ -> ctx.local end diff --git a/src/analyses/modifiedSinceLongjmp.ml b/src/analyses/modifiedSinceLongjmp.ml index f489b08fe9..836cf6f827 100644 --- a/src/analyses/modifiedSinceLongjmp.ml +++ b/src/analyses/modifiedSinceLongjmp.ml @@ -29,6 +29,17 @@ struct 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 ls = + (* TODO: what about AD with both known and unknown pointers? *) + if Queries.AD.is_top ls then + VS.top () + else + Queries.AD.fold (fun addr acc -> + match addr with + | Queries.AD.Addr.Addr (v, _) -> if is_relevant v then VS.add v acc else 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 *) @@ -63,7 +74,7 @@ struct let event ctx (e: Events.t) octx = match e with | Access {lvals; kind = Write; _} -> - add_to_all_defined (relevants_from_ls lvals) ctx.local + add_to_all_defined (relevants_from_ad lvals) ctx.local | _ -> ctx.local end diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 154f7ba183..7f504badf2 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -296,7 +296,7 @@ struct | Events.Access {exp; lvals; kind; _} when ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) -> (* threadflag query in post-threadspawn ctx *) let is_recovered_to_st = not (ThreadFlag.is_currently_multi (Analyses.ask_of_ctx ctx)) in (* must use original (pre-assign, etc) ctx queries *) - let old_access var_opt offs_opt = + let old_access var_opt = (* TODO: this used to use ctx instead of octx, why? *) (*privatization*) match var_opt with @@ -325,24 +325,22 @@ struct ) | None -> M.info ~category:Unsound "Write to unknown address: privatization is unsound." in - let module LS = Queries.LS in + let module AD = Queries.AD in let has_escaped g = octx.ask (Queries.MayEscape g) in - let on_lvals ls = - let ls = LS.filter (fun (g,_) -> g.vglob || has_escaped g) ls in - let f (var, offs) = - let coffs = Offset.Exp.to_cil offs in - if CilType.Varinfo.equal var dummyFunDec.svar then - old_access None (Some coffs) - else - old_access (Some var) (Some coffs) + let on_lvals ad = + let f addr = + match addr with + | AD.Addr.Addr (g,o) when g.vglob || has_escaped g -> old_access (Some g) + | UnknownPtr -> old_access None + | _ -> () in - LS.iter f ls + AD.iter f ad in begin match lvals with - | ls when not (LS.is_top ls) && not (Queries.LS.mem (dummyFunDec.svar,`NoOffset) ls) -> + | ad when not (AD.is_top ad) -> (* the case where the points-to set is non top and does not contain unknown values *) - on_lvals ls - | ls when not (LS.is_top ls) -> + on_lvals ad + | ad -> (* the case where the points-to set is non top and contains unknown values *) (* now we need to access all fields that might be pointed to: is this correct? *) begin match octx.ask (ReachableUkTypes exp) with @@ -354,11 +352,11 @@ struct | _ -> false in if Queries.TS.exists f ts then - old_access None None + old_access None end; - on_lvals ls - | _ -> - old_access None None + on_lvals ad + (* | _ -> + old_access None None *) end; ctx.local | _ -> diff --git a/src/analyses/poisonVariables.ml b/src/analyses/poisonVariables.ml index 5cb34baa26..b124cb90f0 100644 --- a/src/analyses/poisonVariables.ml +++ b/src/analyses/poisonVariables.ml @@ -80,23 +80,28 @@ struct ) longjmp_nodes; D.join modified_locals ctx.local | Access {lvals; kind = Read; _} -> - if Queries.LS.is_top lvals then ( + (* TODO: what about AD with both known and unknown pointers? *) + if Queries.AD.is_top lvals then ( if not (VS.is_empty octx.local) then M.warn ~category:(Behavior (Undefined Other)) "reading unknown memory location, may be tainted!" ) else ( - Queries.LS.iter (fun lv -> + Queries.AD.iter (function (* Use original access state instead of current with removed written vars. *) - check_lval octx.local lv + | Queries.AD.Addr.Addr (v,o) -> check_lval octx.local (v, ValueDomain.Offs.to_exp o) + | _ -> () ) lvals ); ctx.local | Access {lvals; kind = Write; _} -> - if Queries.LS.is_top lvals then + (* TODO: what about AD with both known and unknown pointers? *) + if Queries.AD.is_top lvals then ctx.local else ( - Queries.LS.fold (fun lv acc -> - rem_lval acc lv + Queries.AD.fold (fun addr acc -> + match addr with + | Queries.AD.Addr.Addr (v,o) -> rem_lval acc (v, ValueDomain.Offs.to_exp o) + | _ -> acc ) lvals ctx.local ) | _ -> ctx.local diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index 970895e971..11e77bf902 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -134,7 +134,7 @@ struct | Events.Access {exp=e; lvals; kind; reach} when ThreadFlag.is_currently_multi (Analyses.ask_of_ctx ctx) -> (* threadflag query in post-threadspawn ctx *) (* must use original (pre-assign, etc) ctx queries *) let conf = 110 in - let module LS = Queries.LS in + let module AD = Queries.AD in let part_access (vo:varinfo option): MCPAccess.A.t = (*partitions & locks*) Obj.obj (octx.ask (PartAccess (Memory {exp=e; var_opt=vo; kind}))) @@ -151,24 +151,24 @@ struct let has_escaped g = octx.ask (Queries.MayEscape g) in (* The following function adds accesses to the lval-set ls -- this is the common case if we have a sound points-to set. *) - let on_lvals ls includes_uk = - let ls = LS.filter (fun (g,_) -> g.vglob || has_escaped g) ls in + let on_lvals ad includes_uk = let conf = if reach then conf - 20 else conf in let conf = if includes_uk then conf - 10 else conf in - let f (var, offs) = - let coffs = Offset.Exp.to_cil offs in - if CilType.Varinfo.equal var dummyFunDec.svar then - add_access conf None - else - add_access conf (Some (var, coffs)) + let f addr = + match addr with + | AD.Addr.Addr (g,o) when g.vglob || has_escaped g -> + let coffs = Offset.Exp.to_cil (ValueDomain.Offs.to_exp o) in + add_access conf (Some (g, coffs)) + | UnknownPtr -> add_access conf None + | _ -> () in - LS.iter f ls + AD.iter f ad in begin match lvals with - | ls when not (LS.is_top ls) && not (Queries.LS.mem (dummyFunDec.svar,`NoOffset) ls) -> + | ad when not (AD.is_top ad) -> (* the case where the points-to set is non top and does not contain unknown values *) - on_lvals ls false - | ls when not (LS.is_top ls) -> + on_lvals ad false + | ad -> (* the case where the points-to set is non top and contains unknown values *) let includes_uk = ref false in (* now we need to access all fields that might be pointed to: is this correct? *) @@ -185,9 +185,9 @@ struct in Queries.TS.iter f ts end; - on_lvals ls !includes_uk - | _ -> - add_access (conf - 60) None + on_lvals ad !includes_uk + (* | _ -> + add_access (conf - 60) None *) end; ctx.local | _ -> diff --git a/src/domains/events.ml b/src/domains/events.ml index 2141ad17dd..41e745ed8a 100644 --- a/src/domains/events.ml +++ b/src/domains/events.ml @@ -10,7 +10,7 @@ type t = | EnterMultiThreaded | SplitBranch of exp * bool (** Used to simulate old branch-based split. *) | AssignSpawnedThread of lval * ThreadIdDomain.Thread.t (** Assign spawned thread's ID to lval. *) - | Access of {exp: CilType.Exp.t; lvals: Queries.LS.t; kind: AccessKind.t; reach: bool} + | Access of {exp: CilType.Exp.t; lvals: Queries.AD.t; kind: AccessKind.t; reach: bool} | Assign of {lval: CilType.Lval.t; exp: CilType.Exp.t} (** Used to simulate old [ctx.assign]. *) (* TODO: unused *) | UpdateExpSplit of exp (** Used by expsplit analysis to evaluate [exp] on post-state. *) | Assert of exp @@ -41,7 +41,7 @@ let pretty () = function | EnterMultiThreaded -> text "EnterMultiThreaded" | SplitBranch (exp, tv) -> dprintf "SplitBranch (%a, %B)" d_exp exp tv | AssignSpawnedThread (lval, tid) -> dprintf "AssignSpawnedThread (%a, %a)" d_lval lval ThreadIdDomain.Thread.pretty tid - | Access {exp; lvals; kind; reach} -> dprintf "Access {exp=%a; lvals=%a; kind=%a; reach=%B}" CilType.Exp.pretty exp Queries.LS.pretty lvals AccessKind.pretty kind reach + | Access {exp; lvals; kind; reach} -> dprintf "Access {exp=%a; lvals=%a; kind=%a; reach=%B}" CilType.Exp.pretty exp Queries.AD.pretty lvals AccessKind.pretty kind reach | Assign {lval; exp} -> dprintf "Assign {lval=%a, exp=%a}" CilType.Lval.pretty lval CilType.Exp.pretty exp | UpdateExpSplit exp -> dprintf "UpdateExpSplit %a" d_exp exp | Assert exp -> dprintf "Assert %a" d_exp exp