Skip to content
New issue

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

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

Already on GitHub? Sign in to your account

Context Gas per Function ⛽ #1570

Merged
merged 16 commits into from
Sep 23, 2024
Merged
Changes from 14 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/analyses/apron/relationAnalysis.apron.ml
Original file line number Diff line number Diff line change
@@ -772,7 +772,7 @@ struct
PCU.RH.replace results ctx.node new_value;
end;
WideningTokens.with_local_side_tokens (fun () ->
Priv.sync (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg ctx.local (reason :> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread])
Priv.sync (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg ctx.local (reason :> [`Normal | `Join | `JoinCall of CilType.Fundec.t | `Return | `Init | `Thread])
)

let init marshal =
18 changes: 9 additions & 9 deletions src/analyses/apron/relationPriv.apron.ml
Original file line number Diff line number Diff line change
@@ -36,7 +36,7 @@ module type S =
val lock: Q.ask -> (V.t -> G.t) -> relation_components_t -> LockDomain.MustLock.t -> relation_components_t
val unlock: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> LockDomain.MustLock.t -> relation_components_t

val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread] -> relation_components_t
val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> [`Normal | `Join | `JoinCall of CilType.Fundec.t | `Return | `Init | `Thread] -> relation_components_t

val escape: Node.t -> Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> EscapeDomain.EscapedVars.t -> relation_components_t
val enter_multithreaded: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> relation_components_t
@@ -113,10 +113,10 @@ struct
match reason with
| `Join when ConfCheck.branched_thread_creation () ->
branched_sync ()
| `JoinCall when ConfCheck.branched_thread_creation () ->
| `JoinCall _ when ConfCheck.branched_thread_creation () ->
branched_sync ()
| `Join
| `JoinCall
| `JoinCall _
| `Normal
| `Init
| `Thread
@@ -385,10 +385,10 @@ struct
end
| `Join when ConfCheck.branched_thread_creation () ->
branched_sync ()
| `JoinCall when ConfCheck.branched_thread_creation_at_call ask ->
| `JoinCall f when ConfCheck.branched_thread_creation_at_call ask f ->
branched_sync ()
| `Join
| `JoinCall
| `JoinCall _
| `Normal
| `Init
| `Thread ->
@@ -674,10 +674,10 @@ struct
end
| `Join when ConfCheck.branched_thread_creation () ->
branched_sync ()
| `JoinCall when ConfCheck.branched_thread_creation_at_call ask ->
| `JoinCall f when ConfCheck.branched_thread_creation_at_call ask f ->
branched_sync ()
| `Join
| `JoinCall
| `JoinCall _
| `Normal
| `Init
| `Thread ->
@@ -1230,10 +1230,10 @@ struct
| `Return -> st (* TODO: implement? *)
| `Join when ConfCheck.branched_thread_creation () ->
branched_sync ()
| `JoinCall when ConfCheck.branched_thread_creation_at_call ask ->
| `JoinCall f when ConfCheck.branched_thread_creation_at_call ask f ->
branched_sync ()
| `Join
| `JoinCall
| `JoinCall _
| `Normal
| `Init
| `Thread ->
2 changes: 1 addition & 1 deletion src/analyses/base.ml
Original file line number Diff line number Diff line change
@@ -453,7 +453,7 @@ struct
else
ctx.local

let sync ctx reason = sync' (reason :> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread]) ctx
let sync ctx reason = sync' (reason :> [`Normal | `Join | `JoinCall of CilType.Fundec.t | `Return | `Init | `Thread]) ctx

let publish_all ctx reason =
ignore (sync' reason ctx)
26 changes: 13 additions & 13 deletions src/analyses/basePriv.ml
Original file line number Diff line number Diff line change
@@ -31,7 +31,7 @@ sig
val lock: Q.ask -> (V.t -> G.t) -> BaseComponents (D).t -> LockDomain.MustLock.t -> BaseComponents (D).t
val unlock: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> LockDomain.MustLock.t -> BaseComponents (D).t

val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread] -> BaseComponents (D).t
val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> [`Normal | `Join | `JoinCall of CilType.Fundec.t | `Return | `Init | `Thread] -> BaseComponents (D).t

val escape: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> EscapeDomain.EscapedVars.t -> BaseComponents (D).t
val enter_multithreaded: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> BaseComponents (D).t
@@ -322,10 +322,10 @@ struct
match reason with
| `Join when ConfCheck.branched_thread_creation () ->
branched_sync ()
| `JoinCall when ConfCheck.branched_thread_creation_at_call ask ->
| `JoinCall f when ConfCheck.branched_thread_creation_at_call ask f ->
branched_sync ()
| `Join
| `JoinCall
| `JoinCall _
| `Return
| `Normal
| `Init
@@ -433,10 +433,10 @@ struct
match reason with
| `Join when ConfCheck.branched_thread_creation () ->
branched_sync ()
| `JoinCall when ConfCheck.branched_thread_creation_at_call ask ->
| `JoinCall f when ConfCheck.branched_thread_creation_at_call ask f ->
branched_sync ()
| `Join
| `JoinCall
| `JoinCall _
| `Return
| `Normal
| `Init
@@ -802,10 +802,10 @@ struct
match reason with
| `Join when ConfCheck.branched_thread_creation () ->
branched_sync ()
| `JoinCall when ConfCheck.branched_thread_creation_at_call ask ->
| `JoinCall f when ConfCheck.branched_thread_creation_at_call ask f ->
branched_sync ()
| `Join
| `JoinCall
| `JoinCall _
| `Return
| `Normal
| `Init
@@ -1055,7 +1055,7 @@ struct
| `Return
| `Normal
| `Join (* TODO: no problem with branched thread creation here? *)
| `JoinCall
| `JoinCall _
| `Init
| `Thread ->
st
@@ -1111,7 +1111,7 @@ struct
| `Return
| `Normal
| `Join (* TODO: no problem with branched thread creation here? *)
| `JoinCall
| `JoinCall _
| `Init
| `Thread ->
st
@@ -1183,7 +1183,7 @@ struct
| `Return
| `Normal
| `Join (* TODO: no problem with branched thread creation here? *)
| `JoinCall
| `JoinCall _
| `Init
| `Thread ->
st
@@ -1342,7 +1342,7 @@ struct
| `Return
| `Normal
| `Join (* TODO: no problem with branched thread creation here? *)
| `JoinCall
| `JoinCall _
| `Init
| `Thread ->
st
@@ -1521,7 +1521,7 @@ struct
| `Return
| `Normal
| `Join (* TODO: no problem with branched thread creation here? *)
| `JoinCall
| `JoinCall _
| `Init
| `Thread ->
st
@@ -1704,7 +1704,7 @@ struct
| `Return
| `Normal
| `Join (* TODO: no problem with branched thread creation here? *)
| `JoinCall
| `JoinCall _
| `Init
| `Thread ->
st
2 changes: 1 addition & 1 deletion src/analyses/basePriv.mli
Original file line number Diff line number Diff line change
@@ -20,7 +20,7 @@ sig
val lock: Queries.ask -> (V.t -> G.t) -> BaseDomain.BaseComponents (D).t -> LockDomain.MustLock.t -> BaseDomain.BaseComponents (D).t
val unlock: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> LockDomain.MustLock.t -> BaseDomain.BaseComponents (D).t

