From 7edb312254bdbe221f72c57c16ca8a7eacac8263 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 11 Sep 2023 17:29:23 +0300 Subject: [PATCH] Simplify some AddressDomain query result manipulation --- src/analyses/apron/relationAnalysis.apron.ml | 2 +- src/analyses/base.ml | 4 ++-- src/analyses/condVars.ml | 22 +++++++++----------- src/analyses/extractPthread.ml | 21 +++++-------------- src/analyses/pthreadSignals.ml | 6 ++---- src/analyses/useAfterFree.ml | 11 ++-------- 6 files changed, 22 insertions(+), 44 deletions(-) diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index ca60e5dc30..46c620f390 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -276,7 +276,7 @@ struct let reachable_from_args ctx args = let to_vs e = ctx.ask (ReachableFrom e) - |> LockDomain.MayLocksetNoRW.to_var_may + |> Queries.AD.to_var_may |> VS.of_list in List.fold (fun vs e -> VS.join vs (to_vs e)) (VS.empty ()) args diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 4183261ddb..e59d8a2fc6 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1319,8 +1319,8 @@ struct (* ignore @@ printf "EvalStr Address: %a -> %s (must %i, may %i)\n" d_plainexp e (VD.short 80 (Address a)) (List.length @@ AD.to_var_must a) (List.length @@ AD.to_var_may a); *) begin match unrollType (Cilfacade.typeOf e) with | TPtr(TInt(IChar, _), _) -> - let (v,o) = List.hd (AD.to_mval a) in - let lval = Mval.Exp.to_cil @@ (v, Addr.Offs.to_exp o) in + let mval = List.hd (AD.to_mval a) in + let lval = Addr.Mval.to_cil mval in (try `Lifted (Bytes.to_string (Hashtbl.find char_array lval)) with Not_found -> Queries.Result.top q) | _ -> (* what about ISChar and IUChar? *) diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml index 3d07520576..04b148dd02 100644 --- a/src/analyses/condVars.ml +++ b/src/analyses/condVars.ml @@ -64,18 +64,16 @@ struct let (>?) = Option.bind let mayPointTo ctx exp = - match ctx.ask (Queries.MayPointTo exp) with - | ad when not (Queries.AD.is_top ad) && not (Queries.AD.is_empty ad) -> - let a' = if Queries.AD.mem UnknownPtr ad then ( - M.info ~category:Unsound "mayPointTo: query result for %a contains TOP!" d_exp exp; (* UNSOUND *) - Queries.AD.remove UnknownPtr ad - ) else ad - in - List.filter_map (function - | ValueDomain.Addr.Addr (v,o) -> Some (v, ValueDomain.Addr.Offs.to_exp o) (* TODO: use unconverted addrs in domain? *) - | _ -> None - ) (Queries.AD.elements a') - | _ -> [] + let ad = ctx.ask (Queries.MayPointTo exp) in + let a' = if Queries.AD.mem UnknownPtr ad then ( + M.info ~category:Unsound "mayPointTo: query result for %a contains TOP!" d_exp exp; (* UNSOUND *) + Queries.AD.remove UnknownPtr ad + ) else ad + in + List.filter_map (function + | ValueDomain.Addr.Addr (v,o) -> Some (v, ValueDomain.Addr.Offs.to_exp o) (* TODO: use unconverted addrs in domain? *) + | _ -> None + ) (Queries.AD.elements a') let mustPointTo ctx exp = (* this is just to get Mval.Exp *) match mayPointTo ctx exp with diff --git a/src/analyses/extractPthread.ml b/src/analyses/extractPthread.ml index 211b88fd6e..74657c7468 100644 --- a/src/analyses/extractPthread.ml +++ b/src/analyses/extractPthread.ml @@ -877,16 +877,9 @@ module Spec : Analyses.MCPSpec = struct module ExprEval = struct let eval_ptr ctx exp = - let ad = ctx.ask (Queries.MayPointTo exp) in - if (not (Queries.AD.is_top ad)) && not (Queries.AD.is_empty ad) then - if Queries.AD.mem UnknownPtr ad - then (* UNSOUND *) - Queries.AD.remove UnknownPtr ad - |> Queries.AD.to_var_may - else - Queries.AD.to_var_may ad - else - [] + ctx.ask (Queries.MayPointTo exp) + |> Queries.AD.remove UnknownPtr + |> Queries.AD.to_var_may let eval_var ctx exp = match exp with @@ -1126,11 +1119,7 @@ module Spec : Analyses.MCPSpec = struct ad in let thread_fun = - Queries.AD.fold (fun addr vars -> - match addr with - | Queries.AD.Addr.Addr (v,_) -> v :: vars - | _ -> vars - ) funs_ad [] + Queries.AD.to_var_may funs_ad |> List.unique ~eq:(fun a b -> a.vid = b.vid) |> List.hd in @@ -1255,7 +1244,7 @@ module Spec : Analyses.MCPSpec = struct (* TODO: optimize finding *) let tasks_f = let var_in_ad ad f = Queries.AD.exists (function - | Queries.AD.Addr.Addr (ls_f,_) -> ls_f = f + | Queries.AD.Addr.Addr (ls_f,_) -> CilType.Varinfo.equal ls_f f | _ -> false ) ad in diff --git a/src/analyses/pthreadSignals.ml b/src/analyses/pthreadSignals.ml index d515820514..0b776282e8 100644 --- a/src/analyses/pthreadSignals.ml +++ b/src/analyses/pthreadSignals.ml @@ -17,10 +17,8 @@ struct module C = MustSignals module G = SetDomain.ToppedSet (MHP) (struct let topname = "All Threads" end) - let eval_exp_addr (a: Queries.ask) exp = Queries.AD.elements (a.f (Queries.MayPointTo exp)) - - let possible_vinfos a cv_arg = - List.filter_map ValueDomain.Addr.to_var_may (eval_exp_addr a cv_arg) + let possible_vinfos (a: Queries.ask) cv_arg = + Queries.AD.to_var_may (a.f (Queries.MayPointTo cv_arg)) (* transfer functions *) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index f828e17e2b..0aafbd1ad4 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -160,15 +160,8 @@ struct if Queries.AD.is_top reachable_from_args || D.is_top caller_state then [caller_state, caller_state] else - let reachable_vars = - let get_vars addr vars = - match addr with - | Queries.AD.Addr.Addr (v,_) -> v :: vars - | _ -> vars - in - Queries.AD.fold get_vars reachable_from_args [] - in - let callee_state = D.filter (fun var -> List.mem var reachable_vars) caller_state in + let reachable_vars = Queries.AD.to_var_may reachable_from_args in + let callee_state = D.filter (fun var -> List.mem var reachable_vars) caller_state in (* TODO: use AD.mem directly *) [caller_state, callee_state] )