Skip to content

Commit

Permalink
Merge pull request #1340 from SchiJoha/master
Browse files Browse the repository at this point in the history
master thesis: Taming Recursion with Three Context-Sensitive Analyses (Callstring, LoopfreeCallstring, Context Gas)
  • Loading branch information
michael-schwarz authored Apr 23, 2024
2 parents db226ff + c1165e1 commit 5a389f4
Showing 65 changed files with 3,147 additions and 6 deletions.
2 changes: 1 addition & 1 deletion gobview
Submodule gobview updated 0 files
94 changes: 94 additions & 0 deletions src/analyses/callstring.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,94 @@
(**
Call String analysis [call_string] and/or Call Site analysis [call_site].
The call string limitation for both approaches can be adjusted with the "callString_length" option.
By adding new implementations of the CallstringType, additional analyses can be added.
*)

open Analyses
open GoblintCil
open GobConfig

(* Specifies the type of the call string elements *)
module type CallstringType =
sig
include CilType.S
val ana_name: string
val new_ele: fundec -> ('d,'g,'c,'v) ctx -> t option (* returns an element that should be pushed to the call string *)
end

(** Analysis with infinite call string or with limited call string (k-CFA, tracks the last k call stack elements).
With the CT argument it is possible to specify the type of the call string elements *)
module Spec (CT:CallstringType) : MCPSpec =
struct
include Analyses.IdentitySpec

(* simulates a call string (with or without limitation)*)
module CallString = struct
include Printable.PQueue (CT)

(* pushes "elem" to the call string, guarantees a depth of k if limitation is specified with "ana.context.callString_length" *)
let push callstr elem =
match elem with
| None -> callstr
| Some e ->
let new_callstr = BatDeque.cons e callstr in (* pushes new element to callstr *)
if get_int "ana.context.callString_length" < 0
then new_callstr (* infinite call string *)
else (* maximum of k elements *)
match BatDeque.size new_callstr - (get_int "ana.context.callString_length") with
| 1 -> fst @@ Option.get (BatDeque.rear new_callstr)
| x when x <= 0 -> new_callstr
| _ -> failwith "CallString Error: It shouldn't happen that more than one element must be deleted to maintain the correct height!"
end

module D = Lattice.Flat (CallString) (* should be the CallString (C=D). Since a Lattice is required, Lattice.Flat is used to fulfill the type *)
module C = CallString
module V = EmptyV
module G = Lattice.Unit

let name () = "call_"^ CT.ana_name
let startstate v = `Lifted (BatDeque.empty)
let exitstate v = `Lifted (BatDeque.empty)

let context fd x = match x with
| `Lifted x -> x
| _ -> failwith "CallString: Context error! The context cannot be derived from Top or Bottom!"

let callee_state ctx f =
let elem = CT.new_ele f ctx in (* receive element that should be added to call string *)
let new_callstr = CallString.push (context f ctx.local) elem in
`Lifted new_callstr

let enter ctx r f args = [ctx.local, callee_state ctx f]

let combine_env ctx lval fexp f args fc au f_ask = ctx.local

let threadenter ctx ~multiple lval v args = [callee_state ctx (Cilfacade.find_varinfo_fundec v)]
end

(* implementations of CallstringTypes*)
module Callstring: CallstringType = struct
include CilType.Fundec
let ana_name = "string"
let new_ele f ctx =
let f' = Node.find_fundec ctx.node in
if CilType.Fundec.equal f' dummyFunDec
then None
else Some f'
end

module Callsite: CallstringType = struct
include CilType.Stmt
let ana_name = "site"
let new_ele f ctx =
match ctx.prev_node with
| Statement stmt -> Some stmt
| _ -> None (* first statement is filtered *)
end

let _ =
(* call string approach *)
MCP.register_analysis (module Spec (Callstring) : MCPSpec); (* [call_string] *)

(* call site approach *)
MCP.register_analysis (module Spec (Callsite) : MCPSpec); (* [call_site] *)
60 changes: 60 additions & 0 deletions src/analyses/loopfreeCallstring.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,60 @@
(**
Loopfree Callstring analysis [loopfree_callstring] that reduces the call string length of the classical Call String approach for recursions
The idea is to improve the Call String analysis by representing all detected call cycle of the call string in a set
In case no call cycles appears, the call string is identical to the call string of the Call String approach
For example:
- call string [main, a, b, c, a] is represented as [main, {a, b, c}]
- call string [main, a, a, b, b, b] is represented as [main, {a}, {b}]
This approach is inspired by
@see <https://arxiv.org/abs/2301.06439> Schwarz, M., Saan, S., Seidl, H., Erhard, J., Vojdani, V. Clustered Relational Thread-Modular Abstract Interpretation with Local Traces. Appendix F.
*)
open Analyses