val sync: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread] -> BaseDomain.BaseComponents (D).t
val sync: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> [`Normal | `Join | `JoinCall of CilType.Fundec.t | `Return | `Init | `Thread] -> BaseDomain.BaseComponents (D).t

val escape: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> EscapeDomain.EscapedVars.t -> BaseDomain.BaseComponents (D).t
val enter_multithreaded: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> BaseDomain.BaseComponents (D).t
4 changes: 2 additions & 2 deletions src/analyses/commonPriv.ml
Original file line number Diff line number Diff line change
@@ -61,7 +61,7 @@ struct
true

(** Whether branched thread creation at start nodes of procedures needs to be handled by [sync `JoinCall] of privatization. *)
let branched_thread_creation_at_call (ask:Queries.ask) =
let branched_thread_creation_at_call (ask:Queries.ask) f =
let threadflag_active = List.mem "threadflag" (GobConfig.get_string_list "ana.activated") in
if threadflag_active then
let sens = GobConfig.get_string_list "ana.ctx_sens" in
@@ -74,7 +74,7 @@ struct
if not threadflag_ctx_sens then
true
else
ask.f (Queries.GasExhausted)
ask.f (Queries.GasExhausted f)
else
true
end
4 changes: 2 additions & 2 deletions src/analyses/mCP.ml
Original file line number Diff line number Diff line change
@@ -318,10 +318,10 @@ struct
f (Result.top ()) (!base_id, spec !base_id, assoc !base_id ctx.local) *)
| Queries.DYojson ->
`Lifted (D.to_yojson ctx.local)
| Queries.GasExhausted ->
| Queries.GasExhausted f ->
if (get_int "ana.context.gas_value" >= 0) then
(* There is a lifter above this that will answer it, save to ask *)
ctx.ask (Queries.GasExhausted)
ctx.ask (Queries.GasExhausted f)
else
(* Abort to avoid infinite recursion *)
false
8 changes: 8 additions & 0 deletions src/config/options.schema.json
Original file line number Diff line number Diff line change
@@ -998,6 +998,14 @@
"type": "integer",
"default": -1
},
"gas_scope": {
"title": "ana.context.gas_scope",
"description":
"Whether the gas should be 'global' (default) or per 'function'",
"type": "string",
"enum": ["global","function"],
"default": "global"
},
"callString_length": {
"title": "ana.context.callString_length",
"description": "Length of the call string that should be used as context for the call_string and/or call_site analyses. In case the value is zero, the analysis is context-insensitive. For a negative value, an infinite call string is used! For this option to have an effect, one of the analyses in `callstring.ml` must be activated.",
14 changes: 8 additions & 6 deletions src/domains/queries.ml
Original file line number Diff line number Diff line change
@@ -124,9 +124,9 @@ type _ t =
| MustTermLoop: stmt -> MustBool.t t
| MustTermAllLoops: MustBool.t t
| IsEverMultiThreaded: MayBool.t t
| TmpSpecial: Mval.Exp.t -> ML.t t
| TmpSpecial: Mval.Exp.t -> ML.t t
| MaySignedOverflow: exp -> MayBool.t t
| GasExhausted: MustBool.t t
| GasExhausted: CilType.Fundec.t -> MustBool.t t

type 'a result = 'a

@@ -197,7 +197,7 @@ struct
| IsEverMultiThreaded -> (module MayBool)
| TmpSpecial _ -> (module ML)
| MaySignedOverflow _ -> (module MayBool)
| GasExhausted -> (module MustBool)
| GasExhausted _ -> (module MustBool)

(** Get bottom result for query. *)
let bot (type a) (q: a t): a result =
@@ -267,7 +267,7 @@ struct
| IsEverMultiThreaded -> MayBool.top ()
| TmpSpecial _ -> ML.top ()
| MaySignedOverflow _ -> MayBool.top ()
| GasExhausted -> MustBool.top ()
| GasExhausted _ -> MustBool.top ()
end

(* The type any_query can't be directly defined in Any as t,
@@ -334,7 +334,7 @@ struct
| Any (TmpSpecial _) -> 56
| Any (IsAllocVar _) -> 57
| Any (MaySignedOverflow _) -> 58
| Any GasExhausted -> 59
| Any (GasExhausted _) -> 59

let rec compare a b =
let r = Stdlib.compare (order a) (order b) in
@@ -389,6 +389,7 @@ struct
| 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
| Any (MaySignedOverflow e1), Any (MaySignedOverflow e2) -> CilType.Exp.compare e1 e2
| Any (GasExhausted f1), Any (GasExhausted f2) -> CilType.Fundec.compare f1 f2
(* only argumentless queries should remain *)
| _, _ -> Stdlib.compare (order a) (order b)

@@ -431,6 +432,7 @@ struct
| Any (MustBeSingleThreaded {since_start}) -> Hashtbl.hash since_start
| Any (TmpSpecial lv) -> Mval.Exp.hash lv
| Any (MaySignedOverflow e) -> CilType.Exp.hash e
| Any (GasExhausted f) -> CilType.Fundec.hash f
(* IterSysVars: *)
(* - argument is a function and functions cannot be compared in any meaningful way. *)
(* - doesn't matter because IterSysVars is always queried from outside of the analysis, so MCP's query caching is not done for it. *)
@@ -494,7 +496,7 @@ struct
| Any IsEverMultiThreaded -> Pretty.dprintf "IsEverMultiThreaded"
| Any (TmpSpecial lv) -> Pretty.dprintf "TmpSpecial %a" Mval.Exp.pretty lv
| Any (MaySignedOverflow e) -> Pretty.dprintf "MaySignedOverflow %a" CilType.Exp.pretty e
| Any GasExhausted -> Pretty.dprintf "GasExhausted"
| Any (GasExhausted f) -> Pretty.dprintf "GasExhausted %a" CilType.Fundec.pretty f
end

let to_value_domain_ask (ask: ask) =
4 changes: 3 additions & 1 deletion src/framework/analyses.ml
Original file line number Diff line number Diff line change
@@ -208,7 +208,7 @@ sig
val context: (D.t, G.t, C.t, V.t) ctx -> fundec -> D.t -> C.t
val startcontext: unit -> C.t

val sync : (D.t, G.t, C.t, V.t) ctx -> [`Normal | `Join | `JoinCall | `Return] -> D.t
val sync : (D.t, G.t, C.t, V.t) ctx -> [`Normal | `Join | `JoinCall of CilType.Fundec.t | `Return] -> D.t
val query : (D.t, G.t, C.t, V.t) ctx -> 'a Queries.t -> 'a Queries.result

(** A transfer function which handles the assignment of a rval to a lval, i.e.,
@@ -274,6 +274,8 @@ sig
val event : (D.t, G.t, C.t, V.t) ctx -> Events.t -> (D.t, G.t, C.t, V.t) ctx -> D.t
end

module type Spec2Spec = functor (S: Spec) -> Spec

module type MCPA =
sig
include Printable.S
Loading