From dc0df887e22adc34ff93f170f337ddcc7b9aff19 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 29 Aug 2023 12:27:57 +0300 Subject: [PATCH 01/19] Add MustLocksetA and MustProtectedVarsA to queries --- src/domains/queries.ml | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 0388ce2995..8680103d7a 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -81,6 +81,7 @@ type _ t = | MayBePublicWithout: maybepublicwithout -> MayBool.t t | MustBeProtectedBy: mustbeprotectedby -> MustBool.t t | MustLockset: LS.t t + | MustLocksetA: AD.t t | MustBeAtomic: MustBool.t t | MustBeSingleThreaded: {since_start: bool} -> MustBool.t t | MustBeUniqueThread: MustBool.t t @@ -115,6 +116,7 @@ type _ t = | MustJoinedThreads: ConcDomain.MustThreadSet.t t | ThreadsJoinedCleanly: MustBool.t t | MustProtectedVars: mustprotectedvars -> LS.t t + | MustProtectedVarsA: mustprotectedvars -> AD.t t | Invariant: invariant_context -> Invariant.t t | InvariantGlobal: Obj.t -> Invariant.t t (** Argument must be of corresponding [Spec.V.t]. *) | WarnGlobal: Obj.t -> Unit.t t (** Argument must be of corresponding [Spec.V.t]. *) @@ -145,6 +147,7 @@ struct | ReachableFrom _ -> (module AD) | Regions _ -> (module LS) | MustLockset -> (module LS) + | MustLocksetA -> (module AD) | EvalFunvar _ -> (module LS) | ReachableUkTypes _ -> (module TS) | MayEscape _ -> (module MayBool) @@ -180,6 +183,7 @@ struct | MustJoinedThreads -> (module ConcDomain.MustThreadSet) | ThreadsJoinedCleanly -> (module MustBool) | MustProtectedVars _ -> (module LS) + | MustProtectedVarsA _ -> (module AD) | Invariant _ -> (module Invariant) | InvariantGlobal _ -> (module Invariant) | WarnGlobal _ -> (module Unit) @@ -209,6 +213,7 @@ struct | ReachableFrom _ -> AD.top () | Regions _ -> LS.top () | MustLockset -> LS.top () + | MustLocksetA -> AD.top () | EvalFunvar _ -> LS.top () | ReachableUkTypes _ -> TS.top () | MayEscape _ -> MayBool.top () @@ -244,6 +249,7 @@ struct | MustJoinedThreads -> ConcDomain.MustThreadSet.top () | ThreadsJoinedCleanly -> MustBool.top () | MustProtectedVars _ -> LS.top () + | MustProtectedVarsA _ -> AD.top () | Invariant _ -> Invariant.top () | InvariantGlobal _ -> Invariant.top () | WarnGlobal _ -> Unit.top () @@ -274,6 +280,7 @@ struct | Any (MayBePublicWithout _) -> 8 | Any (MustBeProtectedBy _) -> 9 | Any MustLockset -> 10 + | Any MustLocksetA -> 1010 | Any MustBeAtomic -> 11 | Any (MustBeSingleThreaded _)-> 12 | Any MustBeUniqueThread -> 13 @@ -299,6 +306,7 @@ struct | Any (IterSysVars _) -> 37 | Any (InvariantGlobal _) -> 38 | Any (MustProtectedVars _) -> 39 + | Any (MustProtectedVarsA _) -> 3939 | Any MayAccessed -> 40 | Any MayBeTainted -> 41 | Any (PathQuery _) -> 42 @@ -356,6 +364,7 @@ struct | Any (IterSysVars (vq1, vf1)), Any (IterSysVars (vq2, vf2)) -> VarQuery.compare vq1 vq2 (* not comparing fs *) | Any (MutexType m1), Any (MutexType m2) -> Mval.Unit.compare m1 m2 | Any (MustProtectedVars m1), Any (MustProtectedVars m2) -> compare_mustprotectedvars m1 m2 + | Any (MustProtectedVarsA m1), Any (MustProtectedVarsA m2) -> compare_mustprotectedvars m1 m2 | Any (MayBeModifiedSinceSetjmp e1), Any (MayBeModifiedSinceSetjmp e2) -> JmpBufDomain.BufferEntry.compare e1 e2 | Any (MustBeSingleThreaded {since_start=s1;}), Any (MustBeSingleThreaded {since_start=s2;}) -> Stdlib.compare s1 s2 | Any (TmpSpecial lv1), Any (TmpSpecial lv2) -> Mval.Exp.compare lv1 lv2 @@ -395,6 +404,7 @@ struct | Any (MutexType m) -> Mval.Unit.hash m | Any (InvariantGlobal vi) -> Hashtbl.hash vi | Any (MustProtectedVars m) -> hash_mustprotectedvars m + | Any (MustProtectedVarsA m) -> hash_mustprotectedvars m | Any (MayBeModifiedSinceSetjmp e) -> JmpBufDomain.BufferEntry.hash e | Any (MustBeSingleThreaded {since_start}) -> Hashtbl.hash since_start | Any (TmpSpecial lv) -> Mval.Exp.hash lv @@ -417,6 +427,7 @@ struct | Any (MayBePublicWithout x) -> Pretty.dprintf "MayBePublicWithout _" | Any (MustBeProtectedBy x) -> Pretty.dprintf "MustBeProtectedBy _" | Any MustLockset -> Pretty.dprintf "MustLockset" + | Any MustLocksetA -> Pretty.dprintf "MustLocksetA" | Any MustBeAtomic -> Pretty.dprintf "MustBeAtomic" | Any (MustBeSingleThreaded {since_start}) -> Pretty.dprintf "MustBeSingleThreaded since_start=%b" since_start | Any MustBeUniqueThread -> Pretty.dprintf "MustBeUniqueThread" @@ -445,6 +456,7 @@ struct | Any MustJoinedThreads -> Pretty.dprintf "MustJoinedThreads" | Any ThreadsJoinedCleanly -> Pretty.dprintf "ThreadsJoinedCleanly" | Any (MustProtectedVars m) -> Pretty.dprintf "MustProtectedVars _" + | Any (MustProtectedVarsA m) -> Pretty.dprintf "MustProtectedVarsA _" | Any (Invariant i) -> Pretty.dprintf "Invariant _" | Any (WarnGlobal vi) -> Pretty.dprintf "WarnGlobal _" | Any (IterSysVars _) -> Pretty.dprintf "IterSysVars _" From 326b8e66d7ed97d21ce894bf0a32612487038815 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 29 Aug 2023 12:28:42 +0300 Subject: [PATCH 02/19] Use MustLocksetA and MustProtectedVarsA in mutexAnalysis --- src/analyses/base.ml | 1 + src/analyses/commonPriv.ml | 19 +++++++++---------- src/analyses/mutexAnalysis.ml | 10 ++-------- 3 files changed, 12 insertions(+), 18 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 4183261ddb..d7c7d4429b 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2542,6 +2542,7 @@ struct | MayBePublicWithout _ | MustBeProtectedBy _ | MustLockset + | MustLocksetA | MustBeAtomic | MustBeSingleThreaded _ | MustBeUniqueThread diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index 1b92cb320d..4aca250ba5 100644 --- a/src/analyses/commonPriv.ml +++ b/src/analyses/commonPriv.ml @@ -61,12 +61,13 @@ struct 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 + Q.AD.fold (fun m acc -> + Q.AD.fold (fun l acc -> + match l with + | Q.AD.Addr.Addr (v,_) -> VS.add v acc (* always `NoOffset from mutex analysis *) + | _ -> acc + ) (ask.f (Q.MustProtectedVarsA {mutex = m; write = true})) acc + ) (ask.f Q.MustLocksetA) VS.empty |> VS.elements end @@ -126,10 +127,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.MustLocksetA in + Q.AD.fold (fun mls acc -> Lockset.add mls acc) ad (Lockset.empty ()) (* 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/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 7d8298a0a4..bc03216ba6 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -231,15 +231,9 @@ struct true else *) Mutexes.leq mutex_lockset protecting - | Queries.MustLockset -> + | Queries.MustLocksetA -> 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 From 2bf93536925839af61816451656586208012f763 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 29 Aug 2023 14:44:53 +0300 Subject: [PATCH 03/19] Use MustProtectedVarsA in mutexAnalysis --- src/analyses/mutexAnalysis.ml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index bc03216ba6..9bde708566 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -242,6 +242,11 @@ struct VarSet.fold (fun v acc -> Queries.LS.add (v, `NoOffset) acc ) protected (Queries.LS.empty ()) + | Queries.MustProtectedVarsA {mutex = m; write} -> + let protected = GProtected.get ~write Strong (G.protected (ctx.global (V.protected m))) in + VarSet.fold (fun v acc -> + Queries.AD.join (Queries.AD.of_var v) acc + ) protected (Queries.AD.empty ()) | Queries.IterSysVars (Global g, f) -> f (Obj.repr (V.protecting g)) (* TODO: something about V.protected? *) | WarnGlobal g -> From 65567a603f6b3fb8c7c869fa1bbc6f8a23d69691 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 29 Aug 2023 14:50:29 +0300 Subject: [PATCH 04/19] Remove MustLockset and MustProtectedVars from queries --- src/analyses/base.ml | 1 - src/analyses/mutexAnalysis.ml | 5 ----- src/domains/queries.ml | 16 ++-------------- 3 files changed, 2 insertions(+), 20 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index d7c7d4429b..a7330459f0 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2541,7 +2541,6 @@ struct | MayBePublic _ | MayBePublicWithout _ | MustBeProtectedBy _ - | MustLockset | MustLocksetA | MustBeAtomic | MustBeSingleThreaded _ diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 9bde708566..55172c48eb 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -237,11 +237,6 @@ struct | 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.MustProtectedVarsA {mutex = m; write} -> let protected = GProtected.get ~write Strong (G.protected (ctx.global (V.protected m))) in VarSet.fold (fun v acc -> diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 8680103d7a..a160e6dd7b 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -80,7 +80,6 @@ type _ t = | MayBePublic: maybepublic -> MayBool.t t (* old behavior with write=false *) | MayBePublicWithout: maybepublicwithout -> MayBool.t t | MustBeProtectedBy: mustbeprotectedby -> MustBool.t t - | MustLockset: LS.t t | MustLocksetA: AD.t t | MustBeAtomic: MustBool.t t | MustBeSingleThreaded: {since_start: bool} -> MustBool.t t @@ -115,7 +114,6 @@ type _ t = | CreatedThreads: ConcDomain.ThreadSet.t t | MustJoinedThreads: ConcDomain.MustThreadSet.t t | ThreadsJoinedCleanly: MustBool.t t - | MustProtectedVars: mustprotectedvars -> LS.t t | MustProtectedVarsA: mustprotectedvars -> AD.t t | Invariant: invariant_context -> Invariant.t t | InvariantGlobal: Obj.t -> Invariant.t t (** Argument must be of corresponding [Spec.V.t]. *) @@ -146,7 +144,6 @@ struct | MayPointTo _ -> (module AD) | ReachableFrom _ -> (module AD) | Regions _ -> (module LS) - | MustLockset -> (module LS) | MustLocksetA -> (module AD) | EvalFunvar _ -> (module LS) | ReachableUkTypes _ -> (module TS) @@ -182,7 +179,6 @@ struct | CreatedThreads -> (module ConcDomain.ThreadSet) | MustJoinedThreads -> (module ConcDomain.MustThreadSet) | ThreadsJoinedCleanly -> (module MustBool) - | MustProtectedVars _ -> (module LS) | MustProtectedVarsA _ -> (module AD) | Invariant _ -> (module Invariant) | InvariantGlobal _ -> (module Invariant) @@ -212,7 +208,6 @@ struct | MayPointTo _ -> AD.top () | ReachableFrom _ -> AD.top () | Regions _ -> LS.top () - | MustLockset -> LS.top () | MustLocksetA -> AD.top () | EvalFunvar _ -> LS.top () | ReachableUkTypes _ -> TS.top () @@ -248,7 +243,6 @@ struct | CreatedThreads -> ConcDomain.ThreadSet.top () | MustJoinedThreads -> ConcDomain.MustThreadSet.top () | ThreadsJoinedCleanly -> MustBool.top () - | MustProtectedVars _ -> LS.top () | MustProtectedVarsA _ -> AD.top () | Invariant _ -> Invariant.top () | InvariantGlobal _ -> Invariant.top () @@ -279,8 +273,7 @@ struct | Any (MayBePublic _) -> 7 | Any (MayBePublicWithout _) -> 8 | Any (MustBeProtectedBy _) -> 9 - | Any MustLockset -> 10 - | Any MustLocksetA -> 1010 + | Any MustLocksetA -> 10 | Any MustBeAtomic -> 11 | Any (MustBeSingleThreaded _)-> 12 | Any MustBeUniqueThread -> 13 @@ -305,8 +298,7 @@ struct | Any (Invariant _) -> 36 | Any (IterSysVars _) -> 37 | Any (InvariantGlobal _) -> 38 - | Any (MustProtectedVars _) -> 39 - | Any (MustProtectedVarsA _) -> 3939 + | Any (MustProtectedVarsA _) -> 39 | Any MayAccessed -> 40 | Any MayBeTainted -> 41 | Any (PathQuery _) -> 42 @@ -363,7 +355,6 @@ struct | Any (InvariantGlobal vi1), Any (InvariantGlobal vi2) -> Stdlib.compare (Hashtbl.hash vi1) (Hashtbl.hash vi2) | Any (IterSysVars (vq1, vf1)), Any (IterSysVars (vq2, vf2)) -> VarQuery.compare vq1 vq2 (* not comparing fs *) | Any (MutexType m1), Any (MutexType m2) -> Mval.Unit.compare m1 m2 - | Any (MustProtectedVars m1), Any (MustProtectedVars m2) -> compare_mustprotectedvars m1 m2 | Any (MustProtectedVarsA m1), Any (MustProtectedVarsA m2) -> compare_mustprotectedvars m1 m2 | Any (MayBeModifiedSinceSetjmp e1), Any (MayBeModifiedSinceSetjmp e2) -> JmpBufDomain.BufferEntry.compare e1 e2 | Any (MustBeSingleThreaded {since_start=s1;}), Any (MustBeSingleThreaded {since_start=s2;}) -> Stdlib.compare s1 s2 @@ -403,7 +394,6 @@ struct | Any (Invariant i) -> hash_invariant_context i | Any (MutexType m) -> Mval.Unit.hash m | Any (InvariantGlobal vi) -> Hashtbl.hash vi - | Any (MustProtectedVars m) -> hash_mustprotectedvars m | Any (MustProtectedVarsA m) -> hash_mustprotectedvars m | Any (MayBeModifiedSinceSetjmp e) -> JmpBufDomain.BufferEntry.hash e | Any (MustBeSingleThreaded {since_start}) -> Hashtbl.hash since_start @@ -426,7 +416,6 @@ struct | Any (MayBePublic x) -> Pretty.dprintf "MayBePublic _" | Any (MayBePublicWithout x) -> Pretty.dprintf "MayBePublicWithout _" | Any (MustBeProtectedBy x) -> Pretty.dprintf "MustBeProtectedBy _" - | Any MustLockset -> Pretty.dprintf "MustLockset" | Any MustLocksetA -> Pretty.dprintf "MustLocksetA" | Any MustBeAtomic -> Pretty.dprintf "MustBeAtomic" | Any (MustBeSingleThreaded {since_start}) -> Pretty.dprintf "MustBeSingleThreaded since_start=%b" since_start @@ -455,7 +444,6 @@ struct | Any CreatedThreads -> Pretty.dprintf "CreatedThreads" | Any MustJoinedThreads -> Pretty.dprintf "MustJoinedThreads" | Any ThreadsJoinedCleanly -> Pretty.dprintf "ThreadsJoinedCleanly" - | Any (MustProtectedVars m) -> Pretty.dprintf "MustProtectedVars _" | Any (MustProtectedVarsA m) -> Pretty.dprintf "MustProtectedVarsA _" | Any (Invariant i) -> Pretty.dprintf "Invariant _" | Any (WarnGlobal vi) -> Pretty.dprintf "WarnGlobal _" From 4bf3680a0889e97f7e1cd845241139ccc95d144a Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 29 Aug 2023 14:55:02 +0300 Subject: [PATCH 05/19] Rename MustLocksetA -> MustLockset, MustProtectedVarsA -> MustProtectedVars --- src/analyses/base.ml | 2 +- src/analyses/commonPriv.ml | 6 +++--- src/analyses/mutexAnalysis.ml | 4 ++-- src/domains/queries.ml | 24 ++++++++++++------------ 4 files changed, 18 insertions(+), 18 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index a7330459f0..4183261ddb 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2541,7 +2541,7 @@ struct | MayBePublic _ | MayBePublicWithout _ | MustBeProtectedBy _ - | MustLocksetA + | MustLockset | MustBeAtomic | MustBeSingleThreaded _ | MustBeUniqueThread diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index 4aca250ba5..199fae98b0 100644 --- a/src/analyses/commonPriv.ml +++ b/src/analyses/commonPriv.ml @@ -66,8 +66,8 @@ struct match l with | Q.AD.Addr.Addr (v,_) -> VS.add v acc (* always `NoOffset from mutex analysis *) | _ -> acc - ) (ask.f (Q.MustProtectedVarsA {mutex = m; write = true})) acc - ) (ask.f Q.MustLocksetA) VS.empty + ) (ask.f (Q.MustProtectedVars {mutex = m; write = true})) acc + ) (ask.f Q.MustLockset) VS.empty |> VS.elements end @@ -127,7 +127,7 @@ struct if !AnalysisState.global_initialization then Lockset.empty () else - let ad = ask.f Queries.MustLocksetA in + let ad = ask.f Queries.MustLockset in Q.AD.fold (fun mls acc -> Lockset.add mls acc) ad (Lockset.empty ()) (* TODO: reversed SetDomain.Hoare *) diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 55172c48eb..9cc019db76 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -231,13 +231,13 @@ struct true else *) Mutexes.leq mutex_lockset protecting - | Queries.MustLocksetA -> + | Queries.MustLockset -> let held_locks = Lockset.export_locks (Lockset.filter snd ls) in 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.MustProtectedVarsA {mutex = m; write} -> + | 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.AD.join (Queries.AD.of_var v) acc diff --git a/src/domains/queries.ml b/src/domains/queries.ml index a160e6dd7b..b10d1b673d 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -80,7 +80,7 @@ type _ t = | MayBePublic: maybepublic -> MayBool.t t (* old behavior with write=false *) | MayBePublicWithout: maybepublicwithout -> MayBool.t t | MustBeProtectedBy: mustbeprotectedby -> MustBool.t t - | MustLocksetA: AD.t t + | MustLockset: AD.t t | MustBeAtomic: MustBool.t t | MustBeSingleThreaded: {since_start: bool} -> MustBool.t t | MustBeUniqueThread: MustBool.t t @@ -114,7 +114,7 @@ type _ t = | CreatedThreads: ConcDomain.ThreadSet.t t | MustJoinedThreads: ConcDomain.MustThreadSet.t t | ThreadsJoinedCleanly: MustBool.t t - | MustProtectedVarsA: mustprotectedvars -> AD.t t + | MustProtectedVars: mustprotectedvars -> AD.t t | Invariant: invariant_context -> Invariant.t t | InvariantGlobal: Obj.t -> Invariant.t t (** Argument must be of corresponding [Spec.V.t]. *) | WarnGlobal: Obj.t -> Unit.t t (** Argument must be of corresponding [Spec.V.t]. *) @@ -144,7 +144,7 @@ struct | MayPointTo _ -> (module AD) | ReachableFrom _ -> (module AD) | Regions _ -> (module LS) - | MustLocksetA -> (module AD) + | MustLockset -> (module AD) | EvalFunvar _ -> (module LS) | ReachableUkTypes _ -> (module TS) | MayEscape _ -> (module MayBool) @@ -179,7 +179,7 @@ struct | CreatedThreads -> (module ConcDomain.ThreadSet) | MustJoinedThreads -> (module ConcDomain.MustThreadSet) | ThreadsJoinedCleanly -> (module MustBool) - | MustProtectedVarsA _ -> (module AD) + | MustProtectedVars _ -> (module AD) | Invariant _ -> (module Invariant) | InvariantGlobal _ -> (module Invariant) | WarnGlobal _ -> (module Unit) @@ -208,7 +208,7 @@ struct | MayPointTo _ -> AD.top () | ReachableFrom _ -> AD.top () | Regions _ -> LS.top () - | MustLocksetA -> AD.top () + | MustLockset -> AD.top () | EvalFunvar _ -> LS.top () | ReachableUkTypes _ -> TS.top () | MayEscape _ -> MayBool.top () @@ -243,7 +243,7 @@ struct | CreatedThreads -> ConcDomain.ThreadSet.top () | MustJoinedThreads -> ConcDomain.MustThreadSet.top () | ThreadsJoinedCleanly -> MustBool.top () - | MustProtectedVarsA _ -> AD.top () + | MustProtectedVars _ -> AD.top () | Invariant _ -> Invariant.top () | InvariantGlobal _ -> Invariant.top () | WarnGlobal _ -> Unit.top () @@ -273,7 +273,7 @@ struct | Any (MayBePublic _) -> 7 | Any (MayBePublicWithout _) -> 8 | Any (MustBeProtectedBy _) -> 9 - | Any MustLocksetA -> 10 + | Any MustLockset -> 10 | Any MustBeAtomic -> 11 | Any (MustBeSingleThreaded _)-> 12 | Any MustBeUniqueThread -> 13 @@ -298,7 +298,7 @@ struct | Any (Invariant _) -> 36 | Any (IterSysVars _) -> 37 | Any (InvariantGlobal _) -> 38 - | Any (MustProtectedVarsA _) -> 39 + | Any (MustProtectedVars _) -> 39 | Any MayAccessed -> 40 | Any MayBeTainted -> 41 | Any (PathQuery _) -> 42 @@ -355,7 +355,7 @@ struct | Any (InvariantGlobal vi1), Any (InvariantGlobal vi2) -> Stdlib.compare (Hashtbl.hash vi1) (Hashtbl.hash vi2) | Any (IterSysVars (vq1, vf1)), Any (IterSysVars (vq2, vf2)) -> VarQuery.compare vq1 vq2 (* not comparing fs *) | Any (MutexType m1), Any (MutexType m2) -> Mval.Unit.compare m1 m2 - | Any (MustProtectedVarsA m1), Any (MustProtectedVarsA m2) -> compare_mustprotectedvars m1 m2 + | Any (MustProtectedVars m1), Any (MustProtectedVars m2) -> compare_mustprotectedvars m1 m2 | Any (MayBeModifiedSinceSetjmp e1), Any (MayBeModifiedSinceSetjmp e2) -> JmpBufDomain.BufferEntry.compare e1 e2 | Any (MustBeSingleThreaded {since_start=s1;}), Any (MustBeSingleThreaded {since_start=s2;}) -> Stdlib.compare s1 s2 | Any (TmpSpecial lv1), Any (TmpSpecial lv2) -> Mval.Exp.compare lv1 lv2 @@ -394,7 +394,7 @@ struct | Any (Invariant i) -> hash_invariant_context i | Any (MutexType m) -> Mval.Unit.hash m | Any (InvariantGlobal vi) -> Hashtbl.hash vi - | Any (MustProtectedVarsA m) -> hash_mustprotectedvars m + | Any (MustProtectedVars m) -> hash_mustprotectedvars m | Any (MayBeModifiedSinceSetjmp e) -> JmpBufDomain.BufferEntry.hash e | Any (MustBeSingleThreaded {since_start}) -> Hashtbl.hash since_start | Any (TmpSpecial lv) -> Mval.Exp.hash lv @@ -416,7 +416,7 @@ struct | Any (MayBePublic x) -> Pretty.dprintf "MayBePublic _" | Any (MayBePublicWithout x) -> Pretty.dprintf "MayBePublicWithout _" | Any (MustBeProtectedBy x) -> Pretty.dprintf "MustBeProtectedBy _" - | Any MustLocksetA -> Pretty.dprintf "MustLocksetA" + | Any MustLockset -> Pretty.dprintf "MustLockset" | Any MustBeAtomic -> Pretty.dprintf "MustBeAtomic" | Any (MustBeSingleThreaded {since_start}) -> Pretty.dprintf "MustBeSingleThreaded since_start=%b" since_start | Any MustBeUniqueThread -> Pretty.dprintf "MustBeUniqueThread" @@ -444,7 +444,7 @@ struct | Any CreatedThreads -> Pretty.dprintf "CreatedThreads" | Any MustJoinedThreads -> Pretty.dprintf "MustJoinedThreads" | Any ThreadsJoinedCleanly -> Pretty.dprintf "ThreadsJoinedCleanly" - | Any (MustProtectedVarsA m) -> Pretty.dprintf "MustProtectedVarsA _" + | Any (MustProtectedVars m) -> Pretty.dprintf "MustProtectedVars _" | Any (Invariant i) -> Pretty.dprintf "Invariant _" | Any (WarnGlobal vi) -> Pretty.dprintf "WarnGlobal _" | Any (IterSysVars _) -> Pretty.dprintf "IterSysVars _" From 586a5959a6ba4090f25088c000c94a2a710611c6 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 29 Aug 2023 15:00:20 +0300 Subject: [PATCH 06/19] Add EvalFunvarA to queries --- src/domains/queries.ml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/domains/queries.ml b/src/domains/queries.ml index b10d1b673d..1f17b198b6 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -88,6 +88,7 @@ type _ t = | ThreadCreateIndexedNode: ThreadNodeLattice.t t | MayBeThreadReturn: MayBool.t t | EvalFunvar: exp -> LS.t t + | EvalFunvarA: exp -> AD.t t | EvalInt: exp -> ID.t t | EvalStr: exp -> SD.t t | EvalLength: exp -> ID.t t (* length of an array or string *) @@ -146,6 +147,7 @@ struct | Regions _ -> (module LS) | MustLockset -> (module AD) | EvalFunvar _ -> (module LS) + | EvalFunvarA _ -> (module AD) | ReachableUkTypes _ -> (module TS) | MayEscape _ -> (module MayBool) | MayBePublic _ -> (module MayBool) @@ -210,6 +212,7 @@ struct | Regions _ -> LS.top () | MustLockset -> AD.top () | EvalFunvar _ -> LS.top () + | EvalFunvarA _ -> AD.top () | ReachableUkTypes _ -> TS.top () | MayEscape _ -> MayBool.top () | MayBePublic _ -> MayBool.top () @@ -280,6 +283,7 @@ struct | Any CurrentThreadId -> 14 | Any MayBeThreadReturn -> 15 | Any (EvalFunvar _) -> 16 + | Any (EvalFunvarA _) -> 1616 | Any (EvalInt _) -> 17 | Any (EvalStr _) -> 18 | Any (EvalLength _) -> 19 @@ -330,6 +334,7 @@ struct | Any (MayBePublicWithout x1), Any (MayBePublicWithout x2) -> compare_maybepublicwithout x1 x2 | Any (MustBeProtectedBy x1), Any (MustBeProtectedBy x2) -> compare_mustbeprotectedby x1 x2 | Any (EvalFunvar e1), Any (EvalFunvar e2) -> CilType.Exp.compare e1 e2 + | Any (EvalFunvarA e1), Any (EvalFunvarA e2) -> CilType.Exp.compare e1 e2 | Any (EvalInt e1), Any (EvalInt e2) -> CilType.Exp.compare e1 e2 | Any (EvalStr e1), Any (EvalStr e2) -> CilType.Exp.compare e1 e2 | Any (EvalLength e1), Any (EvalLength e2) -> CilType.Exp.compare e1 e2 @@ -375,6 +380,7 @@ struct | Any (MayBePublicWithout x) -> hash_maybepublicwithout x | Any (MustBeProtectedBy x) -> hash_mustbeprotectedby x | Any (EvalFunvar e) -> CilType.Exp.hash e + | Any (EvalFunvarA e) -> CilType.Exp.hash e | Any (EvalInt e) -> CilType.Exp.hash e | Any (EvalStr e) -> CilType.Exp.hash e | Any (EvalLength e) -> CilType.Exp.hash e @@ -424,6 +430,7 @@ struct | Any ThreadCreateIndexedNode -> Pretty.dprintf "ThreadCreateIndexedNode" | Any MayBeThreadReturn -> Pretty.dprintf "MayBeThreadReturn" | Any (EvalFunvar e) -> Pretty.dprintf "EvalFunvar %a" CilType.Exp.pretty e + | Any (EvalFunvarA e) -> Pretty.dprintf "EvalFunvarA %a" CilType.Exp.pretty e | Any (EvalInt e) -> Pretty.dprintf "EvalInt %a" CilType.Exp.pretty e | Any (EvalStr e) -> Pretty.dprintf "EvalStr %a" CilType.Exp.pretty e | Any (EvalLength e) -> Pretty.dprintf "EvalLength %a" CilType.Exp.pretty e From f15b41fb6fe467c4b4ef113306bea23008d830a5 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 29 Aug 2023 15:08:10 +0300 Subject: [PATCH 07/19] Use EvalFunvarA in base --- src/analyses/base.ml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 4183261ddb..2272a953ca 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1207,6 +1207,11 @@ struct let fs = eval_funvar ctx e in List.fold_left (fun xs v -> Q.LS.add (v,`NoOffset) xs) (Q.LS.empty ()) fs end + | Q.EvalFunvarA e -> + begin + let fs = eval_funvar ctx e in + List.fold_left (fun ad v -> Q.AD.join (Q.AD.of_var v) ad) (Q.AD.empty ()) fs + end | Q.EvalJumpBuf e -> begin match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with | Address jmp_buf -> From bdd90b4c4f7cffa3130b126d1a7b746ee1d9d3d4 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 29 Aug 2023 15:35:27 +0300 Subject: [PATCH 08/19] Use EvalFunvarA in constraints --- src/framework/constraints.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 740d1f85a9..9bbfef9c89 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -299,12 +299,12 @@ struct let query ctx (type a) (q: a Queries.t): a Queries.result = match q with - | Queries.EvalFunvar e -> + | Queries.EvalFunvarA e -> let (d,l) = ctx.local in if leq0 l then - Queries.LS.empty () + Queries.AD.empty () else - query' ctx (Queries.EvalFunvar e) + query' ctx (Queries.EvalFunvarA e) | q -> query' ctx q end @@ -754,8 +754,8 @@ struct [v] | _ -> (* Depends on base for query. *) - let ls = ctx.ask (Queries.EvalFunvar e) in - Queries.LS.fold (fun ((x,_)) xs -> x::xs) ls [] + let ad = ctx.ask (Queries.EvalFunvarA e) in + List.filter_map (fun addr -> Queries.AD.Addr.to_var addr) (Queries.AD.elements ad) in let one_function f = match f.vtype with From e9e53a71080bcbca164906cd8bef1a1d420c5345 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 29 Aug 2023 15:39:07 +0300 Subject: [PATCH 09/19] Remove EvalFunvar queries --- src/analyses/base.ml | 5 ----- src/domains/queries.ml | 9 +-------- 2 files changed, 1 insertion(+), 13 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 2272a953ca..c272bf1a63 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1202,11 +1202,6 @@ 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 | Q.EvalFunvarA e -> begin let fs = eval_funvar ctx e in diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 1f17b198b6..648a0c561e 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -87,7 +87,6 @@ type _ t = | CurrentThreadId: ThreadIdDomain.ThreadLifted.t t | ThreadCreateIndexedNode: ThreadNodeLattice.t t | MayBeThreadReturn: MayBool.t t - | EvalFunvar: exp -> LS.t t | EvalFunvarA: exp -> AD.t t | EvalInt: exp -> ID.t t | EvalStr: exp -> SD.t t @@ -146,7 +145,6 @@ struct | ReachableFrom _ -> (module AD) | Regions _ -> (module LS) | MustLockset -> (module AD) - | EvalFunvar _ -> (module LS) | EvalFunvarA _ -> (module AD) | ReachableUkTypes _ -> (module TS) | MayEscape _ -> (module MayBool) @@ -211,7 +209,6 @@ struct | ReachableFrom _ -> AD.top () | Regions _ -> LS.top () | MustLockset -> AD.top () - | EvalFunvar _ -> LS.top () | EvalFunvarA _ -> AD.top () | ReachableUkTypes _ -> TS.top () | MayEscape _ -> MayBool.top () @@ -282,8 +279,7 @@ struct | Any MustBeUniqueThread -> 13 | Any CurrentThreadId -> 14 | Any MayBeThreadReturn -> 15 - | Any (EvalFunvar _) -> 16 - | Any (EvalFunvarA _) -> 1616 + | Any (EvalFunvarA _) -> 16 | Any (EvalInt _) -> 17 | Any (EvalStr _) -> 18 | Any (EvalLength _) -> 19 @@ -333,7 +329,6 @@ struct | Any (MayBePublic x1), Any (MayBePublic x2) -> compare_maybepublic x1 x2 | Any (MayBePublicWithout x1), Any (MayBePublicWithout x2) -> compare_maybepublicwithout x1 x2 | Any (MustBeProtectedBy x1), Any (MustBeProtectedBy x2) -> compare_mustbeprotectedby x1 x2 - | Any (EvalFunvar e1), Any (EvalFunvar e2) -> CilType.Exp.compare e1 e2 | Any (EvalFunvarA e1), Any (EvalFunvarA e2) -> CilType.Exp.compare e1 e2 | Any (EvalInt e1), Any (EvalInt e2) -> CilType.Exp.compare e1 e2 | Any (EvalStr e1), Any (EvalStr e2) -> CilType.Exp.compare e1 e2 @@ -379,7 +374,6 @@ struct | Any (MayBePublic x) -> hash_maybepublic x | Any (MayBePublicWithout x) -> hash_maybepublicwithout x | Any (MustBeProtectedBy x) -> hash_mustbeprotectedby x - | Any (EvalFunvar e) -> CilType.Exp.hash e | Any (EvalFunvarA e) -> CilType.Exp.hash e | Any (EvalInt e) -> CilType.Exp.hash e | Any (EvalStr e) -> CilType.Exp.hash e @@ -429,7 +423,6 @@ struct | Any CurrentThreadId -> Pretty.dprintf "CurrentThreadId" | Any ThreadCreateIndexedNode -> Pretty.dprintf "ThreadCreateIndexedNode" | Any MayBeThreadReturn -> Pretty.dprintf "MayBeThreadReturn" - | Any (EvalFunvar e) -> Pretty.dprintf "EvalFunvar %a" CilType.Exp.pretty e | Any (EvalFunvarA e) -> Pretty.dprintf "EvalFunvarA %a" CilType.Exp.pretty e | Any (EvalInt e) -> Pretty.dprintf "EvalInt %a" CilType.Exp.pretty e | Any (EvalStr e) -> Pretty.dprintf "EvalStr %a" CilType.Exp.pretty e From 9fef5946d61b009ea31d2090870ed73a5b8755de Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 29 Aug 2023 15:39:46 +0300 Subject: [PATCH 10/19] Rename EvalFunvarA -> EvalFunvar --- src/analyses/base.ml | 2 +- src/domains/queries.ml | 14 +++++++------- src/framework/constraints.ml | 6 +++--- 3 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index c272bf1a63..5dfbe3c64a 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1202,7 +1202,7 @@ struct let query ctx (type a) (q: a Q.t): a Q.result = match q with - | Q.EvalFunvarA e -> + | Q.EvalFunvar e -> begin let fs = eval_funvar ctx e in List.fold_left (fun ad v -> Q.AD.join (Q.AD.of_var v) ad) (Q.AD.empty ()) fs diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 648a0c561e..8626fb9d11 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -87,7 +87,7 @@ type _ t = | CurrentThreadId: ThreadIdDomain.ThreadLifted.t t | ThreadCreateIndexedNode: ThreadNodeLattice.t t | MayBeThreadReturn: MayBool.t t - | EvalFunvarA: exp -> AD.t t + | EvalFunvar: exp -> AD.t t | EvalInt: exp -> ID.t t | EvalStr: exp -> SD.t t | EvalLength: exp -> ID.t t (* length of an array or string *) @@ -145,7 +145,7 @@ struct | ReachableFrom _ -> (module AD) | Regions _ -> (module LS) | MustLockset -> (module AD) - | EvalFunvarA _ -> (module AD) + | EvalFunvar _ -> (module AD) | ReachableUkTypes _ -> (module TS) | MayEscape _ -> (module MayBool) | MayBePublic _ -> (module MayBool) @@ -209,7 +209,7 @@ struct | ReachableFrom _ -> AD.top () | Regions _ -> LS.top () | MustLockset -> AD.top () - | EvalFunvarA _ -> AD.top () + | EvalFunvar _ -> AD.top () | ReachableUkTypes _ -> TS.top () | MayEscape _ -> MayBool.top () | MayBePublic _ -> MayBool.top () @@ -279,7 +279,7 @@ struct | Any MustBeUniqueThread -> 13 | Any CurrentThreadId -> 14 | Any MayBeThreadReturn -> 15 - | Any (EvalFunvarA _) -> 16 + | Any (EvalFunvar _) -> 16 | Any (EvalInt _) -> 17 | Any (EvalStr _) -> 18 | Any (EvalLength _) -> 19 @@ -329,7 +329,7 @@ struct | Any (MayBePublic x1), Any (MayBePublic x2) -> compare_maybepublic x1 x2 | Any (MayBePublicWithout x1), Any (MayBePublicWithout x2) -> compare_maybepublicwithout x1 x2 | Any (MustBeProtectedBy x1), Any (MustBeProtectedBy x2) -> compare_mustbeprotectedby x1 x2 - | Any (EvalFunvarA e1), Any (EvalFunvarA e2) -> CilType.Exp.compare e1 e2 + | Any (EvalFunvar e1), Any (EvalFunvar e2) -> CilType.Exp.compare e1 e2 | Any (EvalInt e1), Any (EvalInt e2) -> CilType.Exp.compare e1 e2 | Any (EvalStr e1), Any (EvalStr e2) -> CilType.Exp.compare e1 e2 | Any (EvalLength e1), Any (EvalLength e2) -> CilType.Exp.compare e1 e2 @@ -374,7 +374,7 @@ struct | Any (MayBePublic x) -> hash_maybepublic x | Any (MayBePublicWithout x) -> hash_maybepublicwithout x | Any (MustBeProtectedBy x) -> hash_mustbeprotectedby x - | Any (EvalFunvarA e) -> CilType.Exp.hash e + | Any (EvalFunvar e) -> CilType.Exp.hash e | Any (EvalInt e) -> CilType.Exp.hash e | Any (EvalStr e) -> CilType.Exp.hash e | Any (EvalLength e) -> CilType.Exp.hash e @@ -423,7 +423,7 @@ struct | Any CurrentThreadId -> Pretty.dprintf "CurrentThreadId" | Any ThreadCreateIndexedNode -> Pretty.dprintf "ThreadCreateIndexedNode" | Any MayBeThreadReturn -> Pretty.dprintf "MayBeThreadReturn" - | Any (EvalFunvarA e) -> Pretty.dprintf "EvalFunvarA %a" CilType.Exp.pretty e + | Any (EvalFunvar e) -> Pretty.dprintf "EvalFunvar %a" CilType.Exp.pretty e | Any (EvalInt e) -> Pretty.dprintf "EvalInt %a" CilType.Exp.pretty e | Any (EvalStr e) -> Pretty.dprintf "EvalStr %a" CilType.Exp.pretty e | Any (EvalLength e) -> Pretty.dprintf "EvalLength %a" CilType.Exp.pretty e diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 9bbfef9c89..3ea62a2f4c 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -299,12 +299,12 @@ struct let query ctx (type a) (q: a Queries.t): a Queries.result = match q with - | Queries.EvalFunvarA e -> + | Queries.EvalFunvar e -> let (d,l) = ctx.local in if leq0 l then Queries.AD.empty () else - query' ctx (Queries.EvalFunvarA e) + query' ctx (Queries.EvalFunvar e) | q -> query' ctx q end @@ -754,7 +754,7 @@ struct [v] | _ -> (* Depends on base for query. *) - let ad = ctx.ask (Queries.EvalFunvarA e) in + let ad = ctx.ask (Queries.EvalFunvar e) in List.filter_map (fun addr -> Queries.AD.Addr.to_var addr) (Queries.AD.elements ad) in let one_function f = From 8e42121dd7a75bdc44568defb29e44dc5cec66a4 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 29 Aug 2023 15:45:30 +0300 Subject: [PATCH 11/19] Add MayBeTaintedA to queries --- src/domains/queries.ml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 8626fb9d11..2cefb3f318 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -121,6 +121,7 @@ type _ t = | IterSysVars: VarQuery.t * Obj.t VarQuery.f -> Unit.t t (** [iter_vars] for [Constraints.FromSpec]. [Obj.t] represents [Spec.V.t]. *) | MayAccessed: AccessDomain.EventSet.t t | MayBeTainted: LS.t t + | MayBeTaintedA: AD.t t | MayBeModifiedSinceSetjmp: JmpBufDomain.BufferEntry.t -> VS.t t | TmpSpecial: Mval.Exp.t -> ML.t t @@ -186,6 +187,7 @@ struct | IterSysVars _ -> (module Unit) | MayAccessed -> (module AccessDomain.EventSet) | MayBeTainted -> (module LS) + | MayBeTaintedA -> (module AD) | MayBeModifiedSinceSetjmp _ -> (module VS) | TmpSpecial _ -> (module ML) @@ -250,6 +252,7 @@ struct | IterSysVars _ -> Unit.top () | MayAccessed -> AccessDomain.EventSet.top () | MayBeTainted -> LS.top () + | MayBeTaintedA -> AD.top () | MayBeModifiedSinceSetjmp _ -> VS.top () | TmpSpecial _ -> ML.top () end @@ -301,6 +304,7 @@ struct | Any (MustProtectedVars _) -> 39 | Any MayAccessed -> 40 | Any MayBeTainted -> 41 + | Any MayBeTaintedA -> 4141 | Any (PathQuery _) -> 42 | Any DYojson -> 43 | Any (EvalValue _) -> 44 @@ -453,6 +457,7 @@ struct | Any (EvalMutexAttr a) -> Pretty.dprintf "EvalMutexAttr _" | Any MayAccessed -> Pretty.dprintf "MayAccessed" | Any MayBeTainted -> Pretty.dprintf "MayBeTainted" + | Any MayBeTaintedA -> Pretty.dprintf "MayBeTaintedA" | Any DYojson -> Pretty.dprintf "DYojson" | Any MayBeModifiedSinceSetjmp buf -> Pretty.dprintf "MayBeModifiedSinceSetjmp %a" JmpBufDomain.BufferEntry.pretty buf | Any (TmpSpecial lv) -> Pretty.dprintf "TmpSpecial %a" Mval.Exp.pretty lv From 392834b054524c2eeac202de7b7ffce375717be3 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 29 Aug 2023 17:01:14 +0300 Subject: [PATCH 12/19] Use MayBeTaintedA in base --- src/analyses/base.ml | 69 ++++++++++++++++++++++++-------------------- 1 file changed, 38 insertions(+), 31 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 5dfbe3c64a..6f0f3a099a 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2386,34 +2386,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) = @@ -2427,10 +2431,10 @@ struct (* Remove the return value as this is dealt with separately. *) 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; + let tainted = f_ask.f Q.MayBeTaintedA in + 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'; @@ -2445,7 +2449,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 } From 224615f63b07448ba45afb79f42c2d8284d4b968 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 29 Aug 2023 20:19:38 +0300 Subject: [PATCH 13/19] Use MayBeTaintedA --- src/analyses/apron/relationAnalysis.apron.ml | 2 +- src/analyses/condVars.ml | 2 +- src/analyses/modifiedSinceLongjmp.ml | 10 +++-- src/analyses/poisonVariables.ml | 18 +++++---- src/analyses/taintPartialContexts.ml | 42 ++++++++------------ src/analyses/varEq.ml | 11 +++-- src/cdomains/addressDomain.ml | 2 + 7 files changed, 46 insertions(+), 41 deletions(-) diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index ca60e5dc30..64b367be68 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -407,7 +407,7 @@ struct let arg_vars = f.sformals |> List.filter (RD.Tracked.varinfo_tracked) |> List.map RV.arg in if M.tracing then M.tracel "combine" "relation remove vars: %a\n" (docList (fun v -> Pretty.text (RD.Var.to_string v))) arg_vars; RD.remove_vars_with new_fun_rel arg_vars; (* fine to remove arg vars that also exist in caller because unify from new_rel adds them back with proper constraints *) - let tainted = f_ask.f Queries.MayBeTainted in + let tainted = f_ask.f Queries.MayBeTaintedA in let tainted_vars = TaintPartialContexts.conv_varset tainted in let new_rel = RD.keep_filter st.rel (fun var -> match RV.find_metadata var with diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml index 04246bf28a..282f5bf020 100644 --- a/src/analyses/condVars.ml +++ b/src/analyses/condVars.ml @@ -146,7 +146,7 @@ struct (* combine caller's state with globals from callee *) (* TODO (precision): globals with only global vars are kept, the rest is lost -> collect which globals are assigned to *) (* D.merge (fun k s1 s2 -> match s2 with Some ss2 when (fst k).vglob && D.only_global_exprs ss2 -> s2 | _ when (fst k).vglob -> None | _ -> s1) ctx.local au *) - let tainted = TaintPartialContexts.conv_varset (f_ask.f Queries.MayBeTainted) in + let tainted = TaintPartialContexts.conv_varset (f_ask.f Queries.MayBeTaintedA) in D.only_untainted ctx.local tainted (* tainted globals might have changed... *) let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t = diff --git a/src/analyses/modifiedSinceLongjmp.ml b/src/analyses/modifiedSinceLongjmp.ml index 0375bd3f74..3cc10196fd 100644 --- a/src/analyses/modifiedSinceLongjmp.ml +++ b/src/analyses/modifiedSinceLongjmp.ml @@ -24,10 +24,14 @@ struct not v.vglob (* *) && not (BaseUtil.is_volatile v) && v.vstorage <> Static let relevants_from_ls ls = - if Queries.LS.is_top ls then + if Queries.AD.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 ()) + Queries.AD.fold (fun addr acc -> + match addr with + | Queries.AD.Addr.Addr (v, _) when is_relevant v -> VS.add v acc + | _ -> acc + ) ls (VS.empty ()) let relevants_from_ad ad = (* TODO: what about AD with both known and unknown pointers? *) @@ -45,7 +49,7 @@ struct [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_ls (f_ask.f Queries.MayBeTaintedA) 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 = diff --git a/src/analyses/poisonVariables.ml b/src/analyses/poisonVariables.ml index f69e5b2fbc..ddbb6a5a40 100644 --- a/src/analyses/poisonVariables.ml +++ b/src/analyses/poisonVariables.ml @@ -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 *) @@ -90,7 +94,7 @@ struct | 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) + | Queries.AD.Addr.Addr (v,o) -> check_mval octx.local (Queries.AD.Addr.Addr (v,o)) | _ -> () ) ad end; @@ -103,7 +107,7 @@ struct | 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) + | Queries.AD.Addr.Addr _ -> rem_mval vs addr | _ -> vs ) ad ctx.local end diff --git a/src/analyses/taintPartialContexts.ml b/src/analyses/taintPartialContexts.ml index d4ea17d2e0..39183ef087 100644 --- a/src/analyses/taintPartialContexts.ml +++ b/src/analyses/taintPartialContexts.ml @@ -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 - | _ -> 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 _ _ = () @@ -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 @@ -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 @@ -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) + | MayBeTaintedA -> (ctx.local : Queries.AD.t) | _ -> Queries.Result.top q end @@ -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 (List.filter_map (fun addr -> Spec.D.Addr.to_var_may addr) (Spec.D.elements addr_set)) diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml index 77823d99d7..3bfd188aba 100644 --- a/src/analyses/varEq.ml +++ b/src/analyses/varEq.ml @@ -433,14 +433,19 @@ struct | false -> [ctx.local,nst] let combine_env ctx lval fexp f args fc au (f_ask: Queries.ask) = - let tainted = f_ask.f Queries.MayBeTainted in + let tainted = f_ask.f Queries.MayBeTaintedA in 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.elements tainted + |> List.filter_map Addr.to_mval + |> 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 diff --git a/src/cdomains/addressDomain.ml b/src/cdomains/addressDomain.ml index 9f6ee56cbf..5981caf9ea 100644 --- a/src/cdomains/addressDomain.ml +++ b/src/cdomains/addressDomain.ml @@ -440,4 +440,6 @@ struct let r = narrow x y in if M.tracing then M.traceu "ad" "-> %a\n" pretty r; r + + let filter f ad = fold (fun addr ad -> if f addr then add addr ad else ad) ad (empty ()) end From 26151efbaf3d2cb107a69209ca5414c96d9b1cd2 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 29 Aug 2023 20:21:09 +0300 Subject: [PATCH 14/19] Remove MayBeTainted from queries --- src/domains/queries.ml | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 2cefb3f318..65c915e472 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -120,7 +120,6 @@ type _ t = | WarnGlobal: Obj.t -> Unit.t t (** Argument must be of corresponding [Spec.V.t]. *) | IterSysVars: VarQuery.t * Obj.t VarQuery.f -> Unit.t t (** [iter_vars] for [Constraints.FromSpec]. [Obj.t] represents [Spec.V.t]. *) | MayAccessed: AccessDomain.EventSet.t t - | MayBeTainted: LS.t t | MayBeTaintedA: AD.t t | MayBeModifiedSinceSetjmp: JmpBufDomain.BufferEntry.t -> VS.t t | TmpSpecial: Mval.Exp.t -> ML.t t @@ -186,7 +185,6 @@ struct | WarnGlobal _ -> (module Unit) | IterSysVars _ -> (module Unit) | MayAccessed -> (module AccessDomain.EventSet) - | MayBeTainted -> (module LS) | MayBeTaintedA -> (module AD) | MayBeModifiedSinceSetjmp _ -> (module VS) | TmpSpecial _ -> (module ML) @@ -251,7 +249,6 @@ struct | WarnGlobal _ -> Unit.top () | IterSysVars _ -> Unit.top () | MayAccessed -> AccessDomain.EventSet.top () - | MayBeTainted -> LS.top () | MayBeTaintedA -> AD.top () | MayBeModifiedSinceSetjmp _ -> VS.top () | TmpSpecial _ -> ML.top () @@ -303,8 +300,7 @@ struct | Any (InvariantGlobal _) -> 38 | Any (MustProtectedVars _) -> 39 | Any MayAccessed -> 40 - | Any MayBeTainted -> 41 - | Any MayBeTaintedA -> 4141 + | Any MayBeTaintedA -> 41 | Any (PathQuery _) -> 42 | Any DYojson -> 43 | Any (EvalValue _) -> 44 @@ -456,7 +452,6 @@ struct | Any (MutexType (v,o)) -> Pretty.dprintf "MutexType _" | Any (EvalMutexAttr a) -> Pretty.dprintf "EvalMutexAttr _" | Any MayAccessed -> Pretty.dprintf "MayAccessed" - | Any MayBeTainted -> Pretty.dprintf "MayBeTainted" | Any MayBeTaintedA -> Pretty.dprintf "MayBeTaintedA" | Any DYojson -> Pretty.dprintf "DYojson" | Any MayBeModifiedSinceSetjmp buf -> Pretty.dprintf "MayBeModifiedSinceSetjmp %a" JmpBufDomain.BufferEntry.pretty buf From 0d3af6cfeb416e039a0058670be588bcf40a74bc Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 29 Aug 2023 20:23:02 +0300 Subject: [PATCH 15/19] Rename MayBeTaintedA -> MayBeTainted --- src/analyses/apron/relationAnalysis.apron.ml | 2 +- src/analyses/base.ml | 2 +- src/analyses/condVars.ml | 2 +- src/analyses/modifiedSinceLongjmp.ml | 2 +- src/analyses/taintPartialContexts.ml | 2 +- src/analyses/varEq.ml | 2 +- src/domains/queries.ml | 10 +++++----- 7 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index 64b367be68..ca60e5dc30 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -407,7 +407,7 @@ struct let arg_vars = f.sformals |> List.filter (RD.Tracked.varinfo_tracked) |> List.map RV.arg in if M.tracing then M.tracel "combine" "relation remove vars: %a\n" (docList (fun v -> Pretty.text (RD.Var.to_string v))) arg_vars; RD.remove_vars_with new_fun_rel arg_vars; (* fine to remove arg vars that also exist in caller because unify from new_rel adds them back with proper constraints *) - let tainted = f_ask.f Queries.MayBeTaintedA in + let tainted = f_ask.f Queries.MayBeTainted in let tainted_vars = TaintPartialContexts.conv_varset tainted in let new_rel = RD.keep_filter st.rel (fun var -> match RV.find_metadata var with diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 6f0f3a099a..24596f5072 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2431,7 +2431,7 @@ struct (* Remove the return value as this is dealt with separately. *) 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.MayBeTaintedA 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 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 AD.is_top tainted then diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml index 282f5bf020..04246bf28a 100644 --- a/src/analyses/condVars.ml +++ b/src/analyses/condVars.ml @@ -146,7 +146,7 @@ struct (* combine caller's state with globals from callee *) (* TODO (precision): globals with only global vars are kept, the rest is lost -> collect which globals are assigned to *) (* D.merge (fun k s1 s2 -> match s2 with Some ss2 when (fst k).vglob && D.only_global_exprs ss2 -> s2 | _ when (fst k).vglob -> None | _ -> s1) ctx.local au *) - let tainted = TaintPartialContexts.conv_varset (f_ask.f Queries.MayBeTaintedA) in + let tainted = TaintPartialContexts.conv_varset (f_ask.f Queries.MayBeTainted) in D.only_untainted ctx.local tainted (* tainted globals might have changed... *) let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t = diff --git a/src/analyses/modifiedSinceLongjmp.ml b/src/analyses/modifiedSinceLongjmp.ml index 3cc10196fd..fafbe54840 100644 --- a/src/analyses/modifiedSinceLongjmp.ml +++ b/src/analyses/modifiedSinceLongjmp.ml @@ -49,7 +49,7 @@ struct [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.MayBeTaintedA) in + let taintedcallee = relevants_from_ls (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 = diff --git a/src/analyses/taintPartialContexts.ml b/src/analyses/taintPartialContexts.ml index 39183ef087..660766667e 100644 --- a/src/analyses/taintPartialContexts.ml +++ b/src/analyses/taintPartialContexts.ml @@ -98,7 +98,7 @@ struct let query ctx (type a) (q: a Queries.t) : a Queries.result = match q with - | MayBeTaintedA -> (ctx.local : Queries.AD.t) + | MayBeTainted -> (ctx.local : Queries.AD.t) | _ -> Queries.Result.top q end diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml index 3bfd188aba..1159ff8b1b 100644 --- a/src/analyses/varEq.ml +++ b/src/analyses/varEq.ml @@ -433,7 +433,7 @@ struct | false -> [ctx.local,nst] let combine_env ctx lval fexp f args fc au (f_ask: Queries.ask) = - let tainted = f_ask.f Queries.MayBeTaintedA in + let tainted = f_ask.f Queries.MayBeTainted in 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!! *) diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 65c915e472..e51ee90f68 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -120,7 +120,7 @@ type _ t = | WarnGlobal: Obj.t -> Unit.t t (** Argument must be of corresponding [Spec.V.t]. *) | IterSysVars: VarQuery.t * Obj.t VarQuery.f -> Unit.t t (** [iter_vars] for [Constraints.FromSpec]. [Obj.t] represents [Spec.V.t]. *) | MayAccessed: AccessDomain.EventSet.t t - | MayBeTaintedA: AD.t t + | MayBeTainted: AD.t t | MayBeModifiedSinceSetjmp: JmpBufDomain.BufferEntry.t -> VS.t t | TmpSpecial: Mval.Exp.t -> ML.t t @@ -185,7 +185,7 @@ struct | WarnGlobal _ -> (module Unit) | IterSysVars _ -> (module Unit) | MayAccessed -> (module AccessDomain.EventSet) - | MayBeTaintedA -> (module AD) + | MayBeTainted -> (module AD) | MayBeModifiedSinceSetjmp _ -> (module VS) | TmpSpecial _ -> (module ML) @@ -249,7 +249,7 @@ struct | WarnGlobal _ -> Unit.top () | IterSysVars _ -> Unit.top () | MayAccessed -> AccessDomain.EventSet.top () - | MayBeTaintedA -> AD.top () + | MayBeTainted -> AD.top () | MayBeModifiedSinceSetjmp _ -> VS.top () | TmpSpecial _ -> ML.top () end @@ -300,7 +300,7 @@ struct | Any (InvariantGlobal _) -> 38 | Any (MustProtectedVars _) -> 39 | Any MayAccessed -> 40 - | Any MayBeTaintedA -> 41 + | Any MayBeTainted -> 41 | Any (PathQuery _) -> 42 | Any DYojson -> 43 | Any (EvalValue _) -> 44 @@ -452,7 +452,7 @@ struct | Any (MutexType (v,o)) -> Pretty.dprintf "MutexType _" | Any (EvalMutexAttr a) -> Pretty.dprintf "EvalMutexAttr _" | Any MayAccessed -> Pretty.dprintf "MayAccessed" - | Any MayBeTaintedA -> Pretty.dprintf "MayBeTaintedA" + | Any MayBeTainted -> Pretty.dprintf "MayBeTainted" | Any DYojson -> Pretty.dprintf "DYojson" | Any MayBeModifiedSinceSetjmp buf -> Pretty.dprintf "MayBeModifiedSinceSetjmp %a" JmpBufDomain.BufferEntry.pretty buf | Any (TmpSpecial lv) -> Pretty.dprintf "TmpSpecial %a" Mval.Exp.pretty lv From cb08d337d202fe2ac6154390f8973f9195c5a7ab Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 15 Sep 2023 11:03:07 +0300 Subject: [PATCH 16/19] 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 From a32be380cd024523408b4e1348eab0d65da2842c Mon Sep 17 00:00:00 2001 From: karoliineh Date: Mon, 18 Sep 2023 15:06:56 +0300 Subject: [PATCH 17/19] Use AddressDomain in eval_funvar --- src/analyses/base.ml | 28 ++++++++++------------------ 1 file changed, 10 insertions(+), 18 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 1364c009d5..912e298143 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -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 "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:Unsound "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 begin + if AD.cardinal fp = 1 then + (M.warn ~category:Unsound "Unknown call to function %a." d_exp fval;) + else + (M.warn ~category:Imprecise "Function pointer %a may contain unknown functions." d_exp fval;) + end; + fp (** Evaluate expression as address. Avoids expensive Apron EvalInt if the Int result would be useless to us anyway. *) @@ -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 ad v -> Q.AD.join (Q.AD.of_var v) ad) (Q.AD.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 -> From 3879fdc2a1f3ced2cc11c15cacd36250219b6744 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Mon, 18 Sep 2023 15:12:19 +0300 Subject: [PATCH 18/19] Use relevants_from_ad instead of relevants_from_ls --- src/analyses/modifiedSinceLongjmp.ml | 16 +++------------- 1 file changed, 3 insertions(+), 13 deletions(-) diff --git a/src/analyses/modifiedSinceLongjmp.ml b/src/analyses/modifiedSinceLongjmp.ml index fafbe54840..5dae8748cb 100644 --- a/src/analyses/modifiedSinceLongjmp.ml +++ b/src/analyses/modifiedSinceLongjmp.ml @@ -23,7 +23,8 @@ 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 = + 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 @@ -33,23 +34,12 @@ struct | _ -> acc ) ls (VS.empty ()) - let relevants_from_ad ad = - (* TODO: what about AD with both known and unknown pointers? *) - if Queries.AD.is_top ad then - VS.top () - else - Queries.AD.fold (fun addr vs -> - match addr with - | Queries.AD.Addr.Addr (v,_) -> if is_relevant v then VS.add v vs else vs - | _ -> vs - ) ad (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 = From 29179999053aa95fcdfe44b3fb83f501be9f7b07 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Mon, 18 Sep 2023 15:47:48 +0300 Subject: [PATCH 19/19] Use VS domain instead of AD for MustProtectedVars --- src/analyses/commonPriv.ml | 11 +++-------- src/analyses/mutexAnalysis.ml | 4 ++-- src/domains/queries.ml | 6 +++--- 3 files changed, 8 insertions(+), 13 deletions(-) diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index 7d06844c1b..db75455b40 100644 --- a/src/analyses/commonPriv.ml +++ b/src/analyses/commonPriv.ml @@ -60,15 +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.AD.fold (fun m acc -> - Q.AD.fold (fun l acc -> - match l with - | Q.AD.Addr.Addr (v,_) -> VS.add v acc (* always `NoOffset from mutex analysis *) - | _ -> acc - ) (ask.f (Q.MustProtectedVars {mutex = m; write = true})) acc - ) (ask.f Q.MustLockset) VS.empty - |> VS.elements + 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 = diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 9cc019db76..5a61976ef5 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -240,8 +240,8 @@ struct | 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.AD.join (Queries.AD.of_var v) acc - ) protected (Queries.AD.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 -> diff --git a/src/domains/queries.ml b/src/domains/queries.ml index e51ee90f68..3a0e493640 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -114,7 +114,7 @@ type _ t = | CreatedThreads: ConcDomain.ThreadSet.t t | MustJoinedThreads: ConcDomain.MustThreadSet.t t | ThreadsJoinedCleanly: MustBool.t t - | MustProtectedVars: mustprotectedvars -> AD.t t + | MustProtectedVars: mustprotectedvars -> VS.t t | Invariant: invariant_context -> Invariant.t t | InvariantGlobal: Obj.t -> Invariant.t t (** Argument must be of corresponding [Spec.V.t]. *) | WarnGlobal: Obj.t -> Unit.t t (** Argument must be of corresponding [Spec.V.t]. *) @@ -179,7 +179,7 @@ struct | CreatedThreads -> (module ConcDomain.ThreadSet) | MustJoinedThreads -> (module ConcDomain.MustThreadSet) | ThreadsJoinedCleanly -> (module MustBool) - | MustProtectedVars _ -> (module AD) + | MustProtectedVars _ -> (module VS) | Invariant _ -> (module Invariant) | InvariantGlobal _ -> (module Invariant) | WarnGlobal _ -> (module Unit) @@ -243,7 +243,7 @@ struct | CreatedThreads -> ConcDomain.ThreadSet.top () | MustJoinedThreads -> ConcDomain.MustThreadSet.top () | ThreadsJoinedCleanly -> MustBool.top () - | MustProtectedVars _ -> AD.top () + | MustProtectedVars _ -> VS.top () | Invariant _ -> Invariant.top () | InvariantGlobal _ -> Invariant.top () | WarnGlobal _ -> Unit.top ()