module Spec : MCPSpec =
struct
include Analyses.IdentitySpec

let name () = "loopfree_callstring"

module FundecSet = SetDomain.Make (CilType.Fundec)
module Either = Printable.Either (CilType.Fundec) (FundecSet)

module D = Lattice.Flat (Printable.Liszt (Either)) (* A domain element is a list containing fundecs and sets of fundecs.*)
module C = D
module V = EmptyV
module G = Lattice.Unit
let startstate v = `Lifted([])
let exitstate v = `Lifted([])

let get_list list = match list with
| `Lifted e -> e
| _ -> failwith "Error loopfreeCallstring (get_list): The list cannot be derived from Top or Bottom!"

let loop_detected f = function
(* note: a call string contains each Fundec at most once *)
| `Left ele -> CilType.Fundec.equal f ele
| `Right set -> FundecSet.mem f set

let add_to_set old = function
| `Left ele -> FundecSet.add ele old
| `Right set -> FundecSet.join old set

let rec callee_state f prev_set prev_list = function
| [] -> (`Left f)::(List.rev prev_list) (* f is not yet contained in the call string *)
| e::rem_list ->
let new_set = add_to_set prev_set e in
if loop_detected f e (* f is already present in the call string *)
then (`Right new_set)::rem_list (* combine all elements of the call cycle in a set *)
else callee_state f new_set (e::prev_list) rem_list

let callee_state f ctx = `Lifted(callee_state f (FundecSet.empty ()) [] (get_list ctx.local))

let enter ctx r f args = [ctx.local, callee_state f ctx]

let threadenter ctx ~multiple lval v args = [callee_state (Cilfacade.find_varinfo_fundec v) ctx]

let combine_env ctx lval fexp f args fc au f_ask = ctx.local
end

let _ = MCP.register_analysis (module Spec : MCPSpec)
16 changes: 12 additions & 4 deletions src/analyses/mCP.ml
Original file line number Diff line number Diff line change
@@ -36,7 +36,7 @@ struct
let name () = "MCP2"

let path_sens = ref []
let cont_inse = ref []
let act_cont_sens = ref Set.empty
let base_id = ref (-1)


@@ -80,10 +80,18 @@ struct
base_id := find_id "base";
activated := map (fun s -> s, find_spec s) xs;
path_sens := map' find_id @@ get_string_list "ana.path_sens";
cont_inse := map' find_id @@ get_string_list "ana.ctx_insens";
check_deps !activated;
activated := topo_sort_an !activated;
activated_ctx_sens := List.filter (fun (n, _) -> not (List.mem n !cont_inse)) !activated;
begin
match get_string_list "ana.ctx_sens" with
| [] -> (* use values of "ana.ctx_insens" (blacklist) *)
let cont_inse = map' find_id @@ get_string_list "ana.ctx_insens" in
activated_ctx_sens := List.filter (fun (n, _) -> not (List.mem n cont_inse)) !activated;
| sens -> (* use values of "ana.ctx_sens" (whitelist) *)
let cont_sens = map' find_id @@ sens in
activated_ctx_sens := List.filter (fun (n, _) -> List.mem n cont_sens) !activated;
end;
act_cont_sens := Set.of_list (List.map (fun (n,p) -> n) !activated_ctx_sens);
activated_path_sens := List.filter (fun (n, _) -> List.mem n !path_sens) !activated;
match marshal with
| Some marshal ->
@@ -108,7 +116,7 @@ struct
let context fd x =
let x = spec_list x in
filter_map (fun (n,(module S:MCPSpec),d) ->
if mem n !cont_inse then
if Set.is_empty !act_cont_sens || not (Set.mem n !act_cont_sens) then (*n is insensitive*)
None
else
Some (n, repr @@ S.context fd (obj d))
37 changes: 37 additions & 0 deletions src/common/domains/printable.ml
Original file line number Diff line number Diff line change
@@ -588,6 +588,43 @@ module Prod4 (Base1: S) (Base2: S) (Base3: S) (Base4: S) = struct
let arbitrary () = QCheck.quad (Base1.arbitrary ()) (Base2.arbitrary ()) (Base3.arbitrary ()) (Base4.arbitrary ())
end

module PQueue (Base: S) =
struct
type t = Base.t BatDeque.dq
include Std

let show x = "[" ^ (BatDeque.fold_right (fun a acc -> Base.show a ^ ", " ^ acc) x "]")

let pretty () x = text (show x)
let name () = Base.name () ^ "queue"

let relift x = BatDeque.map Base.relift x

let printXml f xs =
let rec loop n q =
match BatDeque.front q with
| None -> ()
| Some (x, xs) -> (BatPrintf.fprintf f "<key>%d</key>\n%a\n" n Base.printXml x;
loop (n+1) (xs))
in
BatPrintf.fprintf f "<value>\n<map>\n";
loop 0 xs;
BatPrintf.fprintf f "</map>\n</value>\n"

let to_yojson q = `List (BatDeque.to_list @@ BatDeque.map (Base.to_yojson) q)
let hash q = BatDeque.fold_left (fun acc x -> (acc + 71) * (Base.hash x)) 11 q
let equal q1 q2 = BatDeque.eq ~eq:Base.equal q1 q2
let compare q1 q2 =
match BatDeque.front q1, BatDeque.front q2 with
| None, None -> 0
| None, Some(_, _) -> -1
| Some(_, _), None -> 1
| Some(a1, q1'), Some(a2, q2') ->
let c = Base.compare a1 a2 in
if c <> 0 then c
else compare q1' q2'
end

module Liszt (Base: S) =
struct
type t = Base.t list [@@deriving eq, ord, hash, to_yojson]
21 changes: 20 additions & 1 deletion src/config/options.schema.json
Original file line number Diff line number Diff line change
@@ -356,11 +356,18 @@
},
"ctx_insens": {
"title": "ana.ctx_insens",
"description": "List of context-insensitive analyses",
"description": "List of context-insensitive analyses. This setting is ignored if `ana.ctx_sens` contains elements.",
"type": "array",
"items": { "type": "string" },
"default": [ "stack_loc", "stack_trace_set" ]
},
"ctx_sens": {
"title": "ana.ctx_sens",
"description": "List of context-sensitive analyses. In case this list is empty, `ana.ctx_insens` will be used to determine the set of context-insensitive analyses.",
"type": "array",
"items": { "type": "string" },
"default": []
},
"setjmp" : {
"title": "ana.setjmp",
"description": "Setjmp/Longjmp analysis",
@@ -970,6 +977,18 @@
"Do widening on contexts. Keeps a map of function to call state; enter will then return the widened local state for recursive calls.",
"type": "boolean",
"default": false
},
"gas_value": {
"title": "ana.context.gas_value",
"description": "Denotes the gas value x for the ContextGasLifter. Negative values deactivate the context gas, zero yields a context-insensitve analysis. If enabled, the first x recursive calls of the call stack are analyzed context-sensitively. Any calls deeper in the call stack are analyzed with the same (empty) context.",
"type": "integer",
"default": -1
},
"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.",
"type": "integer",
"default": 2
}
},
"additionalProperties": false
85 changes: 85 additions & 0 deletions src/framework/constraints.ml
Original file line number Diff line number Diff line change
@@ -497,6 +497,91 @@ struct
let event (ctx:(D.t,G.t,C.t,V.t) ctx) (e:Events.t) (octx:(D.t,G.t,C.t,V.t) ctx):D.t = lift_fun ctx D.lift S.event ((|>) (conv octx) % (|>) e) `Bot
end

module NoContext = struct let name = "no context" end
module IntConf =
struct
let n () = max_int
let names x = Format.asprintf "%d" x
end

(** Lifts a [Spec] with the context gas variable. The gas variable limits the number of context-sensitively analyzed function calls in a call stack.
For every function call the gas is reduced. If the gas is zero, the remaining function calls are analyzed without context-information *)
module ContextGasLifter (S:Spec)
: Spec with module D = Lattice.Prod (S.D) (Lattice.Chain (IntConf))
and module C = Printable.Option (S.C) (NoContext)
and module G = S.G
=
struct
include S

module Context_Gas_Prod (Base1: Lattice.S) (Base2: Lattice.S) =
struct
include Lattice.Prod (Base1) (Base2)
let printXml f (x,y) =
BatPrintf.fprintf f "<value>\n<map>\n<key>\n%s\n</key>\n%a<key>\nContext Gas Value\n</key>\n%a</map>\n</value>\n" (XmlUtil.escape (Base1.name ())) Base1.printXml x Base2.printXml y
end
module D = Context_Gas_Prod (S.D) (Lattice.Chain (IntConf)) (* Product of S.D and an integer, tracking the context gas value *)
module C = Printable.Option (S.C) (NoContext)
module G = S.G
module V = S.V
module P =
struct
include S.P
let of_elt (x, _) = of_elt x
end

(* returns context gas value of the given ctx *)
let cg_val ctx = snd ctx.local

type marshal = S.marshal
let init = S.init
let finalize = S.finalize

let name () = S.name ()^" with context gas"
let startstate v = S.startstate v, get_int "ana.context.gas_value"
let exitstate v = S.exitstate v, get_int "ana.context.gas_value"
let morphstate v (d,i) = S.morphstate v d, i

let context fd (d,i) =
(* only keep context if the context gas is greater zero *)
if i <= 0 then None else Some (S.context fd d)

let conv (ctx:(D.t,G.t,C.t,V.t) ctx): (S.D.t,G.t,S.C.t,V.t)ctx =
if (cg_val ctx <= 0)
then {ctx with local = fst ctx.local
; split = (fun d es -> ctx.split (d, cg_val ctx) es)
; context = (fun () -> ctx_failwith "no context (contextGas = 0)")}
else {ctx with local = fst ctx.local
; split = (fun d es -> ctx.split (d, cg_val ctx) es)
; context = (fun () -> Option.get (ctx.context ()))}

let enter ctx r f args =
(* callee gas = caller gas - 1 *)
let liftmap_tup = List.map (fun (x,y) -> (x, cg_val ctx), (y, max 0 (cg_val ctx - 1))) in
liftmap_tup (S.enter (conv ctx) r f args)

let threadenter ctx ~multiple lval f args =
let liftmap f = List.map (fun (x) -> (x, max 0 (cg_val ctx - 1))) f in
liftmap (S.threadenter (conv ctx) ~multiple lval f args)

let sync ctx reason = S.sync (conv ctx) reason, cg_val ctx
let query ctx q = S.query (conv ctx) q
let assign ctx lval expr = S.assign (conv ctx) lval expr, cg_val ctx
let vdecl ctx v = S.vdecl (conv ctx) v, cg_val ctx
let body ctx fundec = S.body (conv ctx) fundec, cg_val ctx
let branch ctx e tv = S.branch (conv ctx) e tv, cg_val ctx
let return ctx r f = S.return (conv ctx) r f, cg_val ctx
let asm ctx = S.asm (conv ctx), cg_val ctx
let skip ctx = S.skip (conv ctx), cg_val ctx
let special ctx r f args = S.special (conv ctx) r f args, cg_val ctx
let combine_env ctx r fe f args fc es f_ask = S.combine_env (conv ctx) r fe f args (Option.bind fc Fun.id) (fst es) f_ask, cg_val ctx
let combine_assign ctx r fe f args fc es f_ask = S.combine_assign (conv ctx) r fe f args (Option.bind fc Fun.id) (fst es) f_ask, cg_val ctx
let paths_as_set ctx = List.map (fun (x) -> (x, cg_val ctx)) @@ S.paths_as_set (conv ctx)
let threadspawn ctx ~multiple lval f args fctx = S.threadspawn (conv ctx) ~multiple lval f args (conv fctx), cg_val ctx
let event ctx e octx = S.event (conv ctx) e (conv octx), cg_val ctx
end


module type Increment =
sig
val increment: increment_data option
1 change: 1 addition & 0 deletions src/framework/control.ml
Original file line number Diff line number Diff line change
@@ -23,6 +23,7 @@ let spec_module: (module Spec) Lazy.t = lazy (
let module S1 =
(val
(module MCP.MCP2 : Spec)
|> lift (get_int "ana.context.gas_value" >= 0) (module ContextGasLifter)
|> lift true (module WidenContextLifterSide) (* option checked in functor *)
(* hashcons before witness to reduce duplicates, because witness re-uses contexts in domain and requires tag for PathSensitive3 *)
|> lift (get_bool "ana.opt.hashcons" || arg_enabled) (module HashconsContextLifter)
2 changes: 2 additions & 0 deletions src/goblint_lib.ml
Original file line number Diff line number Diff line change
@@ -151,6 +151,8 @@ module UnitAnalysis = UnitAnalysis

module Assert = Assert
module LoopTermination = LoopTermination
module Callstring = Callstring
module LoopfreeCallstring = LoopfreeCallstring
module Uninit = Uninit
module Expsplit = Expsplit
module StackTrace = StackTrace
Loading

0 comments on commit 5a389f4

Please sign in to comment.