From 6a549a25eb6983201d62aed5f89eb78c9399048a Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 23 Mar 2023 21:24:43 +0100 Subject: [PATCH 1/6] First steps towards autotuner for longjmp --- src/autoTune.ml | 92 +++++++++++++++++++++++------------- src/goblint.ml | 2 + src/util/options.schema.json | 2 +- 3 files changed, 62 insertions(+), 34 deletions(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index 32f6e33922..6e6a7b5012 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -6,6 +6,7 @@ open AutoTune0 (*Create maps that map each function to the ones called in it and the ones calling it Only considers static calls!*) module FunctionSet = Set.Make(CilType.Varinfo) +module FDSet = Set.Make(CilType.Fundec) module FunctionCallMap = Map.Make(CilType.Varinfo) let addOrCreateMap fd = function @@ -25,10 +26,11 @@ class collectFunctionCallsVisitor(callSet, calledBy, argLists, fd) = object | _ -> DoChildren end -class functionVisitor(calling, calledBy, argLists) = object +class functionVisitor(calling, calledBy, argLists, dynamicallyCalled) = object inherit nopCilVisitor method! vfunc fd = + if fd.svar.vaddrof then dynamicallyCalled := FDSet.add fd !dynamicallyCalled; let callSet = ref FunctionSet.empty in let callVisitor = new collectFunctionCallsVisitor (callSet, calledBy, argLists, fd.svar) in ignore @@ Cil.visitCilFunction callVisitor fd; @@ -40,15 +42,16 @@ let functionCallMaps = ResettableLazy.from_fun (fun () -> let calling = ref FunctionCallMap.empty in let calledBy = ref FunctionCallMap.empty in let argLists = ref FunctionCallMap.empty in - let thisVisitor = new functionVisitor(calling,calledBy, argLists) in + let dynamicallyCalled = ref FDSet.empty in + let thisVisitor = new functionVisitor(calling,calledBy, argLists, dynamicallyCalled) in visitCilFileSameGlobals thisVisitor (!Cilfacade.current_file); - !calling, !calledBy, !argLists) + !calling, !calledBy, !argLists, !dynamicallyCalled) (* Only considers static calls!*) -let calledFunctions fd = ResettableLazy.force functionCallMaps |> fun (x,_,_) -> x |> FunctionCallMap.find_opt fd |> Option.value ~default:FunctionSet.empty -let callingFunctions fd = ResettableLazy.force functionCallMaps |> fun (_,x,_) -> x |> FunctionCallMap.find_opt fd |> Option.value ~default:(FunctionSet.empty, 0) |> fst -let timesCalled fd = ResettableLazy.force functionCallMaps |> fun (_,x,_) -> x |> FunctionCallMap.find_opt fd |> Option.value ~default:(FunctionSet.empty, 0) |> snd -let functionArgs fd = ResettableLazy.force functionCallMaps |> fun (_,_,x) -> x |> FunctionCallMap.find_opt fd +let calledFunctions fd = ResettableLazy.force functionCallMaps |> fun (x,_,_,_) -> x |> FunctionCallMap.find_opt fd |> Option.value ~default:FunctionSet.empty +let callingFunctions fd = ResettableLazy.force functionCallMaps |> fun (_,x,_,_) -> x |> FunctionCallMap.find_opt fd |> Option.value ~default:(FunctionSet.empty, 0) |> fst +let timesCalled fd = ResettableLazy.force functionCallMaps |> fun (_,x,_,_) -> x |> FunctionCallMap.find_opt fd |> Option.value ~default:(FunctionSet.empty, 0) |> snd +let functionArgs fd = ResettableLazy.force functionCallMaps |> fun (_,_,x,_) -> x |> FunctionCallMap.find_opt fd let findMallocWrappers () = let isMalloc f = @@ -65,7 +68,7 @@ let findMallocWrappers () = false in ResettableLazy.force functionCallMaps - |> (fun (x,_,_) -> x) + |> (fun (x,_,_,_) -> x) |> FunctionCallMap.filter (fun _ allCalled -> FunctionSet.exists isMalloc allCalled) |> FunctionCallMap.filter (fun f _ -> timesCalled f > 10) |> FunctionCallMap.bindings @@ -126,7 +129,7 @@ let addModAttributes file = let disableIntervalContextsInRecursiveFunctions () = - ResettableLazy.force functionCallMaps |> fun (x,_,_) -> x |> FunctionCallMap.iter (fun f set -> + ResettableLazy.force functionCallMaps |> fun (x,_,_,_) -> x |> FunctionCallMap.iter (fun f set -> (*detect direct recursion and recursion with one indirection*) if FunctionSet.mem f set || (not @@ FunctionSet.disjoint (calledFunctions f) (callingFunctions f)) then ( print_endline ("function " ^ (f.vname) ^" is recursive, disable interval and interval_set contexts"); @@ -134,6 +137,33 @@ let disableIntervalContextsInRecursiveFunctions () = ) ) +let hasFunction pred = + let relevant_static var = + if LibraryFunctions.is_special var then + let desc = LibraryFunctions.find var in + GobOption.exists (fun args -> pred (desc.special args)) (functionArgs var) + else + false + in + let relevant_dynamic fd = + if LibraryFunctions.is_special fd.svar then + let desc = LibraryFunctions.find fd.svar in + (* We don't really have arguments at hand, so we cheat and just feed it its own formals *) + let args = List.map (fun x -> Lval (Var x, NoOffset)) fd.sformals in + pred (desc.special args) + else + false + in + let (_,static,_,dynamic) = ResettableLazy.force functionCallMaps in + static |> FunctionCallMap.exists (fun var _ -> relevant_static var) || + dynamic |> FDSet.exists relevant_dynamic + +let disableAnalyses anas = + List.iter (GobConfig.set_auto "ana.activated[-]") anas + +let enableAnalyses anas = + List.iter (GobConfig.set_auto "ana.activated[+]") anas + (*If only one thread is used in the program, we can disable most thread analyses*) (*The exceptions are analyses that are depended on by others: base -> mutex -> mutexEvents, access*) (*escape is also still enabled, because otherwise we get a warning*) @@ -141,31 +171,28 @@ let disableIntervalContextsInRecursiveFunctions () = let notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadid"; "threadJoins"; "threadreturn"] let reduceThreadAnalyses () = - let hasThreadCreate () = - ResettableLazy.force functionCallMaps - |> (fun (_,x,_) -> x) (*every function that is called*) - |> FunctionCallMap.exists (fun var (callers,_) -> - if LibraryFunctions.is_special var then ( - let desc = LibraryFunctions.find var in - match functionArgs var with - | None -> false; - | Some args -> - match desc.special args with - | ThreadCreate _ -> - print_endline @@ "thread created by " ^ var.vname ^ ", called by:"; - FunctionSet.iter ( fun c -> print_endline @@ " " ^ c.vname) callers; - true - | _ -> false - ) - else - false - ) + let isThreadCreate = function + | LibraryDesc.ThreadCreate _ -> true + | _ -> false in - if not @@ hasThreadCreate () then ( + let hasThreadCreate = hasFunction isThreadCreate in + if not @@ hasThreadCreate then ( print_endline @@ "no thread creation -> disabeling thread analyses \"" ^ (String.concat ", " notNeccessaryThreadAnalyses) ^ "\""; - let disableAnalysis = GobConfig.set_auto "ana.activated[-]" in - List.iter disableAnalysis notNeccessaryThreadAnalyses; + disableAnalyses notNeccessaryThreadAnalyses; + ) +(* This is run independant of the autotuner being enabled or not to be sound in the presence of setjmp/longjmp *) +(* It is done this way around to allow enabling some of these analyses also for programs without longjmp *) +let longjmpAnalyses = ["activeLongjmp"; "activeSetjmp"; "taintPartialContexts"; "modifiedSinceLongjmp"; "poisonVariables"; "expsplit"; "vla"] + +let activateLongjmpAnalysesWhenRequired () = + let isLongjmp = function + | LibraryDesc.Longjmp _ -> true + | _ -> false +in + if hasFunction isLongjmp then ( + print_endline @@ "longjmp -> enabeling longjmp analyses \"" ^ (String.concat ", " longjmpAnalyses) ^ "\""; + enableAnalyses longjmpAnalyses; ) let focusOnSpecification () = @@ -173,8 +200,7 @@ let focusOnSpecification () = | UnreachCall s -> () | NoDataRace -> (*enable all thread analyses*) print_endline @@ "Specification: NoDataRace -> enabling thread analyses \"" ^ (String.concat ", " notNeccessaryThreadAnalyses) ^ "\""; - let enableAnalysis = GobConfig.set_auto "ana.activated[+]" in - List.iter enableAnalysis notNeccessaryThreadAnalyses; + enableAnalyses notNeccessaryThreadAnalyses; | NoOverflow -> (*We focus on integer analysis*) set_bool "ana.int.def_exc" true; set_bool "ana.int.interval" true diff --git a/src/goblint.ml b/src/goblint.ml index 2b86d027e7..1aa61850f5 100644 --- a/src/goblint.ml +++ b/src/goblint.ml @@ -58,6 +58,8 @@ let main () = else None in + (* This is run independant of the autotuner being enabled or not be sound for programs with longjmp *) + AutoTune.activateLongjmpAnalysesWhenRequired (); if get_bool "ana.autotune.enabled" then AutoTune.chooseConfig file; file |> do_analyze changeInfo; do_html_output (); diff --git a/src/util/options.schema.json b/src/util/options.schema.json index 057720f776..e3673e82c8 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -332,7 +332,7 @@ "default": [ "expRelation", "base", "threadid", "threadflag", "threadreturn", "escape", "mutexEvents", "mutex", "access", "race", "mallocWrapper", "mhp", - "assert","activeLongjmp","activeSetjmp","taintPartialContexts","modifiedSinceLongjmp","poisonVariables","expsplit","vla" + "assert" ] }, "path_sens": { From 47399bf05265fe50e40a1057ed6ec7a7d589ce74 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 24 Mar 2023 12:53:23 +0100 Subject: [PATCH 2/6] Fix issue with dynamic calls --- src/autoTune.ml | 33 ++++++++++++++++++++------------- 1 file changed, 20 insertions(+), 13 deletions(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index 6e6a7b5012..cf15f18999 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -6,7 +6,6 @@ open AutoTune0 (*Create maps that map each function to the ones called in it and the ones calling it Only considers static calls!*) module FunctionSet = Set.Make(CilType.Varinfo) -module FDSet = Set.Make(CilType.Fundec) module FunctionCallMap = Map.Make(CilType.Varinfo) let addOrCreateMap fd = function @@ -29,20 +28,25 @@ end class functionVisitor(calling, calledBy, argLists, dynamicallyCalled) = object inherit nopCilVisitor + method! vglob = function + | GVarDecl (vinfo,_) -> + if vinfo.vaddrof && isFunctionType vinfo.vtype then dynamicallyCalled := FunctionSet.add vinfo !dynamicallyCalled; + DoChildren + | _ -> DoChildren + method! vfunc fd = - if fd.svar.vaddrof then dynamicallyCalled := FDSet.add fd !dynamicallyCalled; let callSet = ref FunctionSet.empty in let callVisitor = new collectFunctionCallsVisitor (callSet, calledBy, argLists, fd.svar) in ignore @@ Cil.visitCilFunction callVisitor fd; calling := FunctionCallMap.add fd.svar !callSet !calling; - SkipChildren + DoChildren end let functionCallMaps = ResettableLazy.from_fun (fun () -> let calling = ref FunctionCallMap.empty in let calledBy = ref FunctionCallMap.empty in let argLists = ref FunctionCallMap.empty in - let dynamicallyCalled = ref FDSet.empty in + let dynamicallyCalled = ref FunctionSet.empty in let thisVisitor = new functionVisitor(calling,calledBy, argLists, dynamicallyCalled) in visitCilFileSameGlobals thisVisitor (!Cilfacade.current_file); !calling, !calledBy, !argLists, !dynamicallyCalled) @@ -138,25 +142,28 @@ let disableIntervalContextsInRecursiveFunctions () = ) let hasFunction pred = - let relevant_static var = - if LibraryFunctions.is_special var then + let relevant_static var = + if LibraryFunctions.is_special var then let desc = LibraryFunctions.find var in GobOption.exists (fun args -> pred (desc.special args)) (functionArgs var) else false in - let relevant_dynamic fd = - if LibraryFunctions.is_special fd.svar then - let desc = LibraryFunctions.find fd.svar in - (* We don't really have arguments at hand, so we cheat and just feed it its own formals *) - let args = List.map (fun x -> Lval (Var x, NoOffset)) fd.sformals in - pred (desc.special args) + let relevant_dynamic var = + if LibraryFunctions.is_special var then + let desc = LibraryFunctions.find var in + (* We don't really have arguments at hand, so we cheat and just feed it a list of Cil.one of appropriate length *) + match unrollType var.vtype with + | TFun (_, args, _, _) -> + let args = BatOption.map_default (List.map (fun (x,_,_) -> Cil.one)) [] args in + pred (desc.special args) + | _ -> false else false in let (_,static,_,dynamic) = ResettableLazy.force functionCallMaps in static |> FunctionCallMap.exists (fun var _ -> relevant_static var) || - dynamic |> FDSet.exists relevant_dynamic + dynamic |> FunctionSet.exists relevant_dynamic let disableAnalyses anas = List.iter (GobConfig.set_auto "ana.activated[-]") anas From 711a3905b28386633ec718d4b746fa77b9525f8f Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 24 Mar 2023 13:02:58 +0100 Subject: [PATCH 3/6] Introduce record type to structure code --- src/autoTune.ml | 30 ++++++++++++++++++------------ 1 file changed, 18 insertions(+), 12 deletions(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index cf15f18999..9d1aaedfa1 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -42,6 +42,13 @@ class functionVisitor(calling, calledBy, argLists, dynamicallyCalled) = object DoChildren end +type functionCallMaps = { + calling: FunctionSet.t FunctionCallMap.t; + calledBy: (FunctionSet.t * int) FunctionCallMap.t; + argLists: Cil.exp list FunctionCallMap.t; + dynamicallyCalled: FunctionSet.t; +} + let functionCallMaps = ResettableLazy.from_fun (fun () -> let calling = ref FunctionCallMap.empty in let calledBy = ref FunctionCallMap.empty in @@ -49,13 +56,13 @@ let functionCallMaps = ResettableLazy.from_fun (fun () -> let dynamicallyCalled = ref FunctionSet.empty in let thisVisitor = new functionVisitor(calling,calledBy, argLists, dynamicallyCalled) in visitCilFileSameGlobals thisVisitor (!Cilfacade.current_file); - !calling, !calledBy, !argLists, !dynamicallyCalled) + {calling = !calling; calledBy = !calledBy; argLists = !argLists; dynamicallyCalled= !dynamicallyCalled}) (* Only considers static calls!*) -let calledFunctions fd = ResettableLazy.force functionCallMaps |> fun (x,_,_,_) -> x |> FunctionCallMap.find_opt fd |> Option.value ~default:FunctionSet.empty -let callingFunctions fd = ResettableLazy.force functionCallMaps |> fun (_,x,_,_) -> x |> FunctionCallMap.find_opt fd |> Option.value ~default:(FunctionSet.empty, 0) |> fst -let timesCalled fd = ResettableLazy.force functionCallMaps |> fun (_,x,_,_) -> x |> FunctionCallMap.find_opt fd |> Option.value ~default:(FunctionSet.empty, 0) |> snd -let functionArgs fd = ResettableLazy.force functionCallMaps |> fun (_,_,x,_) -> x |> FunctionCallMap.find_opt fd +let calledFunctions fd = (ResettableLazy.force functionCallMaps).calling |> FunctionCallMap.find_opt fd |> Option.value ~default:FunctionSet.empty +let callingFunctions fd = (ResettableLazy.force functionCallMaps).calledBy |> FunctionCallMap.find_opt fd |> Option.value ~default:(FunctionSet.empty, 0) |> fst +let timesCalled fd = (ResettableLazy.force functionCallMaps).calledBy |> FunctionCallMap.find_opt fd |> Option.value ~default:(FunctionSet.empty, 0) |> snd +let functionArgs fd = (ResettableLazy.force functionCallMaps).argLists |> FunctionCallMap.find_opt fd let findMallocWrappers () = let isMalloc f = @@ -71,8 +78,7 @@ let findMallocWrappers () = else false in - ResettableLazy.force functionCallMaps - |> (fun (x,_,_,_) -> x) + (ResettableLazy.force functionCallMaps).calling |> FunctionCallMap.filter (fun _ allCalled -> FunctionSet.exists isMalloc allCalled) |> FunctionCallMap.filter (fun f _ -> timesCalled f > 10) |> FunctionCallMap.bindings @@ -133,7 +139,7 @@ let addModAttributes file = let disableIntervalContextsInRecursiveFunctions () = - ResettableLazy.force functionCallMaps |> fun (x,_,_,_) -> x |> FunctionCallMap.iter (fun f set -> + (ResettableLazy.force functionCallMaps).calling |> FunctionCallMap.iter (fun f set -> (*detect direct recursion and recursion with one indirection*) if FunctionSet.mem f set || (not @@ FunctionSet.disjoint (calledFunctions f) (callingFunctions f)) then ( print_endline ("function " ^ (f.vname) ^" is recursive, disable interval and interval_set contexts"); @@ -161,9 +167,9 @@ let hasFunction pred = else false in - let (_,static,_,dynamic) = ResettableLazy.force functionCallMaps in - static |> FunctionCallMap.exists (fun var _ -> relevant_static var) || - dynamic |> FunctionSet.exists relevant_dynamic + let calls = ResettableLazy.force functionCallMaps in + calls.calledBy |> FunctionCallMap.exists (fun var _ -> relevant_static var) || + calls.dynamicallyCalled |> FunctionSet.exists relevant_dynamic let disableAnalyses anas = List.iter (GobConfig.set_auto "ana.activated[-]") anas @@ -188,7 +194,7 @@ let reduceThreadAnalyses () = disableAnalyses notNeccessaryThreadAnalyses; ) -(* This is run independant of the autotuner being enabled or not to be sound in the presence of setjmp/longjmp *) +(* This is run independent of the autotuner being enabled or not to be sound in the presence of setjmp/longjmp *) (* It is done this way around to allow enabling some of these analyses also for programs without longjmp *) let longjmpAnalyses = ["activeLongjmp"; "activeSetjmp"; "taintPartialContexts"; "modifiedSinceLongjmp"; "poisonVariables"; "expsplit"; "vla"] From 83d95df590b0279ac37f4a83d8d701b052a96bc8 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 27 Mar 2023 16:43:18 +0200 Subject: [PATCH 4/6] Fix typo Co-authored-by: Simmo Saan --- src/autoTune.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index 9d1aaedfa1..ba3258f05e 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -204,7 +204,7 @@ let activateLongjmpAnalysesWhenRequired () = | _ -> false in if hasFunction isLongjmp then ( - print_endline @@ "longjmp -> enabeling longjmp analyses \"" ^ (String.concat ", " longjmpAnalyses) ^ "\""; + print_endline @@ "longjmp -> enabling longjmp analyses \"" ^ (String.concat ", " longjmpAnalyses) ^ "\""; enableAnalyses longjmpAnalyses; ) From a160745fafd20e61566b170c45720d9004388f41 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 27 Mar 2023 16:43:32 +0200 Subject: [PATCH 5/6] Fix typo Co-authored-by: Simmo Saan --- src/autoTune.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index ba3258f05e..0149db1618 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -190,7 +190,7 @@ let reduceThreadAnalyses () = in let hasThreadCreate = hasFunction isThreadCreate in if not @@ hasThreadCreate then ( - print_endline @@ "no thread creation -> disabeling thread analyses \"" ^ (String.concat ", " notNeccessaryThreadAnalyses) ^ "\""; + print_endline @@ "no thread creation -> disabling thread analyses \"" ^ (String.concat ", " notNeccessaryThreadAnalyses) ^ "\""; disableAnalyses notNeccessaryThreadAnalyses; ) From b874f1911a33d1ca8371a7ae30cb24d5035f9b97 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 27 Mar 2023 16:48:42 +0200 Subject: [PATCH 6/6] Use `MyCFG.unknown_exp` instead of `Cil.one` --- src/autoTune.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index 0149db1618..79d85d8009 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -158,10 +158,10 @@ let hasFunction pred = let relevant_dynamic var = if LibraryFunctions.is_special var then let desc = LibraryFunctions.find var in - (* We don't really have arguments at hand, so we cheat and just feed it a list of Cil.one of appropriate length *) + (* We don't really have arguments at hand, so we cheat and just feed it a list of MyCFG.unknown_exp of appropriate length *) match unrollType var.vtype with | TFun (_, args, _, _) -> - let args = BatOption.map_default (List.map (fun (x,_,_) -> Cil.one)) [] args in + let args = BatOption.map_default (List.map (fun (x,_,_) -> MyCFG.unknown_exp)) [] args in pred (desc.special args) | _ -> false else