From cb08d337d202fe2ac6154390f8973f9195c5a7ab Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 15 Sep 2023 11:03:07 +0300 Subject: [PATCH] Simplify some AD conversions, add TODOs --- src/analyses/commonPriv.ml | 2 +- src/analyses/poisonVariables.ml | 11 +++-------- src/analyses/taintPartialContexts.ml | 2 +- src/analyses/varEq.ml | 3 +-- src/cdomains/lockDomain.ml | 2 +- src/framework/constraints.ml | 2 +- 6 files changed, 8 insertions(+), 14 deletions(-) diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index 199fae98b0..7d06844c1b 100644 --- a/src/analyses/commonPriv.ml +++ b/src/analyses/commonPriv.ml @@ -128,7 +128,7 @@ struct Lockset.empty () else let ad = ask.f Queries.MustLockset in - Q.AD.fold (fun mls acc -> Lockset.add mls acc) ad (Lockset.empty ()) + 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 *) diff --git a/src/analyses/poisonVariables.ml b/src/analyses/poisonVariables.ml index ddbb6a5a40..acd687835e 100644 --- a/src/analyses/poisonVariables.ml +++ b/src/analyses/poisonVariables.ml @@ -92,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 (Queries.AD.Addr.Addr (v,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; _} -> @@ -106,9 +103,7 @@ struct ctx.local | ad -> Queries.AD.fold (fun addr vs -> - match addr with - | Queries.AD.Addr.Addr _ -> rem_mval vs addr - | _ -> vs + rem_mval vs addr ) ad ctx.local end | _ -> ctx.local diff --git a/src/analyses/taintPartialContexts.ml b/src/analyses/taintPartialContexts.ml index eaafbf01f5..feb9599977 100644 --- a/src/analyses/taintPartialContexts.ml +++ b/src/analyses/taintPartialContexts.ml @@ -113,4 +113,4 @@ let conv_varset (addr_set : Spec.D.t) : VS.t = if Spec.D.is_top addr_set then VS.top () else - VS.of_list (List.filter_map (fun addr -> Spec.D.Addr.to_var_may addr) (Spec.D.elements addr_set)) + VS.of_list (Spec.D.to_var_may addr_set) diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml index db164a313c..dcd49c9f02 100644 --- a/src/analyses/varEq.ml +++ b/src/analyses/varEq.ml @@ -441,8 +441,7 @@ struct D.top () else let taint_exp = - Queries.AD.elements tainted - |> List.filter_map Addr.to_mval + Queries.AD.to_mval tainted |> List.map Addr.Mval.to_cil_exp |> Queries.ES.of_list in diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml index 0de5afc32c..4bc97b34ab 100644 --- a/src/cdomains/lockDomain.ml +++ b/src/cdomains/lockDomain.ml @@ -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 diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 3ea62a2f4c..26fdfac606 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -755,7 +755,7 @@ struct | _ -> (* Depends on base for query. *) let ad = ctx.ask (Queries.EvalFunvar e) in - List.filter_map (fun addr -> Queries.AD.Addr.to_var addr) (Queries.AD.elements ad) + Queries.AD.to_var_may ad (* TODO: don't convert, handle UnknownPtr below *) in let one_function f = match f.vtype with