diff --git a/docs/user-guide/annotating.md b/docs/user-guide/annotating.md index 4fd80a4bd9..74e85a4a56 100644 --- a/docs/user-guide/annotating.md +++ b/docs/user-guide/annotating.md @@ -26,6 +26,30 @@ The following string arguments are supported: 4. `apron.context`/`apron.no-context` to override the `ana.apron.context` option. 5. `widen`/`no-widen` to override the `ana.context.widen` option. +### Apron attributes +The Apron library can be set to only track variables with the attribute `goblint_apron_track` + +### Array attributes +Arrays can be annotated with the domain that should be used for it ("unroll", "partitioned", or "trivial"): + +```c +int x[4] __attribute__((goblint_array_domain("unroll"))); +__attribute__((goblint_array_domain("trivial"))) int x[4]; + +struct array { + int arr[5] __attribute__((goblint_array_domain("partitioned"))); +}; +``` +It is also possible to annotate a type, so that all arrays of this type without an own attribute will use this one: + +```c +typedef int unrollInt __attribute__((goblint_array_domain("trivial"))); +unrollInt x[4]; +``` + +One can also annotate pointer parameters. Inside the function of the parameter, Goblint tries to use the annotated domain for the arrays pointed at by that pointer. This is not guaranteed to work, as following the pointers is done only in the first analyzed function context. + + ## Functions Goblint-specific functions can be called in the code, where they assist the analyzer but have no runtime effect. diff --git a/src/analyses/apron/apronAnalysis.apron.ml b/src/analyses/apron/apronAnalysis.apron.ml index 8b6ecb61a3..4592d36ccd 100644 --- a/src/analyses/apron/apronAnalysis.apron.ml +++ b/src/analyses/apron/apronAnalysis.apron.ml @@ -147,6 +147,7 @@ struct ) else ( let v_out = Goblintutil.create_var @@ makeVarinfo false (v.vname ^ "#out") v.vtype in (* temporary local g#out for global g *) + v_out.vattr <- v.vattr; (*copy the attributes because the tracking may depend on them. Otherwise an assertion fails *) let st = {st with apr = AD.add_vars st.apr [V.local v_out]} in (* add temporary g#out *) let st' = {st with apr = f st v_out} in (* g#out = e; *) if M.tracing then M.trace "apron" "write_global %a %a\n" d_varinfo v d_varinfo v_out; diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 2fec3d7500..5dec7b8a96 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -87,14 +87,50 @@ struct let is_privglob v = GobConfig.get_bool "annotation.int.privglobs" && v.vglob - let project_val p_opt value is_glob = - match GobConfig.get_bool "annotation.int.enabled", is_glob, p_opt with - | true, true, _ -> VD.project PU.max_int_precision value - | true, false, Some p -> VD.project p value - | _ -> value + (*This is a bit of a hack to be able to change array domains if a pointer to an array is given as an argument*) + (*We have to prevent different domains to be used at the same time for the same array*) + (*After a function call, the domain has to be the same as before and we can not depend on the pointers staying the same*) + (*-> we determine the arrays a pointer can point to once at the beginning of a function*) + (*There surely is a better way, because this means that often the wrong one gets chosen*) + module VarH = Hashtbl.Make(CilType.Varinfo) + module VarMap = Map.Make(CilType.Varinfo) + let array_map = VarH.create 20 + + let add_to_array_map fundec arguments = + let rec pointedArrayMap = function + | [] -> VarMap.empty + | (info,value)::xs -> ( + match value with + | `Address t when hasAttribute "goblint_array_domain" info.vattr -> ( + let possibleVars = PreValueDomain.AD.to_var_may t in + List.fold_left (fun map arr -> VarMap.add arr (info.vattr) map) (pointedArrayMap xs) @@ List.filter (fun info -> isArrayType info.vtype) possibleVars + ) + | _ -> pointedArrayMap xs + ) + in + match VarH.find_option array_map fundec.svar with + | Some _ -> () (*We already have something -> do not change it*) + | None -> VarH.add array_map fundec.svar (pointedArrayMap arguments) + + let attributes_varinfo info fundec = + let map = VarH.find array_map fundec.svar in + match VarMap.find_opt info map with + | Some attr -> Some (attr, typeAttrs (info.vtype)) (*if the function has a different domain for this array, use it*) + | None -> Some (info.vattr, typeAttrs (info.vtype)) + + let project_val ask array_attr p_opt value is_glob = + let p = if GobConfig.get_bool "annotation.int.enabled" then ( + if is_glob then + Some PU.max_int_precision + else p_opt + ) else None + in + let a = if GobConfig.get_bool "annotation.goblint_array_domain" then array_attr else None in + VD.project ask p a value - let project p_opt cpa = - CPA.mapi (fun varinfo value -> project_val p_opt value (is_privglob varinfo)) cpa + let project ask p_opt cpa fundec = + CPA.mapi (fun varinfo value -> project_val ask (attributes_varinfo varinfo fundec) p_opt value (is_privglob varinfo)) + cpa (************************************************************************** @@ -120,7 +156,8 @@ struct Priv.init () let finalize () = - Priv.finalize () + Priv.finalize (); + VarH.clear array_map (************************************************************************** * Abstract evaluation functions @@ -1298,7 +1335,7 @@ struct let update_variable variable typ value cpa = if ((get_bool "exp.volatiles_are_top") && (is_always_unknown variable)) then - CPA.add variable (VD.top_value typ) cpa + CPA.add variable (VD.top_value ~varAttr:variable.vattr typ) cpa else CPA.add variable value cpa @@ -1355,8 +1392,8 @@ struct lval_type in let update_offset old_value = - (* Projection to highest Precision *) - let projected_value = project_val None value (is_global a x) in + (* Projection globals to highest Precision *) + let projected_value = project_val a None None value (is_global a x) in let new_value = VD.update_offset a old_value offs projected_value lval_raw ((Var x), cil_offset) t in if WeakUpdates.mem x st.weak then VD.join old_value new_value @@ -1384,7 +1421,7 @@ struct The case when invariant = true requires the old_value to be sound for the meet. Allocated blocks are representend by Blobs with additional information, so they need to be looked-up. *) let old_value = if not invariant && Cil.isIntegralType x.vtype && not (a.f (IsHeapVar x)) && offs = `NoOffset then begin - VD.bot_value lval_type + VD.bot_value ~varAttr:x.vattr lval_type end else Priv.read_global a priv_getg st x in @@ -2166,7 +2203,7 @@ struct begin match Addr.to_var_offset (AD.choose lval_val) with | Some (x,offs) -> let t = v.vtype in - let iv = VD.bot_value t in (* correct bottom value for top level variable *) + let iv = VD.bot_value ~varAttr:v.vattr t in (* correct bottom value for top level variable *) if M.tracing then M.tracel "set" "init bot value: %a\n" VD.pretty iv; let nv = VD.update_offset (Analyses.ask_of_ctx ctx) iv offs rval_val (Some (Lval lval)) lval t in (* do desired update to value *) set_savetop ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local (AD.from_var v) lval_t nv ~lval_raw:lval ~rval_raw:rval (* set top-level variable to updated value *) @@ -2227,7 +2264,7 @@ struct let body ctx f = (* First we create a variable-initvalue pair for each variable *) - let init_var v = (AD.from_var v, v.vtype, VD.init_value v.vtype) in + let init_var v = (AD.from_var v, v.vtype, VD.init_value ~varAttr:v.vattr v.vtype) in (* Apply it to all the locals and then assign them all *) let inits = List.map init_var f.slocals in set_many ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local inits @@ -2350,6 +2387,7 @@ struct in (* Assign parameters to arguments *) let pa = GobList.combine_short fundec.sformals vals in (* TODO: is it right to ignore missing formals/args? *) + add_to_array_map fundec pa; let new_cpa = CPA.add_list pa st'.cpa in (* List of reachable variables *) let reachable = List.concat_map AD.to_var_may (reachable_vars (Analyses.ask_of_ctx ctx) (get_ptrs vals) ctx.global st) in @@ -2358,7 +2396,7 @@ struct (* Projection to Precision of the Callee *) let p = PU.int_precision_from_fundec fundec in - let new_cpa = project (Some p) new_cpa in + let new_cpa = project (Analyses.ask_of_ctx ctx) (Some p) new_cpa fundec in (* Identify locals of this fundec for which an outer copy (from a call down the callstack) is reachable *) let reachable_other_copies = List.filter (fun v -> match Cilfacade.find_scope_fundec v with Some scope -> CilType.Fundec.equal scope fundec | None -> false) reachable in @@ -2720,9 +2758,13 @@ struct let nst = add_globals st fun_st in (* Projection to Precision of the Caller *) - let p = PrecisionUtil.int_precision_from_node () in (* Since f is the fundec of the Callee we have to get the fundec of the current Node instead *) - let return_val = project_val (Some p) return_val (is_privglob (return_varinfo ())) in - let cpa' = project (Some p) nst.cpa in + let p = PrecisionUtil.int_precision_from_node ()in (* Since f is the fundec of the Callee we have to get the fundec of the current Node instead *) + let callerFundec = match !MyCFG.current_node with + | Some n -> Node.find_fundec n + | None -> failwith "callerfundec not found" + in + let return_val = project_val (Analyses.ask_of_ctx ctx) (attributes_varinfo (return_varinfo ()) callerFundec) (Some p) return_val (is_privglob (return_varinfo ())) in + let cpa' = project (Analyses.ask_of_ctx ctx) (Some p) nst.cpa callerFundec in let st = { nst with cpa = cpa'; weak = st.weak } in (* keep weak from caller *) match lval with diff --git a/src/autoTune.ml b/src/autoTune.ml new file mode 100644 index 0000000000..182153279a --- /dev/null +++ b/src/autoTune.ml @@ -0,0 +1,431 @@ +open GobConfig +open GoblintCil +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 FunctionCallMap = Map.Make(CilType.Varinfo) + +let addOrCreateMap fd = function + | Some (set, i) -> Some (FunctionSet.add fd set, i+1) + | None -> Some (FunctionSet.singleton fd, 1) + +class collectFunctionCallsVisitor(callSet, calledBy, argLists, fd) = object + inherit nopCilVisitor + + method! vinst = function + | Call (_,Lval ((Var info), NoOffset),args,_,_)-> + callSet := FunctionSet.add info !callSet; + calledBy := FunctionCallMap.update info (addOrCreateMap fd) !calledBy; + (*We collect the argument list so we can use LibraryFunctions.find to classify functions*) + argLists := FunctionCallMap.add info args !argLists; + DoChildren + | _ -> DoChildren +end + +class functionVisitor(calling, calledBy, argLists) = object + inherit nopCilVisitor + + method! vfunc fd = + 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 +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 thisVisitor = new functionVisitor(calling,calledBy, argLists) in + visitCilFileSameGlobals thisVisitor (!Cilfacade.current_file); + !calling, !calledBy, !argLists) + +(* 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 findMallocWrappers () = + let isMalloc f = + let desc = LibraryFunctions.find f in + match (functionArgs f) with + | None -> false + | Some args -> + match desc.special args with + | Malloc _ -> true + | _ -> false + in + ResettableLazy.force functionCallMaps + |> (fun (x,_,_) -> x) + |> FunctionCallMap.filter (fun _ allCalled -> FunctionSet.exists isMalloc allCalled) + |> FunctionCallMap.filter (fun f _ -> timesCalled f > 10) + |> FunctionCallMap.bindings + |> List.map (fun (v,_) -> v.vname) + |> List.iter (fun n -> print_endline ("malloc wrapper: " ^ n); GobConfig.set_auto "ana.malloc.wrappers[+]" n) + + +(*Functions for determining if the congruence analysis should be enabled *) +let isExtern = function + | Extern -> true + | _ -> false + +let rec setCongruenceRecursive fd depth neigbourFunction = + if depth >= 0 then ( + fd.svar.vattr <- addAttributes (fd.svar.vattr) [Attr ("goblint_precision",[AStr "congruence"])]; + FunctionSet.iter + (fun vinfo -> + print_endline (" " ^ vinfo.vname); + setCongruenceRecursive (Cilfacade.find_varinfo_fundec vinfo) (depth -1) neigbourFunction + ) + (FunctionSet.filter (*for extern and builtin functions there is no function definition in CIL*) + (fun x -> not (isExtern x.vstorage || String.starts_with ~prefix:"__builtin" x.vname)) + (neigbourFunction fd.svar) + ) + ; + ) + +exception ModFound +class modVisitor = object + inherit nopCilVisitor + + method! vexpr = function + | BinOp (Mod,_,_,_) -> + raise ModFound; + | _ -> DoChildren +end + +class modFunctionAnnotatorVisitor = object + inherit nopCilVisitor + + method! vfunc fd = + let thisVisitor = new modVisitor in + try ignore (visitCilFunction thisVisitor fd) with + | ModFound -> + print_endline ("function " ^ (CilType.Fundec.show fd) ^" uses mod, enable congruence domain recursively for:"); + print_endline (" \"down\":"); + setCongruenceRecursive fd 6 calledFunctions; + print_endline (" \"up\":"); + setCongruenceRecursive fd 3 callingFunctions; + ; + SkipChildren +end + +let addModAttributes file = + set_bool "annotation.int.enabled" true; + let thisVisitor = new modFunctionAnnotatorVisitor in + ignore (visitCilFileSameGlobals thisVisitor file) + + +let disableIntervalContextsInRecursiveFunctions () = + 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 context"); + f.vattr <- addAttributes (f.vattr) [Attr ("goblint_context",[AStr "base.no-interval"])]; + ) + ) + +(*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*) +(*does not consider dynamic calls!*) + +let notNeccessaryThreadAnalyses = ["deadlock"; "maylocks"; "symb_locks"; "thread"; "threadflag"; "threadid"; "threadJoins"; "threadreturn"] +let reduceThreadAnalyses () = + let hasThreadCreate () = + ResettableLazy.force functionCallMaps + |> fun (_,x,_) -> x (*every function that is called*) + |> FunctionCallMap.exists + (fun var (callers,_) -> + 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; + ) + 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; + + ) + +let focusOnSpecification () = + match Svcomp.Specification.of_option () with + | UnreachCall s -> () + | NoDataRace -> (*enable all thread analyses*) + print_endline @@ "Specification: NoDataRace -> enabeling thread analyses \"" ^ (String.concat ", " notNeccessaryThreadAnalyses) ^ "\""; + let enableAnalysis = GobConfig.set_auto "ana.activated[+]" in + List.iter enableAnalysis notNeccessaryThreadAnalyses; + | NoOverflow -> (*We focus on integer analysis*) + set_bool "ana.int.def_exc" true; + set_bool "ana.int.interval" true + +(*Detect enumerations and enable the "ana.int.enums" option*) +exception EnumFound +class enumVisitor = object + inherit nopCilVisitor + + method! vglob = function + | GEnumTag _ + | GEnumTagDecl _ -> + raise EnumFound; + | _ -> SkipChildren; +end + +let hasEnums file = + let thisVisitor = new enumVisitor in + try + ignore (visitCilFileSameGlobals thisVisitor file); + false; + with EnumFound -> true + + +class addTypeAttributeVisitor = object + inherit nopCilVisitor + + (*large arrays -> partitioned*) + (*because unroll only is usefull if most values are actually unrolled*) + method! vvdec info = + (if is_large_array info.vtype && not @@ hasAttribute "goblint_array_domain" (typeAttrs info.vtype) then + info.vattr <- addAttribute (Attr ("goblint_array_domain", [AStr "partitioned"])) info.vattr); + DoChildren + + (*Set arrays with important types for thread analysis to unroll*) + method! vtype typ = + let is_important_type (t: typ): bool = match t with + | TNamed (info, attr) -> List.mem info.tname ["pthread_mutex_t"; "spinlock_t"; "pthread_t"] + | TInt (IInt, attr) -> hasAttribute "mutex" attr + | _ -> false + in + if is_important_type typ && not @@ hasAttribute "goblint_array_domain" (typeAttrs typ) then + ChangeTo (typeAddAttributes [Attr ("goblint_array_domain", [AStr "unroll"])] typ) + else SkipChildren +end + +let selectArrayDomains file = + set_bool "annotation.goblint_array_domain" true; + let thisVisitor = new addTypeAttributeVisitor in + ignore (visitCilFileSameGlobals thisVisitor file) +(*small unrolled loops also set domain of accessed arrays to unroll, at the point where loops are unrolled*) + + +(*option that can be selected based on value/cost*) +type option = { + value:int; + cost:int; + activate: unit -> unit +} + +(*Option for activating the octagon apron domain on selected vars*) +module VariableMap = Map.Make(CilType.Varinfo) +module VariableSet = Set.Make(CilType.Varinfo) + +let isComparison = function + | Lt | Gt | Le | Ge | Ne | Eq -> true + | _ -> false + +let rec extractVar = function + | UnOp (Neg, e, _) -> extractVar e + | Lval ((Var info),_) -> Some info + | _ -> None + +let extractOctagonVars = function + | BinOp (PlusA, e1,e2, (TInt _)) + | BinOp (MinusA, e1,e2, (TInt _)) -> ( + match extractVar e1, extractVar e2 with + | Some a, Some b -> Some (Either.Left (a,b)) + | Some a, None + | None, Some a -> if isConstant e1 then Some (Either.Right a) else None + | _,_ -> None + ) + | _ -> None + +let addOrCreateVarMapping varMap key v globals = if key.vglob = globals then varMap := + if VariableMap.mem key !varMap then + let old = VariableMap.find key !varMap in + VariableMap.add key (old + v) !varMap + else + VariableMap.add key v !varMap + +let handle varMap v globals = function + | Some (Either.Left (a,b)) -> + addOrCreateVarMapping varMap a v globals; + addOrCreateVarMapping varMap b v globals; + | Some (Either.Right a) -> addOrCreateVarMapping varMap a v globals; + | None -> () + +class octagonVariableVisitor(varMap, globals) = object + inherit nopCilVisitor + + method! vexpr = function + (*an expression of type +/- a +/- b where a,b are either variables or constants*) + | BinOp (op, e1,e2, (TInt _)) when isComparison op -> ( + handle varMap 5 globals (extractOctagonVars e1) ; + handle varMap 5 globals (extractOctagonVars e2) ; + DoChildren + ) + | Lval ((Var info),_) -> handle varMap 1 globals (Some (Either.Right info)) ; SkipChildren + (*Traverse down only operations fitting for linear equations*) + | UnOp (Neg, _,_) + | BinOp (PlusA,_,_,_) + | BinOp (MinusA,_,_,_) + | BinOp (Mult,_,_,_) + | BinOp (LAnd,_,_,_) + | BinOp (LOr,_,_,_) -> DoChildren + | _ -> SkipChildren +end + +let topVars n varMap= + let compareValueDesc = (fun (_,v1) (_,v2) -> - (compare v1 v2)) in + varMap + |> VariableMap.bindings + |> List.sort compareValueDesc + |> BatList.take n + |> List.map fst + +class octagonFunctionVisitor(list, amount) = object + inherit nopCilVisitor + + method! vfunc f = + let varMap = ref VariableMap.empty in + let visitor = new octagonVariableVisitor(varMap, false) in + ignore (visitCilFunction visitor f); + + list := topVars amount !varMap ::!list; + SkipChildren + +end + +let apronOctagonOption factors file = + let locals = + if List.mem "specification" (get_string_list "ana.autotune.activated" ) && get_string "ana.specification" <> "" then + match Svcomp.Specification.of_option () with + | NoOverflow -> 12 + | _ -> 8 + else 8 + in let globals = 2 in + let selectedLocals = + let list = ref [] in + let visitor = new octagonFunctionVisitor(list, locals) in + visitCilFileSameGlobals visitor file; + List.concat !list + in + let selectedGlobals = + let varMap = ref VariableMap.empty in + let visitor = new octagonVariableVisitor(varMap, true) in + visitCilFileSameGlobals visitor file; + topVars globals !varMap + in + let allVars = (selectedGlobals @ selectedLocals) in + let cost = (Batteries.Int.pow (locals + globals) 3) * (factors.instructions / 70) in + let activateVars () = + print_endline @@ "Octagon: " ^ string_of_int cost; + set_bool "annotation.goblint_apron_track" true; + set_string "ana.apron.domain" "octagon"; + set_auto "ana.activated[+]" "apron"; + set_bool "ana.apron.threshold_widening" true; + set_string "ana.apron.threshold_widening_constants" "comparisons"; + print_endline "Enabled octagon domain for:"; + print_endline @@ String.concat ", " @@ List.map (fun info -> info.vname) allVars; + List.iter (fun info -> info.vattr <- addAttribute (Attr("goblint_apron_track",[])) info.vattr) allVars + in + { + value = 50 * (List.length allVars) ; + cost = cost; + activate = activateVars; + } + + +let wideningOption factors file = + let amountConsts = List.length @@ WideningThresholds.upper_thresholds () in + let cost = amountConsts * (factors.loops * 5 + factors.controlFlowStatements) in + { + value = amountConsts * (factors.loops * 5 + factors.controlFlowStatements); + cost = cost; + activate = fun () -> + print_endline @@ "Widening: " ^ string_of_int cost; + set_bool "ana.int.interval_threshold_widening" true; + set_string "ana.int.interval_threshold_widening_constants" "comparisons"; + print_endline "Enabled widening thresholds"; + } + + +let estimateComplexity factors file = + let pathsEstimate = factors.loops + factors.controlFlowStatements / 90 in + let operationEstimate = factors.instructions + (factors.expressions / 60) in + let callsEstimate = factors.functionCalls * factors.loops / factors.functions / 10 in + let globalVars = fst factors.pointerVars * 2 + fst factors.arrayVars * 4 + fst factors.integralVars in + let localVars = snd factors.pointerVars * 2 + snd factors.arrayVars * 4 + snd factors.integralVars in + let varEstimates = globalVars + localVars / factors.functions in + pathsEstimate * operationEstimate * callsEstimate + varEstimates / 10 + +let totalTarget = 30000 +(*A simple greedy approximation to the knapsack problem: + take options with the highest use/cost ratio that still fit*) +let chooseFromOptions costTarget options = + let ratio o = Float.of_int o.value /. Float.of_int o.cost in + let compareRatio o1 o2 = Float.compare (ratio o1) (ratio o2) in + let rec takeFitting remainingTarget options = + if remainingTarget < 0 then (print_endline @@ "Total: " ^ string_of_int (totalTarget - remainingTarget); [] ) else match options with + | o::os -> + if o.cost < remainingTarget + costTarget / 20 then (*because we are already estimating, we allow overshooting *) + o::takeFitting (remainingTarget - o.cost) os + else + takeFitting (remainingTarget - o.cost) os + | [] -> print_endline @@ "Total: " ^ string_of_int (totalTarget - remainingTarget); [] + in + takeFitting costTarget @@ List.sort compareRatio options + +let isActivated a = get_bool "ana.autotune.enabled" && List.mem a @@ get_string_list "ana.autotune.activated" + +let chooseConfig file = + if isActivated "congruence" then + addModAttributes file; + + if isActivated "noRecursiveIntervals" then + disableIntervalContextsInRecursiveFunctions (); + + if isActivated "mallocWrappers" then + findMallocWrappers (); + + if isActivated "specification" && get_string "ana.specification" <> "" then + focusOnSpecification (); + + if isActivated "enums" && hasEnums file then + set_bool "ana.int.enums" true; + + if isActivated "singleThreaded" then + reduceThreadAnalyses (); + + if isActivated "arrayDomain" then + selectArrayDomains file; + + let factors = collectFactors visitCilFileSameGlobals file in + let fileCompplexity = estimateComplexity factors file in + + print_endline "Collected factors:"; + printFactors factors; + print_endline ""; + print_endline "Complexity estimates:"; + print_endline @@ "File: " ^ string_of_int fileCompplexity; + + let options = [] in + let options = if isActivated "octagon" then (apronOctagonOption factors file)::options else options in + let options = if isActivated "wideningThresholds" then (wideningOption factors file)::options else options in + + List.iter (fun o -> o.activate ()) @@ chooseFromOptions (totalTarget - fileCompplexity) options + + +let reset_lazy () = ResettableLazy.reset functionCallMaps diff --git a/src/autoTune0.ml b/src/autoTune0.ml new file mode 100644 index 0000000000..27dba37252 --- /dev/null +++ b/src/autoTune0.ml @@ -0,0 +1,97 @@ +open GobConfig +open GoblintCil +let isActivated a = get_bool "ana.autotune.enabled" && List.mem a @@ get_string_list "ana.autotune.activated" + +(*Collect stats to be able to make decisions*) +type complexityFactors = { + mutable functions : int; (*function definitions. Does not include extern functions, but functions that get added by goblint (e.g. bsearch or __VERIFIER_nondet_pointer (sv-comp))*) + mutable functionCalls : int; (*places where functions are called*) + mutable loops : int; + mutable loopBreaks : int; (*Breaks and continues. Cil converts the loop conditions to a break. Only set if collection is done before prepareCFG, afterwards they are replaced by GOTOs*) + mutable controlFlowStatements : int; (*Return, Goto, break, continue, if, switch. Includes at least one (implicit) return in each function*) + mutable expressions : int; (* recursively. e.g. x = x + 1 has 4 expressions*) + mutable instructions : int; (*function calls and assignments*) + mutable integralVars : (int * int); (*global, local. Does not consider the types that a pointer/array contains*) + mutable arrayVars : (int * int); + mutable pointerVars : (int * int); +} + +let printFactors f = + Printf.printf "functions: %d\n" f.functions; + Printf.printf "functionCalls: %d\n" f.functionCalls; + Printf.printf "loops: %d\n" f.loops; + Printf.printf "loopBreaks: %d\n" f.loopBreaks; + Printf.printf "controlFlowStatements: %d\n" f.controlFlowStatements; + Printf.printf "expressions: %d\n" f.expressions; + Printf.printf "instructions: %d\n" f.instructions; + Printf.printf "integralVars: (%d,%d)\n" (fst f.integralVars) (snd f.integralVars); + Printf.printf "arrayVars: (%d,%d)\n" (fst f.arrayVars) (snd f.arrayVars); + Printf.printf "pointerVars: (%d,%d)\n" (fst f.pointerVars) (snd f.pointerVars); + flush stdout; + + +class collectComplexityFactorsVisitor(factors) = object + inherit nopCilVisitor + + method! vfunc _ = factors.functions <- factors.functions + 1; DoChildren + + method! vvdec var = + let incVar (g,l) = if var.vglob then (g + 1, l) else (g, l+1) in + (if isIntegralType var.vtype then + factors.integralVars <- incVar factors.integralVars + else if isPointerType var.vtype then + factors.pointerVars <- incVar factors.pointerVars + else if isArrayType var.vtype then + factors.arrayVars <- incVar factors.arrayVars + ); DoChildren + + method! vexpr _ = factors.expressions <- factors.expressions + 1; DoChildren + + method! vinst = function + | Set _ -> + factors.instructions <- factors.instructions + 1; DoChildren + | Call (Some _, _,_,_,_) -> + factors.instructions <- factors.instructions + 2; (*Count function call and assignment of the result seperately *) + factors.functionCalls <- factors.functionCalls + 1; DoChildren + | Call _ -> + factors.instructions <- factors.instructions + 1; + factors.functionCalls <- factors.functionCalls + 1; DoChildren + | _ -> DoChildren + + method! vstmt stmt = match stmt.skind with + | Loop _ -> + factors.controlFlowStatements <- factors.controlFlowStatements + 1; + factors.loops <- factors.loops + 1; DoChildren + | If _ + | Switch _ + | Goto _ + | ComputedGoto _ + | Return _ -> factors.controlFlowStatements <- factors.controlFlowStatements + 1; DoChildren + | Break _ + | Continue _ -> + factors.controlFlowStatements <- factors.controlFlowStatements + 1; + factors.loopBreaks <- factors.loopBreaks + 1; DoChildren + | _ -> DoChildren + +end + +let collectFactors visitAction visitedObject = + let factors = { + functions = 0; + functionCalls = 0; + loops = 0; + loopBreaks = 0; + controlFlowStatements = 0; + expressions = 0; + instructions = 0; + integralVars = (0,0); + arrayVars = (0,0); + pointerVars = (0,0); + } in + let visitor = new collectComplexityFactorsVisitor(factors) in + ignore (visitAction visitor visitedObject); + factors + +let is_large_array = function + | TArray (_,Some (Const (CInt (i,_,_))),_) -> i > Z.of_int @@ 10 * get_int "ana.base.arrays.unrolling-factor" + | _ -> false diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml index 5f01aef297..643e8b76ef 100644 --- a/src/cdomains/apron/apronDomain.apron.ml +++ b/src/cdomains/apron/apronDomain.apron.ml @@ -16,7 +16,7 @@ module M = Messages - heterogeneous environments: https://link.springer.com/chapter/10.1007%2F978-3-030-17184-1_26 (Section 4.1) *) let widening_thresholds_apron = ResettableLazy.from_fun (fun () -> - let t = WideningThresholds.thresholds_incl_mul2 () in + let t = if GobConfig.get_string "ana.apron.threshold_widening_constants" = "comparisons" then WideningThresholds.octagon_thresholds () else WideningThresholds.thresholds_incl_mul2 () in let r = List.map (fun x -> Apron.Scalar.of_mpqf @@ Mpqf.of_mpz @@ Z_mlgmpidl.mpz_of_z x) t in Array.of_list r ) @@ -824,7 +824,9 @@ struct let varinfo_tracked vi = (* no vglob check here, because globals are allowed in apron, but just have to be handled separately *) - type_tracked vi.vtype + let hasTrackAttribute = List.exists (fun (Attr(s,_)) -> s = "goblint_apron_track") in + type_tracked vi.vtype && (not @@ GobConfig.get_bool "annotation.goblint_apron_track" || hasTrackAttribute vi.vattr) + end module DWithOps (Man: Manager) (D: SLattice with type t = Man.mt A.t) = diff --git a/src/cdomains/arrayDomain.ml b/src/cdomains/arrayDomain.ml index 3ef0f8f922..46b0621f75 100644 --- a/src/cdomains/arrayDomain.ml +++ b/src/cdomains/arrayDomain.ml @@ -10,15 +10,44 @@ module BI = IntOps.BigIntOps module LiftExp = Printable.Lift (CilType.Exp) (Printable.DefaultNames) +type domain = TrivialDomain | PartitionedDomain | UnrolledDomain + +(* determines the domain based on variable, type and flag *) +let get_domain ~varAttr ~typAttr = + let domain_from_string = function + | "partitioned" -> PartitionedDomain + | "trivial" -> TrivialDomain + | "unroll" -> UnrolledDomain + | _ -> failwith "AttributeConfiguredArrayDomain: invalid option for domain" + in + (*TODO add options?*) + (*TODO let attribute determine unrolling factor?*) + let from_attributes = List.find_map ( + fun (Attr (s,ps) )-> + if s = "goblint_array_domain" then ( + List.find_map (fun p -> match p with + | AStr x -> Some x + | _ -> None + ) ps + ) + else None + ) in + if get_bool "annotation.goblint_array_domain" then + match from_attributes varAttr, from_attributes typAttr with + | Some x, _ -> domain_from_string x + | _, Some x -> domain_from_string x + | _ -> domain_from_string @@ get_string "ana.base.arrays.domain" + else domain_from_string @@ get_string "ana.base.arrays.domain" + module type S = sig include Lattice.S type idx type value - val get: Q.ask -> t -> ExpDomain.t * idx -> value + val get: ?checkBounds:bool -> Q.ask -> t -> ExpDomain.t * idx -> value val set: Q.ask -> t -> ExpDomain.t * idx -> value -> t - val make: idx -> value -> t + val make: ?varAttr:attributes -> ?typAttr:attributes -> idx -> value -> t val length: t -> idx option val move_if_affected: ?replace_with_const:bool -> Q.ask -> t -> Cil.varinfo -> (Cil.exp -> int option) -> t @@ -29,6 +58,7 @@ sig val smart_widen: (exp -> BI.t option) -> (exp -> BI.t option) -> t -> t -> t val smart_leq: (exp -> BI.t option) -> (exp -> BI.t option) -> t -> t -> bool val update_length: idx -> t -> t + val project: ?varAttr:attributes -> ?typAttr:attributes -> Q.ask -> t -> t end module type LatticeWithSmartOps = @@ -50,9 +80,9 @@ struct let show x = "Array: " ^ Val.show x let pretty () x = text "Array: " ++ pretty () x let pretty_diff () (x,y) = dprintf "%s: %a not leq %a" (name ()) pretty x pretty y - let get (ask: Q.ask) a i = a + let get ?(checkBounds=true) (ask: Q.ask) a i = a let set (ask: Q.ask) a i v = join a v - let make i v = v + let make ?(varAttr=[]) ?(typAttr=[]) i v = v let length _ = None let move_if_affected ?(replace_with_const=false) _ x _ _ = x @@ -65,8 +95,14 @@ struct let smart_widen _ _ = widen let smart_leq _ _ = leq let update_length _ x = x + let project ?(varAttr=[]) ?(typAttr=[]) _ t = t end +let factor () = + match get_int "ana.base.arrays.unrolling-factor" with + | 0 -> failwith "ArrayDomain: ana.base.arrays.unrolling-factor needs to be set when using the unroll domain" + | x -> x + module Unroll (Val: Lattice.S) (Idx:IntDomain.Z): S with type value = Val.t and type idx = Idx.t = struct module Factor = struct let x () = (get_int "ana.base.arrays.unrolling-factor") end @@ -76,10 +112,6 @@ struct let name () = "unrolled arrays" type idx = Idx.t type value = Val.t - let factor () = - match get_int "ana.base.arrays.unrolling-factor" with - | 0 -> failwith "ArrayDomain: ana.base.arrays.unrolling-factor needs to be set when using the unroll domain" - | x -> x let join_of_all_parts (xl, xr) = List.fold_left Val.join xr xl let show (xl, xr) = let rec show_list xlist = match xlist with @@ -92,7 +124,7 @@ struct let extract x default = match x with | Some c -> c | None -> default - let get (ask: Q.ask) (xl, xr) (_,i) = + let get ?(checkBounds=true) (ask: Q.ask) (xl, xr) (_,i) = let search_unrolled_values min_i max_i = let rec subjoin l i = match l with | [] -> Val.bot () @@ -131,7 +163,7 @@ struct if Z.geq min_i f then (xl, (Val.join xr v)) else if Z.lt max_i f then ((update_unrolled_values min_i max_i), xr) else ((update_unrolled_values min_i (Z.of_int ((factor ())-1))), (Val.join xr v)) - let make _ v = + let make ?(varAttr=[]) ?(typAttr=[]) _ v = let xl = BatList.make (factor ()) v in (xl,Val.bot ()) let length _ = None @@ -148,6 +180,7 @@ struct let smart_widen _ _ = widen let smart_leq _ _ = leq let update_length _ x = x + let project ?(varAttr=[]) ?(typAttr=[]) _ t = t end (** Special signature so that we can use the _with_length functions from PartitionedWithLength but still match the interface * @@ -202,9 +235,9 @@ struct "Array (no part.): " ^ Val.show xl else "Array (part. by " ^ Expp.show e ^ "): (" ^ - Val.show xl ^ " -- " ^ - Val.show xm ^ " -- " ^ - Val.show xr ^ ")" + Val.show xl ^ " -- " ^ + Val.show xm ^ " -- " ^ + Val.show xr ^ ")" let pretty () x = text "Array: " ++ text (show x) let pretty_diff () (x,y) = dprintf "%s: %a not leq %a" (name ()) pretty x pretty y @@ -232,7 +265,7 @@ struct let r' = Val.to_yojson r in `Assoc [ ("partitioned by", e'); ("l", l'); ("m", m'); ("r", r') ] - let get (ask:Q.ask) ((e, (xl, xm, xr)) as x) (i,_) = + let get ?(checkBounds=true) (ask:Q.ask) ((e, (xl, xm, xr)) as x) (i,_) = match e, i with | `Lifted e', `Lifted i' -> begin @@ -240,14 +273,14 @@ struct else begin let contributionLess = match Q.may_be_less ask i' e' with (* (may i < e) ? xl : bot *) - | false -> Val.bot () - | _ -> xl in + | false -> Val.bot () + | _ -> xl in let contributionEqual = match Q.may_be_equal ask i' e' with (* (may i = e) ? xm : bot *) - | false -> Val.bot () - | _ -> xm in + | false -> Val.bot () + | _ -> xm in let contributionGreater = match Q.may_be_less ask e' i' with (* (may i > e) ? xr : bot *) - | false -> Val.bot () - | _ -> xr in + | false -> Val.bot () + | _ -> xr in Val.join (Val.join contributionLess contributionEqual) contributionGreater end end @@ -269,24 +302,24 @@ struct | Field (_, o) -> offset_contains_array_access o in match e with - | Const _ - | SizeOf _ - | SizeOfE _ - | SizeOfStr _ - | AlignOf _ - | AlignOfE _ -> false - | Question(e1, e2, e3, _) -> - contains_array_access e1 || contains_array_access e2 || contains_array_access e3 - | CastE(_, e) - | UnOp(_, e , _) - | Real e - | Imag e -> contains_array_access e - | BinOp(_, e1, e2, _) -> contains_array_access e1 || contains_array_access e2 - | AddrOf _ - | AddrOfLabel _ - | StartOf _ -> false - | Lval(Mem e, o) -> offset_contains_array_access o || contains_array_access e - | Lval(Var _, o) -> offset_contains_array_access o + | Const _ + | SizeOf _ + | SizeOfE _ + | SizeOfStr _ + | AlignOf _ + | AlignOfE _ -> false + | Question(e1, e2, e3, _) -> + contains_array_access e1 || contains_array_access e2 || contains_array_access e3 + | CastE(_, e) + | UnOp(_, e , _) + | Real e + | Imag e -> contains_array_access e + | BinOp(_, e1, e2, _) -> contains_array_access e1 || contains_array_access e2 + | AddrOf _ + | AddrOfLabel _ + | StartOf _ -> false + | Lval(Mem e, o) -> offset_contains_array_access o || contains_array_access e + | Lval(Var _, o) -> offset_contains_array_access o in match e with | `Top @@ -337,37 +370,37 @@ struct in match e with | `Lifted exp -> - let is_affected = Basetype.CilExp.occurs v exp in - if not is_affected then - x - else - (* check if one part covers the entire array, so we can drop partitioning *) - begin - let e_must_bigger_max_index = - match length with - | Some l -> - begin - match Idx.to_int l with - | Some i -> - let b = Q.may_be_less ask exp (Cil.kintegerCilint (Cilfacade.ptrdiff_ikind ()) i) in - not b (* !(e <_{may} length) => e >=_{must} length *) - | None -> false - end - | _ -> false - in - let e_must_less_zero = - Q.eval_int_binop (module Q.MustBool) Lt ask exp Cil.zero (* TODO: untested *) - in - if e_must_bigger_max_index then - (* Entire array is covered by left part, dropping partitioning. *) - Expp.top(),(xl, xl, xl) - else if e_must_less_zero then - (* Entire array is covered by right value, dropping partitioning. *) - Expp.top(),(xr, xr, xr) - else - (* If we can not drop partitioning, move *) - move (movement_for_exp exp) - end + let is_affected = Basetype.CilExp.occurs v exp in + if not is_affected then + x + else + (* check if one part covers the entire array, so we can drop partitioning *) + begin + let e_must_bigger_max_index = + match length with + | Some l -> + begin + match Idx.to_int l with + | Some i -> + let b = Q.may_be_less ask exp (Cil.kintegerCilint (Cilfacade.ptrdiff_ikind ()) i) in + not b (* !(e <_{may} length) => e >=_{must} length *) + | None -> false + end + | _ -> false + in + let e_must_less_zero = + Q.eval_int_binop (module Q.MustBool) Lt ask exp Cil.zero (* TODO: untested *) + in + if e_must_bigger_max_index then + (* Entire array is covered by left part, dropping partitioning. *) + Expp.top(),(xl, xl, xl) + else if e_must_less_zero then + (* Entire array is covered by right value, dropping partitioning. *) + Expp.top(),(xr, xr, xr) + else + (* If we can not drop partitioning, move *) + move (movement_for_exp exp) + end | _ -> x (* If the array is not partitioned, nothing to do *) let move_if_affected ?replace_with_const = move_if_affected_with_length ?replace_with_const None @@ -377,8 +410,8 @@ struct if i = `Lifted MyCFG.all_array_index_exp then (assert !Goblintutil.global_initialization; (* just joining with xm here assumes that all values will be set, which is guaranteed during inits *) (* the join is needed here! see e.g 30/04 *) - let r = Val.join xm a in - (Expp.top(), (r, r, r))) + let r = Val.join xm a in + (Expp.top(), (r, r, r))) else normalize @@ let use_last = get_string "ana.base.partition-arrays.keep-expr" = "last" in @@ -433,19 +466,19 @@ struct (e, (xl, a, xr)) else if Cil.isConstant e' && Cil.isConstant i' then match Cil.getInteger e', Cil.getInteger i' with - | Some (e'': Cilint.cilint), Some i'' -> - let (i'': BI.t) = Cilint.big_int_of_cilint i'' in - let (e'': BI.t) = Cilint.big_int_of_cilint e'' in - - if BI.equal i'' (BI.add e'' BI.one) then - (* If both are integer constants and they are directly adjacent, we change partitioning to maintain information *) - (i, (Val.join xl xm, a, xr)) - else if BI.equal e'' (BI.add i'' BI.one) then - (i, (xl, a, Val.join xm xr)) - else - default - | _ -> + | Some (e'': Cilint.cilint), Some i'' -> + let (i'': BI.t) = Cilint.big_int_of_cilint i'' in + let (e'': BI.t) = Cilint.big_int_of_cilint e'' in + + if BI.equal i'' (BI.add e'' BI.one) then + (* If both are integer constants and they are directly adjacent, we change partitioning to maintain information *) + (i, (Val.join xl xm, a, xr)) + else if BI.equal e'' (BI.add i'' BI.one) then + (i, (xl, a, Val.join xm xr)) + else default + | _ -> + default else default end @@ -457,36 +490,36 @@ struct (match Q.may_be_equal ask e' i' with (* TODO: untested *) | false -> Val.bot() | _ -> xm) (* if e' may be equal to i', but e' may not be smaller than i' then we only need xm *) - ( - let t = Cilfacade.typeOf e' in - let ik = Cilfacade.get_ikind t in - match Q.must_be_equal ask (BinOp(PlusA, e', Cil.kinteger ik 1, t)) i' with - | true -> xm - | _ -> - begin - match Q.may_be_less ask e' i' with (* TODO: untested *) - | false-> Val.bot() - | _ -> Val.join xm xr (* if e' may be less than i' then we also need xm for sure *) - end - ) + ( + let t = Cilfacade.typeOf e' in + let ik = Cilfacade.get_ikind t in + match Q.must_be_equal ask (BinOp(PlusA, e', Cil.kinteger ik 1, t)) i' with + | true -> xm + | _ -> + begin + match Q.may_be_less ask e' i' with (* TODO: untested *) + | false-> Val.bot() + | _ -> Val.join xm xr (* if e' may be less than i' then we also need xm for sure *) + end + ) in let right = if equals_maxIndex i then Val.bot () else Val.join xr @@ Val.join (match Q.may_be_equal ask e' i' with (* TODO: untested *) | false -> Val.bot() | _ -> xm) - ( - let t = Cilfacade.typeOf e' in - let ik = Cilfacade.get_ikind t in - match Q.must_be_equal ask (BinOp(PlusA, e', Cil.kinteger ik (-1), t)) i' with (* TODO: untested *) - | true -> xm - | _ -> - begin - match Q.may_be_less ask i' e' with (* TODO: untested *) - | false -> Val.bot() - | _ -> Val.join xl xm (* if e' may be less than i' then we also need xm for sure *) - end - ) + ( + let t = Cilfacade.typeOf e' in + let ik = Cilfacade.get_ikind t in + match Q.must_be_equal ask (BinOp(PlusA, e', Cil.kinteger ik (-1), t)) i' with (* TODO: untested *) + | true -> xm + | _ -> + begin + match Q.may_be_less ask i' e' with (* TODO: untested *) + | false -> Val.bot() + | _ -> Val.join xl xm (* if e' may be less than i' then we also need xm for sure *) + end + ) in (* The new thing is partitioned according to i so we can strongly update *) (i,(left, a, right)) @@ -507,7 +540,7 @@ struct (* leq needs not be given explicitly, leq from product domain works here *) - let make i v = + let make ?(varAttr=[]) ?(typAttr=[]) i v = if Idx.to_int i = Some BI.one then (`Lifted (Cil.integer 0), (v, v, v)) else if Val.is_bot v then @@ -554,16 +587,16 @@ struct else (Expp.top (), (op_over_all, op_over_all, op_over_all)) else (* first try if the result can be partitioned by e2e *) - if must_be_zero e2e_in_state_of_x1 then - (e2, (xl2, op over_all_x1 xm2, op over_all_x1 xr2)) - else if must_be_length_minus_one e2e_in_state_of_x1 then - (e2, (op over_all_x1 xl2, op over_all_x1 xm2, xr2)) - else if must_be_zero e1e_in_state_of_x2 then - (e1, (xl1, op xm1 over_all_x2, op xr1 over_all_x2)) - else if must_be_length_minus_one e1e_in_state_of_x2 then - (e1, (op xl1 over_all_x2, op xm1 over_all_x2, xr1)) - else - (Expp.top (), (op_over_all, op_over_all, op_over_all)) + if must_be_zero e2e_in_state_of_x1 then + (e2, (xl2, op over_all_x1 xm2, op over_all_x1 xr2)) + else if must_be_length_minus_one e2e_in_state_of_x1 then + (e2, (op over_all_x1 xl2, op over_all_x1 xm2, xr2)) + else if must_be_zero e1e_in_state_of_x2 then + (e1, (xl1, op xm1 over_all_x2, op xr1 over_all_x2)) + else if must_be_length_minus_one e1e_in_state_of_x2 then + (e1, (op xl1 over_all_x2, op xm1 over_all_x2, xr1)) + else + (Expp.top (), (op_over_all, op_over_all, op_over_all)) else (Expp.top (), (op_over_all, op_over_all, op_over_all)) | `Top, `Top -> @@ -656,6 +689,7 @@ struct | _ -> narrow (e1,v1) (e2,v2) let update_length _ x = x + let project ?(varAttr=[]) ?(typAttr=[]) _ t = t end (* This is the main array out of bounds check *) let array_oob_check ( type a ) (module Idx: IntDomain.Z with type t = a) (x, l) (e, v) = @@ -686,13 +720,12 @@ struct type idx = Idx.t type value = Val.t - let get (ask : Q.ask) (x, (l : idx)) ((e: ExpDomain.t), v) = - (array_oob_check (module Idx) (x, l) (e, v)); + let get ?(checkBounds=true) (ask : Q.ask) (x, (l : idx)) ((e: ExpDomain.t), v) = + if checkBounds then (array_oob_check (module Idx) (x, l) (e, v)); Base.get ask x (e, v) let set (ask: Q.ask) (x,l) i v = Base.set ask x i v, l - let make l x = Base.make l x, l + let make ?(varAttr=[]) ?(typAttr=[]) l x = Base.make l x, l let length (_,l) = Some l - let move_if_affected ?(replace_with_const=false) _ x _ _ = x let map f (x, l):t = (Base.map f x, l) let fold_left f a (x, l) = Base.fold_left f a x @@ -710,6 +743,8 @@ struct (* the declaration is visited. *) let update_length newl (x, l) = (x, newl) + let project ?(varAttr=[]) ?(typAttr=[]) _ t = t + let printXml f (x,y) = BatPrintf.fprintf f "\n\n\n%s\n\n%a\n%s\n\n%a\n\n" (XmlUtil.escape (Base.name ())) Base.printXml x "length" Idx.printXml y @@ -724,11 +759,11 @@ struct type idx = Idx.t type value = Val.t - let get (ask : Q.ask) (x, (l : idx)) ((e: ExpDomain.t), v) = - (array_oob_check (module Idx) (x, l) (e, v)); + let get ?(checkBounds=true) (ask : Q.ask) (x, (l : idx)) ((e: ExpDomain.t), v) = + if checkBounds then (array_oob_check (module Idx) (x, l) (e, v)); Base.get ask x (e, v) let set ask (x,l) i v = Base.set_with_length (Some l) ask x i v, l - let make l x = Base.make l x, l + let make ?(varAttr=[]) ?(typAttr=[]) l x = Base.make l x, l let length (_,l) = Some l let move_if_affected ?replace_with_const ask (x,l) v i = @@ -758,6 +793,8 @@ struct (* the declaration is visited. *) let update_length newl (x, l) = (x, newl) + let project ?(varAttr=[]) ?(typAttr=[]) _ t = t + let printXml f (x,y) = BatPrintf.fprintf f "\n\n\n%s\n\n%a\n%s\n\n%a\n\n" (XmlUtil.escape (Base.name ())) Base.printXml x "length" Idx.printXml y @@ -771,11 +808,11 @@ struct type idx = Idx.t type value = Val.t - let get (ask : Q.ask) (x, (l : idx)) ((e: ExpDomain.t), v) = - (array_oob_check (module Idx) (x, l) (e, v)); + let get ?(checkBounds=true) (ask : Q.ask) (x, (l : idx)) ((e: ExpDomain.t), v) = + if checkBounds then (array_oob_check (module Idx) (x, l) (e, v)); Base.get ask x (e, v) let set (ask: Q.ask) (x,l) i v = Base.set ask x i v, l - let make l x = Base.make l x, l + let make ?(varAttr=[]) ?(typAttr=[]) l x = Base.make l x, l let length (_,l) = Some l let move_if_affected ?(replace_with_const=false) _ x _ _ = x @@ -795,13 +832,15 @@ struct (* the declaration is visited. *) let update_length newl (x, l) = (x, newl) + let project ?(varAttr=[]) ?(typAttr=[]) _ t = t + let printXml f (x,y) = BatPrintf.fprintf f "\n\n\n%s\n\n%a\n%s\n\n%a\n\n" (XmlUtil.escape (Base.name ())) Base.printXml x "length" Idx.printXml y let to_yojson (x, y) = `Assoc [ (Base.name (), Base.to_yojson x); ("length", Idx.to_yojson y) ] end -module FlagConfiguredArrayDomain(Val: LatticeWithSmartOps) (Idx:IntDomain.Z):S with type value = Val.t and type idx = Idx.t = +module AttributeConfiguredArrayDomain(Val: LatticeWithSmartOps) (Idx:IntDomain.Z):S with type value = Val.t and type idx = Idx.t = struct module P = PartitionedWithLength(Val)(Idx) module T = TrivialWithLength(Val)(Idx) @@ -811,15 +850,15 @@ struct type value = Val.t module K = struct - let msg = "FlagConfiguredArrayDomain received a value where not exactly one component is set" - let name = "FlagConfiguredArrayDomain" + let msg = "AttributeConfiguredArrayDomain received a value where not exactly one component is set" + let name = "AttributeConfiguredArrayDomain" end let to_t = function | (Some p, None, None) -> (Some p, None) | (None, Some t, None) -> (None, Some (Some t, None)) | (None, None, Some u) -> (None, Some (None, Some u)) - | _ -> failwith "FlagConfiguredArrayDomain received a value where not exactly one component is set" + | _ -> failwith "AttributeConfiguredArrayDomain received a value where not exactly one component is set" module I = struct include LatticeFlagHelper (T) (U) (K) let name () = "" end include LatticeFlagHelper (P) (I) (K) @@ -830,13 +869,13 @@ struct let unop_to_t' opp opt opu = unop_to_t opp (I.unop_to_t opt opu) (* Simply call appropriate function for component that is not None *) - let get a x (e,i) = unop' (fun x -> + let get ?(checkBounds=true) a x (e,i) = unop' (fun x -> if e = `Top then let e' = BatOption.map_default (fun x -> `Lifted (Cil.kintegerCilint (Cilfacade.ptrdiff_ikind ()) x)) (`Top) (Idx.to_int i) in - P.get a x (e', i) + P.get ~checkBounds a x (e', i) else - P.get a x (e, i) - ) (fun x -> T.get a x (e,i)) (fun x -> U.get a x (e,i)) x + P.get ~checkBounds a x (e, i) + ) (fun x -> T.get ~checkBounds a x (e,i)) (fun x -> U.get ~checkBounds a x (e,i)) x let set (ask:Q.ask) x i a = unop_to_t' (fun x -> P.set ask x i a) (fun x -> T.set ask x i a) (fun x -> U.set ask x i a) x let length = unop' P.length T.length U.length let map f = unop_to_t' (P.map f) (T.map f) (U.map f) @@ -845,37 +884,68 @@ struct let move_if_affected ?(replace_with_const=false) (ask:Q.ask) x v f = unop_to_t' (fun x -> P.move_if_affected ~replace_with_const:replace_with_const ask x v f) (fun x -> T.move_if_affected ~replace_with_const:replace_with_const ask x v f) (fun x -> U.move_if_affected ~replace_with_const:replace_with_const ask x v f) x let get_vars_in_e = unop' P.get_vars_in_e T.get_vars_in_e U.get_vars_in_e let smart_join f g = binop_to_t' (P.smart_join f g) (T.smart_join f g) (U.smart_join f g) - let smart_widen f g = binop_to_t' (P.smart_widen f g) (T.smart_widen f g) (U.smart_widen f g) + let smart_widen f g = binop_to_t' (P.smart_widen f g) (T.smart_widen f g) (U.smart_widen f g) let smart_leq f g = binop' (P.smart_leq f g) (T.smart_leq f g) (U.smart_leq f g) let update_length newl x = unop_to_t' (P.update_length newl) (T.update_length newl) (U.update_length newl) x - - (* Functions that make use of the configuration flag *) - let chosen_domain () = get_string "ana.base.arrays.domain" - - let name () = "FlagConfiguredArrayDomain: " ^ match chosen_domain () with - | "trivial" -> T.name () - | "partitioned" -> P.name () - | "unroll" -> U.name () - | _ -> failwith "FlagConfiguredArrayDomain cannot name an array from set option" - - let bot () = - to_t @@ match chosen_domain () with - | "partitioned" -> (Some (P.bot ()), None, None) - | "trivial" -> (None, Some (T.bot ()), None) - | "unroll" -> (None, None, Some (U.bot ())) - | _ -> failwith "FlagConfiguredArrayDomain cannot construct a bot array from set option" - - let top () = - to_t @@ match chosen_domain () with - | "partitioned" -> (Some (P.top ()), None, None) - | "trivial" -> (None, Some (T.top ()), None) - | "unroll" -> (None, None, Some (U.top ())) - | _ -> failwith "FlagConfiguredArrayDomain cannot construct a top array from set option" - - let make i v = - to_t @@ match chosen_domain () with - | "partitioned" -> (Some (P.make i v), None, None) - | "trivial" -> (None, Some (T.make i v), None) - | "unroll" -> (None, None, Some (U.make i v)) - | _ -> failwith "FlagConfiguredArrayDomain cannot construct an array from set option" + let name () = "AttributeConfiguredArrayDomain" + + let bot () = to_t @@ match get_domain ~varAttr:[] ~typAttr:[] with + | PartitionedDomain -> (Some (P.bot ()), None, None) + | TrivialDomain -> (None, Some (T.bot ()), None) + | UnrolledDomain -> (None, None, Some (U.bot ())) + + let top () = to_t @@ match get_domain ~varAttr:[] ~typAttr:[] with + | PartitionedDomain -> (Some (P.top ()), None, None) + | TrivialDomain -> (None, Some (T.top ()), None) + | UnrolledDomain -> (None, None, Some (U.top ())) + + let make ?(varAttr=[]) ?(typAttr=[]) i v = to_t @@ match get_domain ~varAttr ~typAttr with + | PartitionedDomain -> (Some (P.make i v), None, None) + | TrivialDomain -> (None, Some (T.make i v), None) + | UnrolledDomain -> (None, None, Some (U.make i v)) + + (* convert to another domain *) + let index_as_expression i = (`Lifted (Cil.integer i), Idx.of_int IInt (BI.of_int i)) + + let partitioned_of_trivial ask t = P.make (Option.value (T.length t) ~default:(Idx.top ())) (T.get ~checkBounds:false ask t (index_as_expression 0)) + + let partitioned_of_unroll ask u = + (* We end with a partition at "ana.base.arrays.unrolling-factor", which keeps the most information. Maybe first element is more commonly useful? *) + let rest = (U.get ~checkBounds:false ask u (index_as_expression (factor ()))) in + let p = P.make (Option.value (U.length u) ~default:(Idx.top ())) rest in + let get_i i = (i, P.get ~checkBounds:false ask p (index_as_expression i)) in + let set_i p (i,v) = P.set ask p (index_as_expression i) v in + List.fold_left set_i p @@ List.init (factor ()) get_i + + let trivial_of_partitioned ask p = + let element = (P.get ~checkBounds:false ask p (ExpDomain.top (), Idx.top ())) + in T.make (Option.value (P.length p) ~default:(Idx.top ())) element + + let trivial_of_unroll ask u = + let get_i i = U.get ~checkBounds:false ask u (index_as_expression i) in + let element = List.fold_left Val.join (get_i (factor ())) @@ List.init (factor ()) get_i in (*join all single elements and the element at *) + T.make (Option.value (U.length u) ~default:(Idx.top ())) element + + let unroll_of_trivial ask t = U.make (Option.value (T.length t) ~default:(Idx.top ())) (T.get ~checkBounds:false ask t (index_as_expression 0)) + + let unroll_of_partitioned ask p = + let unrolledValues = List.init (factor ()) (fun i ->(i, P.get ~checkBounds:false ask p (index_as_expression i))) in + (* This could be more precise if we were able to compare this with the partition index, but we can not access it here *) + let rest = (P.get ~checkBounds:false ask p (ExpDomain.top (), Idx.top ())) in + let u = U.make (Option.value (P.length p) ~default:(Idx.top ())) (Val.bot ()) in + let set_i u (i,v) = U.set ask u (index_as_expression i) v in + set_i (List.fold_left set_i u unrolledValues) (factor (), rest) + + let project ?(varAttr=[]) ?(typAttr=[]) ask (t:t) = + match get_domain ~varAttr ~typAttr, t with + | PartitionedDomain, (Some x, None) -> to_t @@ (Some x, None, None) + | PartitionedDomain, (None, Some (Some x, None)) -> to_t @@ (Some (partitioned_of_trivial ask x), None, None) + | PartitionedDomain, (None, Some (None, Some x)) -> to_t @@ (Some (partitioned_of_unroll ask x), None, None) + | TrivialDomain, (Some x, None) -> to_t @@ (None, Some (trivial_of_partitioned ask x), None) + | TrivialDomain, (None, Some (Some x, None)) -> to_t @@ (None, Some x, None) + | TrivialDomain, (None, Some (None, Some x)) -> to_t @@ (None, Some (trivial_of_unroll ask x), None) + | UnrolledDomain, (Some x, None) -> to_t @@ (None, None, Some (unroll_of_partitioned ask x) ) + | UnrolledDomain, (None, Some (Some x, None)) -> to_t @@ (None, None, Some (unroll_of_trivial ask x) ) + | UnrolledDomain, (None, Some (None, Some x)) -> to_t @@ (None, None, Some x) + | _ -> failwith "AttributeConfiguredArrayDomain received a value where not exactly one component is set" end diff --git a/src/cdomains/arrayDomain.mli b/src/cdomains/arrayDomain.mli index 2254c31f8a..a69468a3a0 100644 --- a/src/cdomains/arrayDomain.mli +++ b/src/cdomains/arrayDomain.mli @@ -1,6 +1,11 @@ open IntOps open GoblintCil +type domain = TrivialDomain | PartitionedDomain | UnrolledDomain + +val get_domain: varAttr:Cil.attributes -> typAttr:Cil.attributes -> domain +(** gets the underlying domain: chosen by the attributes in AttributeConfiguredArrayDomain *) + (** Abstract domains representing arrays. *) module type S = sig @@ -11,14 +16,14 @@ sig type value (** The abstract domain of values stored in the array. *) - val get: Queries.ask -> t -> ExpDomain.t * idx -> value + val get: ?checkBounds:bool -> Queries.ask -> t -> ExpDomain.t * idx -> value (** Returns the element residing at the given index. *) val set: Queries.ask -> t -> ExpDomain.t * idx -> value -> t (** Returns a new abstract value, where the given index is replaced with the * given element. *) - val make: idx -> value -> t + val make: ?varAttr:Cil.attributes -> ?typAttr:Cil.attributes -> idx -> value -> t (** [make l e] creates an abstract representation of an array of length [l] * containing the element [e]. *) @@ -43,6 +48,8 @@ sig val smart_widen: (Cil.exp -> BigIntOps.t option) -> (Cil.exp -> BigIntOps.t option) -> t -> t -> t val smart_leq: (Cil.exp -> BigIntOps.t option) -> (Cil.exp -> BigIntOps.t option) -> t -> t -> bool val update_length: idx -> t -> t + + val project: ?varAttr:Cil.attributes -> ?typAttr:Cil.attributes -> Queries.ask -> t -> t end module type LatticeWithSmartOps = @@ -68,10 +75,10 @@ module Partitioned (Val: LatticeWithSmartOps) (Idx: IntDomain.Z): S with type va * uses three values from Val to represent the elements of the array to the left, * at, and to the right of the expression. The Idx domain is required only so to * have a signature that allows for choosing an array representation at runtime. - *) +*) module PartitionedWithLength (Val: LatticeWithSmartOps) (Idx:IntDomain.Z): S with type value = Val.t and type idx = Idx.t (** Like partitioned but additionally manages the length of the array. *) -module FlagConfiguredArrayDomain(Val: LatticeWithSmartOps) (Idx:IntDomain.Z):S with type value = Val.t and type idx = Idx.t -(** Switches between PartitionedWithLength, TrivialWithLength and Unroll based on the value of ana.base.arrays.domain. *) +module AttributeConfiguredArrayDomain(Val: LatticeWithSmartOps) (Idx:IntDomain.Z):S with type value = Val.t and type idx = Idx.t +(** Switches between PartitionedWithLength, TrivialWithLength and Unroll based on variable, type, and flag. *) diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml index d0a74d2226..9c9d40e7bf 100644 --- a/src/cdomains/intDomain.ml +++ b/src/cdomains/intDomain.ml @@ -616,13 +616,13 @@ struct let (min_ik, max_ik) = range ik in let threshold = get_bool "ana.int.interval_threshold_widening" in let upper_threshold u = - let ts = ResettableLazy.force widening_thresholds in + let ts = if GobConfig.get_string "ana.int.interval_threshold_widening_constants" = "comparisons" then WideningThresholds.upper_thresholds () else ResettableLazy.force widening_thresholds in let u = Ints_t.to_bigint u in let t = List.find_opt (fun x -> Z.compare u x <= 0) ts in BatOption.map_default Ints_t.of_bigint max_ik t in let lower_threshold l = - let ts = ResettableLazy.force widening_thresholds_desc in + let ts = if GobConfig.get_string "ana.int.interval_threshold_widening_constants" = "comparisons" then WideningThresholds.lower_thresholds () else ResettableLazy.force widening_thresholds_desc in let l = Ints_t.to_bigint l in let t = List.find_opt (fun x -> Z.compare l x >= 0) ts in BatOption.map_default Ints_t.of_bigint min_ik t diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml index d11f5f3c58..dd852b0824 100644 --- a/src/cdomains/valueDomain.ml +++ b/src/cdomains/valueDomain.ml @@ -1,6 +1,5 @@ open GoblintCil open Pretty -open GobConfig open PrecisionUtil include PreValueDomain @@ -29,14 +28,14 @@ sig val smart_widen: (exp -> BI.t option) -> (exp -> BI.t option) -> t -> t -> t val smart_leq: (exp -> BI.t option) -> (exp -> BI.t option) -> t -> t -> bool val is_immediate_type: typ -> bool - val bot_value: typ -> t + val bot_value: ?varAttr:attributes -> typ -> t val is_bot_value: t -> bool - val init_value: typ -> t - val top_value: typ -> t + val init_value: ?varAttr:attributes -> typ -> t + val top_value: ?varAttr:attributes -> typ -> t val is_top_value: t -> typ -> bool - val zero_init_value: typ -> t + val zero_init_value: ?varAttr:attributes -> typ -> t - val project: int_precision -> t -> t + val project: Q.ask -> int_precision option-> ( attributes * attributes ) option -> t -> t end module type Blob = @@ -108,21 +107,23 @@ struct | TNamed ({tname = "pthread_t"; _}, _) -> true | _ -> false - let rec bot_value (t: typ): t = + let rec bot_value ?(varAttr=[]) (t: typ): t = match t with | _ when is_mutex_type t -> `Mutex | TInt _ -> `Bot (*`Int (ID.bot ()) -- should be lower than any int or address*) | TFloat _ -> `Bot | TPtr _ -> `Address (AD.bot ()) - | TComp ({cstruct=true; _} as ci,_) -> `Struct (Structs.create (fun fd -> bot_value fd.ftype) ci) + | TComp ({cstruct=true; _} as ci,_) -> `Struct (Structs.create (fun fd -> bot_value ~varAttr:fd.fattr fd.ftype) ci) | TComp ({cstruct=false; _},_) -> `Union (Unions.bot ()) | TArray (ai, None, _) -> - `Array (CArrays.make (IndexDomain.bot ()) (bot_value ai)) + let typAttr = typeAttrs ai in + `Array (CArrays.make ~varAttr ~typAttr (IndexDomain.bot ()) (bot_value ai)) | TArray (ai, Some exp, _) -> + let typAttr = typeAttrs ai in let l = BatOption.map Cilint.big_int_of_cilint (Cil.getInteger (Cil.constFold true exp)) in - `Array (CArrays.make (BatOption.map_default (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ())) (IndexDomain.bot ()) l) (bot_value ai)) + `Array (CArrays.make ~varAttr ~typAttr (BatOption.map_default (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ())) (IndexDomain.bot ()) l) (bot_value ai)) | t when is_thread_type t -> `Thread (ConcDomain.ThreadSet.empty ()) - | TNamed ({ttype=t; _}, _) -> bot_value t + | TNamed ({ttype=t; _}, _) -> bot_value ~varAttr (unrollType t) | _ -> `Bot let is_bot_value x = @@ -139,37 +140,45 @@ struct | `Bot -> true | `Top -> false - let rec init_value (t: typ): t = (* top_value is not used here because structs, blob etc will not contain the right members *) + let rec init_value ?(varAttr=[]) (t: typ): t = (* top_value is not used here because structs, blob etc will not contain the right members *) match t with | t when is_mutex_type t -> `Mutex | TInt (ik,_) -> `Int (ID.top_of ik) | TFloat ((FFloat | FDouble | FLongDouble as fkind), _) -> `Float (FD.top_of fkind) | TPtr _ -> `Address AD.top_ptr - | TComp ({cstruct=true; _} as ci,_) -> `Struct (Structs.create (fun fd -> init_value fd.ftype) ci) + | TComp ({cstruct=true; _} as ci,_) -> `Struct (Structs.create (fun fd -> init_value ~varAttr:fd.fattr fd.ftype) ci) | TComp ({cstruct=false; _},_) -> `Union (Unions.top ()) | TArray (ai, None, _) -> - `Array (CArrays.make (IndexDomain.bot ()) (if (get_string "ana.base.arrays.domain"="partitioned" || get_string "ana.base.arrays.domain"="unroll") then (init_value ai) else (bot_value ai))) + let typAttr = typeAttrs ai in + let domain = ArrayDomain.get_domain ~varAttr ~typAttr in + `Array (CArrays.make ~varAttr ~typAttr (IndexDomain.bot ()) (if (domain = PartitionedDomain || domain = UnrolledDomain) then (init_value ai) else (bot_value ai))) | TArray (ai, Some exp, _) -> + let typAttr = typeAttrs ai in let l = BatOption.map Cilint.big_int_of_cilint (Cil.getInteger (Cil.constFold true exp)) in - `Array (CArrays.make (BatOption.map_default (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ())) (IndexDomain.bot ()) l) (if (get_string "ana.base.arrays.domain"="partitioned" || get_string "ana.base.arrays.domain"="unroll") then (init_value ai) else (bot_value ai))) + let domain = ArrayDomain.get_domain ~varAttr ~typAttr in + `Array (CArrays.make ~varAttr ~typAttr (BatOption.map_default (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ())) (IndexDomain.bot ()) l) (if (domain = PartitionedDomain || domain = UnrolledDomain) then (init_value ai) else (bot_value ai))) (* | t when is_thread_type t -> `Thread (ConcDomain.ThreadSet.empty ()) *) - | TNamed ({ttype=t; _}, _) -> init_value t + | TNamed ({ttype=t; _}, _) -> init_value ~varAttr t | _ -> `Top - let rec top_value (t: typ): t = + let rec top_value ?(varAttr=[]) (t: typ): t = match t with | _ when is_mutex_type t -> `Mutex | TInt (ik,_) -> `Int (ID.(cast_to ik (top_of ik))) | TFloat ((FFloat | FDouble | FLongDouble as fkind), _) -> `Float (FD.top_of fkind) | TPtr _ -> `Address AD.top_ptr - | TComp ({cstruct=true; _} as ci,_) -> `Struct (Structs.create (fun fd -> top_value fd.ftype) ci) + | TComp ({cstruct=true; _} as ci,_) -> `Struct (Structs.create (fun fd -> top_value ~varAttr:fd.fattr fd.ftype) ci) | TComp ({cstruct=false; _},_) -> `Union (Unions.top ()) | TArray (ai, None, _) -> - `Array (CArrays.make (IndexDomain.top ()) (if (get_string "ana.base.arrays.domain"="partitioned" || get_string "ana.base.arrays.domain"="unroll") then (top_value ai) else (bot_value ai))) + let typAttr = typeAttrs ai in + let domain = ArrayDomain.get_domain ~varAttr ~typAttr in + `Array (CArrays.make ~varAttr ~typAttr (IndexDomain.top ()) (if (domain = PartitionedDomain || domain = UnrolledDomain) then (top_value ai) else (bot_value ai))) | TArray (ai, Some exp, _) -> + let typAttr = typeAttrs ai in let l = BatOption.map Cilint.big_int_of_cilint (Cil.getInteger (Cil.constFold true exp)) in - `Array (CArrays.make (BatOption.map_default (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ())) (IndexDomain.top_of (Cilfacade.ptrdiff_ikind ())) l) (if (get_string "ana.base.arrays.domain"="partitioned" || get_string "ana.base.arrays.domain"="unroll") then (top_value ai) else (bot_value ai))) - | TNamed ({ttype=t; _}, _) -> top_value t + let domain = ArrayDomain.get_domain ~varAttr ~typAttr in + `Array (CArrays.make ~varAttr ~typAttr (BatOption.map_default (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ())) (IndexDomain.top_of (Cilfacade.ptrdiff_ikind ())) l) (if (domain = PartitionedDomain || domain = UnrolledDomain) then (top_value ai) else (bot_value ai))) + | TNamed ({ttype=t; _}, _) -> top_value ~varAttr t | _ -> `Top let is_top_value x (t: typ) = @@ -186,31 +195,33 @@ struct | `Top -> true | `Bot -> false - let rec zero_init_value (t:typ): t = - match t with - | _ when is_mutex_type t -> `Mutex - | TInt (ikind, _) -> `Int (ID.of_int ikind BI.zero) - | TFloat ((FFloat | FDouble | FLongDouble as fkind), _) -> `Float (FD.of_const fkind 0.0) - | TPtr _ -> `Address AD.null_ptr - | TComp ({cstruct=true; _} as ci,_) -> `Struct (Structs.create (fun fd -> zero_init_value fd.ftype) ci) - | TComp ({cstruct=false; _} as ci,_) -> - let v = try + let rec zero_init_value ?(varAttr=[]) (t:typ): t = + match t with + | _ when is_mutex_type t -> `Mutex + | TInt (ikind, _) -> `Int (ID.of_int ikind BI.zero) + | TFloat ((FFloat | FDouble | FLongDouble as fkind), _) -> `Float (FD.of_const fkind 0.0) + | TPtr _ -> `Address AD.null_ptr + | TComp ({cstruct=true; _} as ci,_) -> `Struct (Structs.create (fun fd -> zero_init_value ~varAttr:fd.fattr fd.ftype) ci) + | TComp ({cstruct=false; _} as ci,_) -> + let v = try (* C99 6.7.8.10: the first named member is initialized (recursively) according to these rules *) let firstmember = List.hd ci.cfields in - `Lifted firstmember, zero_init_value firstmember.ftype + `Lifted firstmember, zero_init_value ~varAttr:firstmember.fattr firstmember.ftype with - (* Union with no members ò.O *) + (* Union with no members ò.O *) Failure _ -> Unions.top () - in - `Union(v) - | TArray (ai, None, _) -> - `Array (CArrays.make (IndexDomain.top_of (Cilfacade.ptrdiff_ikind ())) (zero_init_value ai)) - | TArray (ai, Some exp, _) -> - let l = BatOption.map Cilint.big_int_of_cilint (Cil.getInteger (Cil.constFold true exp)) in - `Array (CArrays.make (BatOption.map_default (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ())) (IndexDomain.top_of (Cilfacade.ptrdiff_ikind ())) l) (zero_init_value ai)) - (* | t when is_thread_type t -> `Thread (ConcDomain.ThreadSet.empty ()) *) - | TNamed ({ttype=t; _}, _) -> zero_init_value t - | _ -> `Top + in + `Union(v) + | TArray (ai, None, _) -> + let typAttr = typeAttrs ai in + `Array (CArrays.make ~varAttr ~typAttr (IndexDomain.top_of (Cilfacade.ptrdiff_ikind ())) (zero_init_value ai)) + | TArray (ai, Some exp, _) -> + let typAttr = typeAttrs ai in + let l = BatOption.map Cilint.big_int_of_cilint (Cil.getInteger (Cil.constFold true exp)) in + `Array (CArrays.make ~varAttr ~typAttr (BatOption.map_default (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ())) (IndexDomain.top_of (Cilfacade.ptrdiff_ikind ())) l) (zero_init_value ai)) + (* | t when is_thread_type t -> `Thread (ConcDomain.ThreadSet.empty ()) *) + | TNamed ({ttype=t; _}, _) -> zero_init_value ~varAttr t + | _ -> `Top let tag_name : t -> string = function | `Top -> "Top" | `Int _ -> "Int" | `Float _ -> "Float" | `Address _ -> "Address" | `Struct _ -> "Struct" | `Union _ -> "Union" | `Array _ -> "Array" | `Blob _ -> "Blob" | `Thread _ -> "Thread" | `Mutex -> "Mutex" | `Bot -> "Bot" @@ -436,8 +447,8 @@ struct | `Struct x when same_struct x -> x | `Struct x when ci.cfields <> [] -> let first = List.hd ci.cfields in - Structs.(replace (Structs.create (fun fd -> top_value fd.ftype) ci) first (get x first)) - | _ -> log_top __POS__; Structs.create (fun fd -> top_value fd.ftype) ci + Structs.(replace (Structs.create (fun fd -> top_value ~varAttr:fd.fattr fd.ftype) ci) first (get x first)) + | _ -> log_top __POS__; Structs.create (fun fd -> top_value ~varAttr:fd.fattr fd.ftype) ci ) else `Union (match v with @@ -999,7 +1010,7 @@ struct else begin match offs with | `Field (fldi, _) when fldi.fcomp.cstruct -> - (top_value fld.ftype), offs + (top_value ~varAttr:fld.fattr fld.ftype), offs | `Field (fldi, _) -> `Union (Unions.top ()), offs | `NoOffset -> top (), offs | `Index (idx, _) when Cil.isArrayType fld.ftype -> @@ -1147,20 +1158,22 @@ struct let arbitrary () = QCheck.always `Bot (* S TODO: other elements *) - let rec project p (v: t): t = - match v with - | `Int n -> `Int (ID.project p n) + (*Changes the value: if p is present, change all Integer precisions. If array_attr=(varAttr, typeAttr) is present, change the top level array domain according to the attributes *) + let rec project ask p array_attr (v: t): t = + match v, p, array_attr with + | _, None, None -> v (*Nothing to change*) (* as long as we only have one representation, project is a nop*) - | `Float n -> `Float n - | `Address n -> `Address (project_addr p n) - | `Struct n -> `Struct (Structs.map (fun (x: t) -> project p x) n) - | `Union (f, v) -> `Union (f, project p v) - | `Array n -> `Array (project_arr p n) - | `Blob (v, s, z) -> `Blob (project p v, ID.project p s, z) - | `Thread n -> `Thread n - | `Mutex -> `Mutex - | `Bot -> `Bot - | `Top -> `Top + | `Float n, _, _ -> `Float n + | `Int n, Some p, _-> `Int (ID.project p n) + | `Address n, Some p, _-> `Address (project_addr p n) + | `Struct n, _, _ -> `Struct (Structs.map (fun (x: t) -> project ask p None x) n) + | `Union (f, v), _, _ -> `Union (f, project ask p None v) + | `Array n , _, _ -> `Array (project_arr ask p array_attr n) + | `Blob (v, s, z), Some p', _ -> `Blob (project ask p None v, ID.project p' s, z) + | `Thread n, _, _ -> `Thread n + | `Bot, _, _ -> `Bot + | `Top, _, _ -> `Top + | _, _, _ -> v (*Nothing to change*) and project_addr p a = AD.map (fun addr -> match addr with @@ -1171,11 +1184,15 @@ struct | `NoOffset -> `NoOffset | `Field (field, offs') -> `Field (field, project_offs p offs') | `Index (idx, offs') -> `Index (ID.project p idx, project_offs p offs') - and project_arr p n = - let n' = CArrays.map (fun (x: t) -> project p x) n in - match CArrays.length n with - | None -> n' - | Some l -> CArrays.update_length (ID.project p l) n' + and project_arr ask p array_attr n = + let n = match array_attr with + | Some (varAttr,typAttr) -> CArrays.project ~varAttr ~typAttr ask n + | _ -> n + in let n' = CArrays.map (fun (x: t) -> project ask p None x) n in + match CArrays.length n, p with + | None, _ + | _, None -> n' + | Some l, Some p -> CArrays.update_length (ID.project p l) n' end and Structs: StructDomain.S with type field = fieldinfo and type value = Compound.t = @@ -1184,8 +1201,7 @@ and Structs: StructDomain.S with type field = fieldinfo and type value = Compoun and Unions: UnionDomain.S with type t = UnionDomain.Field.t * Compound.t and type value = Compound.t = UnionDomain.Simple (Compound) -and CArrays: ArrayDomain.S with type value = Compound.t and type idx = ArrIdxDomain.t = - ArrayDomain.FlagConfiguredArrayDomain(Compound)(ArrIdxDomain) +and CArrays: ArrayDomain.S with type value = Compound.t and type idx = ArrIdxDomain.t = ArrayDomain.AttributeConfiguredArrayDomain(Compound)(ArrIdxDomain) and Blobs: Blob with type size = ID.t and type value = Compound.t and type origin = ZeroInit.t = Blob (Compound) (ID) diff --git a/src/goblint.ml b/src/goblint.ml index 343d98fe2d..40cbd1198e 100644 --- a/src/goblint.ml +++ b/src/goblint.ml @@ -58,6 +58,7 @@ let main () = else Analyses.empty_increment_data () in + if get_bool "ana.autotune.enabled" then AutoTune.chooseConfig file; file |> do_analyze changeInfo; do_stats (); do_html_output (); diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 1e9e0125e7..850301ffe8 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -130,7 +130,8 @@ let check_arguments () = (* order matters: non-ptr=false, int=true -> int=false cascades to interval=false with warning *) if get_bool "ana.base.context.interval" && not (get_bool "ana.base.context.int") then (set_bool "ana.base.context.interval" false; warn "ana.base.context.interval implicitly disabled by ana.base.context.int"); if get_bool "incremental.only-rename" then (set_bool "incremental.load" true; warn "incremental.only-rename implicitly activates incremental.load. Previous AST is loaded for diff and rename, but analyis results are not reused."); - if get_bool "incremental.restart.sided.enabled" && get_string_list "incremental.restart.list" <> [] then warn "Passing a non-empty list to incremental.restart.list (manual restarting) while incremental.restart.sided.enabled (automatic restarting) is activated." + if get_bool "incremental.restart.sided.enabled" && get_string_list "incremental.restart.list" <> [] then warn "Passing a non-empty list to incremental.restart.list (manual restarting) while incremental.restart.sided.enabled (automatic restarting) is activated."; + if get_bool "ana.autotune.enabled" && get_bool "incremental.load" then (set_bool "ana.autotune.enabled" false; warn "ana.autotune.enabled implicitly disabled by incremental.load") (** Initialize some globals in other modules. *) let handle_flags () = diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml index ce432eab2a..6421378e33 100644 --- a/src/util/cilfacade.ml +++ b/src/util/cilfacade.ml @@ -58,119 +58,6 @@ let end_basic_blocks f = let thisVisitor = new allBBVisitor in visitCilFileSameGlobals thisVisitor f -(* replaces goto s with goto s' when newtarget s = Some s' IN PLACE *) -class patchLabelsGotosVisitor(newtarget) = object - inherit nopCilVisitor - - method! vstmt s = - match s.skind with - | Goto (target,loc) -> - (match newtarget !target with - | None -> SkipChildren - | Some nt -> s.skind <- Goto (ref nt, loc); DoChildren) - | _ -> DoChildren -end - -(* Hashtable used to patch gotos later *) -module StatementHashTable = Hashtbl.Make(struct - type t = stmt - (* Identity by physical equality. *) - let equal = (==) - let hash = Hashtbl.hash - end) - -(* - Makes a copy, replacing top-level breaks with goto loopEnd and top-level continues with - goto currentIterationEnd - Also assigns fresh names to all labels and patches gotos for labels appearing in the current - fragment to their new name -*) -class copyandPatchLabelsVisitor(loopEnd,currentIterationEnd) = object - inherit nopCilVisitor - - val mutable depth = 0 - val mutable loopNestingDepth = 0 - - val gotos = StatementHashTable.create 20 - - method! vstmt s = - let after x = - depth <- depth-1; - if depth = 0 then - (* the labels can only be patched once the entire part of the AST we want has been transformed, and *) - (* we know all lables appear in the hash table *) - let patchLabelsVisitor = new patchLabelsGotosVisitor(StatementHashTable.find_opt gotos) in - let x = visitCilStmt patchLabelsVisitor x in - StatementHashTable.clear gotos; - x - else - x - in - let rename_labels sn = - let new_labels = List.map (function Label(str,loc,b) -> Label (Cil.freshLabel str,loc,b) | x -> x) sn.labels in - (* this makes new physical copy*) - let new_s = {sn with labels = new_labels} in - if new_s.labels <> [] then - (* Use original s, ns might be temporay e.g. if the type of statement changed *) - (* record that goto s; appearing in the current fragment should later be patched to goto new_s *) - StatementHashTable.add gotos s new_s; - new_s - in - depth <- depth+1; - match s.skind with - | Continue loc -> - if loopNestingDepth = 0 then - (* turn top-level continues into gotos to end of current unrolling *) - ChangeDoChildrenPost(rename_labels {s with skind = Goto (!currentIterationEnd, loc)}, after) - else - ChangeDoChildrenPost(rename_labels s, after) - | Break loc -> - if loopNestingDepth = 0 then - (* turn top-level breaks into gotos to end of current unrolling *) - ChangeDoChildrenPost(rename_labels {s with skind = Goto (loopEnd,loc)}, after) - else - ChangeDoChildrenPost(rename_labels s, after) - | Loop _ -> loopNestingDepth <- loopNestingDepth+1; - ChangeDoChildrenPost(rename_labels s, fun x -> loopNestingDepth <- loopNestingDepth-1; after x) - | _ -> ChangeDoChildrenPost(rename_labels s, after) -end - -class loopUnrollingVisitor = object - (* Labels are simply handled by giving them a fresh name. Jumps coming from outside will still always go to the original label! *) - inherit nopCilVisitor - - method! vstmt s = - match s.skind with - | Loop (b,loc, loc2, break , continue) -> - let duplicate_and_rem_labels s = - match s.skind with - | Loop (b,loc, loc2, break , continue) -> - (* We copy the statement to later be able to modify it without worrying about invariants *) - let s = { s with sid = s.sid } in - let factor = GobConfig.get_int "exp.unrolling-factor" in - (* top-level breaks should immediately go to the end of the loop, and not just break out of the current iteration *) - let break_target = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel "loop_end",loc, true)]} in - (* continues should go to the next unrolling *) - let continue_target i = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel ("loop_continue_" ^ (string_of_int i)),loc, true)]} in - (* passed as a reference so we can reuse the patcher for all unrollings of the current loop *) - let current_continue_target = ref dummyStmt in - let patcher = new copyandPatchLabelsVisitor (ref break_target, ref current_continue_target) in - let one_copy () = visitCilStmt patcher (mkStmt (Block (mkBlock b.bstmts))) in - let copies = List.init (factor) (fun i -> - current_continue_target := continue_target i; - mkStmt (Block (mkBlock [one_copy (); !current_continue_target]))) - in - mkStmt (Block (mkBlock (copies@[s]@[break_target]))) - | _ -> failwith "invariant broken" - in - ChangeDoChildrenPost({s with sid = s.sid},duplicate_and_rem_labels) - | _ -> DoChildren -end - -let loop_unrolling fd = - let thisVisitor = new loopUnrollingVisitor in - ignore (visitCilFunction thisVisitor fd) - let visitors = ref [] let register_preprocess name visitor_fun = visitors := !visitors @ [name, visitor_fun] @@ -183,6 +70,8 @@ let do_preprocess ast = in iterGlobals ast (function GFun (fd,_) -> List.iter (f fd) !visitors | _ -> ()) + + let createCFG (fileAST: file) = (* The analyzer keeps values only for blocks. So if you want a value for every program point, each instruction *) (* needs to be in its own block. end_basic_blocks does that. *) @@ -201,13 +90,14 @@ let createCFG (fileAST: file) = match glob with | GFun(fd,_) -> (* before prepareCfg so continues still appear as such *) - if (get_int "exp.unrolling-factor")>0 then loop_unrolling fd; + if (get_int "exp.unrolling-factor")>0 || AutoTune0.isActivated "loopUnrollHeuristic" then LoopUnrolling.unroll_loops fd; prepareCFG fd; computeCFGInfo fd true | _ -> () ); do_preprocess fileAST + let getAST fileName = let fileAST = parse fileName in (* rmTemps fileAST; *) diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml new file mode 100644 index 0000000000..7ad59e379d --- /dev/null +++ b/src/util/loopUnrolling.ml @@ -0,0 +1,473 @@ +open GobConfig +open GoblintCil + +(*loop unroll heuristics*) +(*used if AutoTune is activated*) + +(*simple fixed loop iterations: + - one single break with a comparison of a single integral local variable against a constant + - before the loop the variable is assigned a constant (or never assigned) + - only one assign to this variable inside the loop with a fixed difference to before + - no pointer to this variable is used (to make the last two things checkable) + + We can't use succs/preds, because they get computed with the CFG, and the loop unrolling has to happen before + TODO: gotos inside the loop could make the iteration not fixed, but are ignored for now +*) + +(*exceptions to break out of visitors. two to make purpose clear*) +exception WrongOrMultiple +exception Found +class checkNoBreakVisitor = object + inherit nopCilVisitor + + method! vstmt stmt = + match stmt.skind with + | Loop _ + | Switch _ -> SkipChildren (*Breaks in inner loops/switch are fine*) + | Break _ -> raise WrongOrMultiple + | _ -> DoChildren + +end + +let checkNoBreakStmt stmt = + let visitor = new checkNoBreakVisitor in + ignore @@ visitCilStmt visitor stmt + +let checkNoBreakBlock block = + let visitor = new checkNoBreakVisitor in + ignore @@ visitCilBlock visitor block + +class findBreakVisitor(compOption: exp option ref) = object + inherit nopCilVisitor + + method! vstmt stmt = + match stmt.skind with + | Block _ -> DoChildren + | Break _ -> raise WrongOrMultiple + | If (cond, t, e, _, _) -> ( + checkNoBreakBlock t; + match e.bstmts with + | [s] -> ( + match s.skind with + | Break _ -> ( + match !compOption with + | Some _ -> raise WrongOrMultiple (*more than one loop break*) + | _ -> compOption := Some cond; SkipChildren + ) + | _ -> checkNoBreakStmt stmt; SkipChildren + ) + | _ -> checkNoBreakStmt stmt; SkipChildren + ) + | _ -> SkipChildren + +end + +class isPointedAtVisitor(var) = object + inherit nopCilVisitor + + method! vexpr = function + | AddrOf (Var info, NoOffset) when info.vid == var.vid -> raise Found + | _ -> DoChildren +end + +class hasAssignmentVisitor(var) = object + inherit nopCilVisitor + + method! vinst = function + | Set ((Var info, NoOffset),_,_,_) when info.vid == var.vid -> raise Found + | _ -> SkipChildren +end + +let hasAssignmentTo var block = try + let visitor = new hasAssignmentVisitor(var) in + ignore @@ visitCilBlock visitor block; + false + with | Found -> true + +class findAssignmentConstDiff((diff: Z.t option ref), var) = object + inherit nopCilVisitor + + method! vstmt stmt = match stmt.skind with + | Instr _ + | Block _ -> DoChildren + | Loop (b,_,_,_,_) -> if hasAssignmentTo var b then raise WrongOrMultiple else SkipChildren + | If (_, t, e, _, _) -> + if hasAssignmentTo var t || hasAssignmentTo var t then + raise WrongOrMultiple + else SkipChildren + | Switch (_,b,_,_,_) -> + if hasAssignmentTo var b then + raise WrongOrMultiple + else SkipChildren + | _ -> SkipChildren + + method! vinst = function + | Set ((Var v, NoOffset), BinOp (PlusA, Const (CInt (cint,_,_)), Lval (Var v2, NoOffset), _ ),_,_) + | Set ((Var v, NoOffset), BinOp (PlusA, Lval (Var v2, NoOffset), Const (CInt (cint,_,_)), _ ),_,_) when v.vid = var.vid && v2.vid = var.vid -> + ( match !diff with + | Some _ -> raise WrongOrMultiple + | _ -> diff := Some (Cilint.big_int_of_cilint cint); SkipChildren + ) + | Set ((Var v, NoOffset), BinOp (MinusA, Lval (Var v2, NoOffset), Const (CInt (cint,_,_)), _ ),_,_) when v.vid = var.vid && v2.vid = var.vid -> + ( match !diff with + | Some _ -> raise WrongOrMultiple + | _ -> diff := Some (Z.neg (Cilint.big_int_of_cilint cint)); SkipChildren + ) + | Set ((Var v, NoOffset), _,_,_) when v.vid = var.vid -> raise WrongOrMultiple + | _ -> SkipChildren +end + +let isCompare = function + | Lt | Gt | Le | Ge | Ne -> true (*an loop that test for equality can not be of the type we look for*) + | _ -> false + +let loopBody loopStatement = match loopStatement.skind with + | Loop (b,_,_,_,_) -> b + | _ -> failwith "loopBody on non loop" +let loopLocation loopStatement = match loopStatement.skind with + | Loop (_,l,_,_,_) -> l + | _ -> failwith "loopLocation on non loop" + +type assignment = + | NoAssign + | Const of Z.t + | Other + +let classifyInstruction var = function + | Set (((Var info), NoOffset), Const(CInt (i,_,_)), _,_) when info.vid = var.vid -> Const (Cilint.big_int_of_cilint i) + | Set (((Var info), NoOffset), _ , _,_) when info.vid = var.vid -> Other + | _ -> NoAssign + +let lastAssignToVar var insList = + let reverse = List.rev_map (classifyInstruction var) insList in + let rec firstAssign = function + | NoAssign::rest -> firstAssign rest + | s::_ -> s + | [] -> NoAssign + in firstAssign reverse + +(*find the last assignment to var before loop in f*) +(*return it if it is a constant and not inside a conditional branch*) +let constBefore var loop f = + let targetLocation = loopLocation loop + in let rec lastAssignmentToVarBeforeLoop (current: (Z.t option)) (statements: stmt list) = match statements with + | st::stmts -> ( + let current' = if st.labels <> [] then (print_endline "has Label"; (None)) else current in + match st.skind with + | Instr list -> ( + match lastAssignToVar var list with + | NoAssign -> lastAssignmentToVarBeforeLoop current' stmts + | Other -> lastAssignmentToVarBeforeLoop (None) stmts + | Const i -> lastAssignmentToVarBeforeLoop (Some i) stmts + ) + | If (_, t, e, _, _) -> ( + match lastAssignmentToVarBeforeLoop current' t.bstmts with + | (_, false) -> ( + match lastAssignmentToVarBeforeLoop current' e.bstmts with + | (_, false) -> (*neither the then nor the else part contain loop*) + if hasAssignmentTo var t || hasAssignmentTo var e then + lastAssignmentToVarBeforeLoop (None) stmts (*because we do not know which path has been taken, invalidate previous assignment*) + else + lastAssignmentToVarBeforeLoop (current') stmts + | c -> c + ) + | c -> c + ) + | Loop (block, loc,_,_,_) -> ( + if CilType.Location.equal loc targetLocation then ( (*sid is not initialised at this point-> use location to identify loop*) + (current', true) (*Stop iteration at the searched for loop*) + ) else + match lastAssignmentToVarBeforeLoop current' block.bstmts with + | (_, false) -> ( + if hasAssignmentTo var block then + lastAssignmentToVarBeforeLoop (None) stmts + else + lastAssignmentToVarBeforeLoop (current') stmts + ) + | c -> c + ) + | Block block -> + let (l, f) = lastAssignmentToVarBeforeLoop current' block.bstmts in + if f then + (l,f) + else + lastAssignmentToVarBeforeLoop l stmts + | Switch (_, block, _,_,_) -> ( + match lastAssignmentToVarBeforeLoop current' block.bstmts with + | (_, false) -> ( + if hasAssignmentTo var block then + lastAssignmentToVarBeforeLoop (None) stmts + else + lastAssignmentToVarBeforeLoop (current') stmts + ) + | c -> c + ) + | _-> lastAssignmentToVarBeforeLoop (None) stmts (*the control flow could only go further if a goto jumps to this*) + ) + | [] -> (current, false) (*we did not have the loop inside these statements*) + in + fst @@ lastAssignmentToVarBeforeLoop (Some Z.zero) f.sbody.bstmts (*the top level call should never return false*) + +let rec loopIterations start diff comp = + let flip = function + | Lt -> Gt + | Gt -> Lt + | Ge -> Le + | Le -> Ge + | s -> s + in let loopIterations' goal shouldBeExact = + let range = Z.sub goal start in + if Z.equal diff Z.zero || Z.equal range Z.zero || (Z.gt diff Z.zero && Z.lt range Z.zero) || (Z.lt diff Z.zero && Z.gt range Z.zero) then + None (*unfitting parameters*) + else ( + let roundedDown = Z.div range diff in + let isExact = Z.equal (Z.mul roundedDown diff) range in + if isExact then + Some roundedDown + else if shouldBeExact then + None + else + Some (Z.add roundedDown Z.one) + ) + in + match comp with + | BinOp (op, (Const _ as c), var, t) -> loopIterations start diff (BinOp (flip op, var, c, t)) + | BinOp (Lt, _, (Const (CInt (cint,_,_) )), _) -> if Z.lt diff Z.zero then None else loopIterations' (Cilint.big_int_of_cilint cint) false + | BinOp (Gt, _, (Const (CInt (cint,_,_) )), _) -> if Z.gt diff Z.zero then None else loopIterations' (Cilint.big_int_of_cilint cint) false + | BinOp (Le, _, (Const (CInt (cint,_,_) )), _) -> if Z.lt diff Z.zero then None else loopIterations' (Z.add Z.one @@ Cilint.big_int_of_cilint cint) false + | BinOp (Ge, _, (Const (CInt (cint,_,_) )), _) -> if Z.gt diff Z.zero then None else loopIterations' (Z.pred @@ Cilint.big_int_of_cilint cint ) false + | BinOp (Ne, _, (Const (CInt (cint,_,_) )), _) -> loopIterations' (Cilint.big_int_of_cilint cint) true + | _ -> failwith "unexpected comparison in loopIterations" + +let ( >>= ) = Option.bind +let fixedLoopSize loopStatement func = + let findBreakComparison = try (*find a single break in the else branch of a toplevel if*) + let compOption = ref None in + let visitor = new findBreakVisitor(compOption) in + ignore @@ visitCilBlock visitor (loopBody loopStatement); + !compOption + with | WrongOrMultiple -> None + in let getLoopVar = function + | BinOp (op, (Const (CInt _ )), Lval ((Var info), NoOffset), (TInt _)) + | BinOp (op, Lval ((Var info), NoOffset), (Const (CInt _ )), (TInt _)) when isCompare op && not info.vglob-> + Some info + | _ -> None + in let getsPointedAt var = try + let visitor = new isPointedAtVisitor(var) in + ignore @@ visitCilFunction visitor func; + false + with | Found -> true + in let assignmentDifference loop var = try + let diff = ref None in + let visitor = new findAssignmentConstDiff(diff, var) in + ignore @@ visitCilStmt visitor loop; + !diff + with | WrongOrMultiple -> None + in + + findBreakComparison >>= fun comparison -> + getLoopVar comparison >>= fun var -> + if getsPointedAt var then + None + else + constBefore var loopStatement func >>= fun start -> + assignmentDifference loopStatement var >>= fun diff -> + print_endline "comparison: "; + Pretty.fprint stdout (dn_exp () comparison) ~width:50; + print_endline ""; + print_endline "variable: "; + print_endline var.vname; + print_endline "start:"; + print_endline @@ Z.to_string start; + print_endline "diff:"; + print_endline @@ Z.to_string diff; + let iterations = loopIterations start diff comparison in + match iterations with + | None -> print_endline "iterations failed"; None + | Some s -> + try + let s' = Z.to_int s in + print_endline "iterations:"; + print_endline @@ string_of_int s'; + Some s' + with _ -> print_endline "iterations too big for integer"; None + + +class arrayVisitor = object + inherit nopCilVisitor + + method! vvrbl info = + if not @@ (hasAttribute "goblint_array_domain" info.vattr || AutoTune0.is_large_array info.vtype) then + info.vattr <- addAttribute (Attr ("goblint_array_domain", [AStr "unroll"]) ) info.vattr; + DoChildren +end +let annotateArrays loopBody = ignore @@ visitCilBlock (new arrayVisitor) loopBody + +(*unroll loops that handle locks, threads and mallocs, asserts and reach_error*) +class loopUnrollingCallVisitor = object + inherit nopCilVisitor + + method! vinst = function + | Call (_,Lval ((Var info), NoOffset),args,_,_) -> ( + let desc = LibraryFunctions.find info in + match desc.special args with + | Malloc _ + | Calloc _ + | Realloc _ + | Lock _ + | Unlock _ + | ThreadCreate _ + | Assert _ + | ThreadJoin _ -> + raise Found; + | _ -> + if List.mem "specification" @@ get_string_list "ana.autotune.activated" && get_string "ana.specification" <> "" then ( + match SvcompSpec.of_option () with + | UnreachCall s -> if info.vname = s then raise Found + | _ -> () + ); + DoChildren + ) + | _ -> DoChildren + +end + +let loop_unrolling_factor loopStatement func = + let configFactor = get_int "exp.unrolling-factor" in + let unrollFunctionCalled = try + let thisVisitor = new loopUnrollingCallVisitor in + ignore (visitCilStmt thisVisitor loopStatement); + false; + with + Found -> true + in + (*unroll up to near an instruction count, higher if the loop uses malloc/lock/threads *) + let targetInstructions = if unrollFunctionCalled then 50 else 25 in + let loopStats = AutoTune0.collectFactors visitCilStmt loopStatement in + let targetFactor = if loopStats.instructions > 0 then targetInstructions / loopStats.instructions else 0 in (* Don't unroll empty (= while(1){}) loops*) + let fixedLoop = fixedLoopSize loopStatement func in + if AutoTune0.isActivated "loopUnrollHeuristic" then + match fixedLoop with + | Some i -> if i * loopStats.instructions < 100 then (print_endline "fixed loop size"; i) else 100 / loopStats.instructions + | _ -> targetFactor + else + configFactor + +(*actual loop unrolling*) + +(* Hashtable used to patch gotos later *) +module StatementHashTable = Hashtbl.Make(struct + type t = stmt + (* Identity by physical equality. *) + let equal = (==) + let hash = Hashtbl.hash + end) + +(* replaces goto s with goto s' when newtarget s = Some s' IN PLACE *) +class patchLabelsGotosVisitor(newtarget) = object + inherit nopCilVisitor + + method! vstmt s = + match s.skind with + | Goto (target,loc) -> + (match newtarget !target with + | None -> SkipChildren + | Some nt -> s.skind <- Goto (ref nt, loc); DoChildren) + | _ -> DoChildren +end + +(* + Makes a copy, replacing top-level breaks with goto loopEnd and top-level continues with + goto currentIterationEnd + Also assigns fresh names to all labels and patches gotos for labels appearing in the current + fragment to their new name +*) +class copyandPatchLabelsVisitor(loopEnd,currentIterationEnd) = object + inherit nopCilVisitor + + val mutable depth = 0 + val mutable loopNestingDepth = 0 + + val gotos = StatementHashTable.create 20 + + method! vstmt s = + let after x = + depth <- depth-1; + if depth = 0 then + (* the labels can only be patched once the entire part of the AST we want has been transformed, and *) + (* we know all lables appear in the hash table *) + let patchLabelsVisitor = new patchLabelsGotosVisitor(StatementHashTable.find_opt gotos) in + let x = visitCilStmt patchLabelsVisitor x in + StatementHashTable.clear gotos; + x + else + x + in + let rename_labels sn = + let new_labels = List.map (function Label(str,loc,b) -> Label (Cil.freshLabel str,loc,b) | x -> x) sn.labels in + (* this makes new physical copy*) + let new_s = {sn with labels = new_labels} in + if new_s.labels <> [] then + (* Use original s, ns might be temporay e.g. if the type of statement changed *) + (* record that goto s; appearing in the current fragment should later be patched to goto new_s *) + StatementHashTable.add gotos s new_s; + new_s + in + depth <- depth+1; + match s.skind with + | Continue loc -> + if loopNestingDepth = 0 then + (* turn top-level continues into gotos to end of current unrolling *) + ChangeDoChildrenPost(rename_labels {s with skind = Goto (!currentIterationEnd, loc)}, after) + else + ChangeDoChildrenPost(rename_labels s, after) + | Break loc -> + if loopNestingDepth = 0 then + (* turn top-level breaks into gotos to end of current unrolling *) + ChangeDoChildrenPost(rename_labels {s with skind = Goto (loopEnd,loc)}, after) + else + ChangeDoChildrenPost(rename_labels s, after) + | Loop _ -> loopNestingDepth <- loopNestingDepth+1; + ChangeDoChildrenPost(rename_labels s, fun x -> loopNestingDepth <- loopNestingDepth-1; after x) + | _ -> ChangeDoChildrenPost(rename_labels s, after) +end + +class loopUnrollingVisitor(func) = object + (* Labels are simply handled by giving them a fresh name. Jumps coming from outside will still always go to the original label! *) + inherit nopCilVisitor + + method! vstmt s = + match s.skind with + | Loop (b,loc, loc2, break , continue) -> + let duplicate_and_rem_labels s = + let factor = loop_unrolling_factor s func in + if(factor > 0) then ( + print_endline @@ "unrolling loop at " ^ CilType.Location.show loc ^" with factor " ^ string_of_int factor; + annotateArrays b; + match s.skind with + | Loop (b,loc, loc2, break , continue) -> + (* We copy the statement to later be able to modify it without worrying about invariants *) + let s = { s with sid = s.sid } in + + (* top-level breaks should immediately go to the end of the loop, and not just break out of the current iteration *) + let break_target = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel "loop_end",loc, true)]} in + (* continues should go to the next unrolling *) + let continue_target i = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel ("loop_continue_" ^ (string_of_int i)),loc, true)]} in + (* passed as a reference so we can reuse the patcher for all unrollings of the current loop *) + let current_continue_target = ref dummyStmt in + let patcher = new copyandPatchLabelsVisitor (ref break_target, ref current_continue_target) in + let one_copy () = visitCilStmt patcher (mkStmt (Block (mkBlock b.bstmts))) in + let copies = List.init (factor) (fun i -> + current_continue_target := continue_target i; + mkStmt (Block (mkBlock [one_copy (); !current_continue_target]))) + in + mkStmt (Block (mkBlock (copies@[s]@[break_target]))) + | _ -> failwith "invariant broken" + ) else s (*no change*) + in ChangeDoChildrenPost({s with sid = s.sid},duplicate_and_rem_labels); + | _ -> DoChildren +end + +let unroll_loops fd = + let thisVisitor = new loopUnrollingVisitor(fd) in + ignore (visitCilFunction thisVisitor fd) \ No newline at end of file diff --git a/src/util/options.schema.json b/src/util/options.schema.json index 548e4203d2..251b6e90a4 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -389,6 +389,14 @@ "Use constants appearing in program as threshold for widening", "type": "boolean", "default": false + }, + "interval_threshold_widening_constants": { + "title": "ana.int.interval_threshold_widening_constants", + "description": + "Which constants in the program should be considered as threshold constants (all/comparisons)", + "type": "string", + "enum": ["all", "comparisons"], + "default": "all" } }, "additionalProperties": false @@ -482,6 +490,28 @@ }, "additionalProperties": false }, + "autotune": { + "title": "ana.autotune", + "type": "object", + "properties": { + "enabled": { + "title": "ana.autotune.enabled", + "description": "Try to intelligently select analyses based on analysed file", + "type": "boolean", + "default": false + }, + "activated": { + "title": "ana.autotune.activated", + "description": "Lists of activated tuning options. By default all are activated", + "type": "array", + "items": { "type": "string" }, + "default": [ + "congruence", "singleThreaded", "specification", "mallocWrappers", "noRecursiveIntervals", "enums", "loopUnrollHeuristic", "arrayDomain", "octagon", "wideningThresholds" + ] + } + }, + "additionalProperties": false + }, "sv-comp": { "title": "ana.sv-comp", "type": "object", @@ -762,6 +792,14 @@ "type": "boolean", "default": false }, + "threshold_widening_constants": { + "title": "ana.apron.threshold_widening_constants", + "description": + "Which constants in the programm should be considered as threshold constants", + "type": "string", + "enum": ["all", "comparisons"], + "default": "all" + }, "privatization": { "title": "ana.apron.privatization", "description": @@ -1284,7 +1322,7 @@ "enabled": { "title": "annotation.int.enabled", "description": - "Enable manual annotation of functions with desired precision, i.e. the activated IntDomains.", + "Enable manual annotation of functions with desired precision, i.e., the activated IntDomains.", "type": "boolean", "default": false }, @@ -1305,7 +1343,7 @@ "enabled": { "title": "annotation.float.enabled", "description": - "Enable manual annotation of functions with desired precision, i.e. the activated FloatDomains.", + "Enable manual annotation of functions with desired precision, i.e., the activated FloatDomains.", "type": "boolean", "default": false } @@ -1335,6 +1373,18 @@ }, "default": [] } + }, + "goblint_array_domain": { + "title": "annotation.goblint_array_domain", + "description": "Enable manual annotation of arrays with desired domain", + "type": "boolean", + "default": false + }, + "goblint_apron_track": { + "title": "annotation.goblint_apron_track", + "description": "Let apron track variables only if they have the attribute goblint_apron_track", + "type": "boolean", + "default": false } }, "additionalProperties": false diff --git a/src/util/server.ml b/src/util/server.ml index 13a9cb738a..ecf02a25e9 100644 --- a/src/util/server.ml +++ b/src/util/server.ml @@ -192,6 +192,7 @@ let analyze ?(reset=false) (s: t) = WideningThresholds.reset_lazy (); IntDomain.reset_lazy (); ApronDomain.reset_lazy (); + AutoTune.reset_lazy (); Access.reset (); s.file <- Some file; GobConfig.set_bool "incremental.load" (not fresh); diff --git a/src/util/wideningThresholds.ml b/src/util/wideningThresholds.ml index 5e4c4dcad2..5553f3159d 100644 --- a/src/util/wideningThresholds.ml +++ b/src/util/wideningThresholds.ml @@ -1,6 +1,89 @@ open GoblintCil +open Batteries module Thresholds = Set.Make(Z) +(* Collect only constants that are used in comparisons *) +(* For widening we want to have the tightest representation that includes the exit condition *) +(* differentiating between upper and lower bounds, because e.g. expr > 10 is definitely true for an interval [11, x] and definitely false for an interval [x, 10] *) +(* apron octagons use thresholds for c in inequalities +/- x +/- y <= c *) +let addThreshold t_ref z = t_ref := Thresholds.add z !t_ref +let one = Z.of_int 1 + +class extractThresholdsFromConditionsVisitor(upper_thresholds,lower_thresholds, octagon_thresholds) = object + inherit nopCilVisitor + + method! vexpr = function + (* Comparisons of type: 10 <= expr, expr >= 10, expr < 10, 10 > expr *) + | BinOp (Le, (Const (CInt(i,_,_))), _, (TInt _)) + | BinOp (Ge, _, (Const (CInt(i,_,_))), (TInt _)) + | BinOp (Lt, _, (Const (CInt(i,_,_))), (TInt _)) + | BinOp (Gt, (Const (CInt(i,_,_))), _, (TInt _)) -> + addThreshold upper_thresholds @@ i; + addThreshold lower_thresholds @@ Z.sub i one; + + let negI = Z.add one @@ Z.neg i in + addThreshold octagon_thresholds @@ i; (* upper, just large enough: x + Y <= i *) + addThreshold octagon_thresholds @@ negI; (* lower, just small enough: -X -Y <= -i+1 -> X + Y >= i-1 -> X + Y >= i-1 *) + addThreshold octagon_thresholds @@ Z.add i i; (* double upper: X + X <= 2i -> X <= i *) + addThreshold octagon_thresholds @@ Z.add negI negI; (* double lower: -X -X <= -2i -> X >= i *) + DoChildren + + (* Comparisons of type: 10 < expr, expr > 10, expr <= 10, 10 >= expr *) + | BinOp (Lt, (Const (CInt(i,_,_))), _, (TInt _)) + | BinOp (Gt, _, (Const (CInt(i,_,_))), (TInt _)) + | BinOp (Le, _, (Const (CInt(i,_,_))), (TInt _)) + | BinOp (Ge, (Const (CInt(i,_,_))), _, (TInt _)) -> + let i = Z.add i one in (* The same as above with i+1 because for integers expr <= 10 <=> expr < 11 *) + addThreshold upper_thresholds @@ i; + addThreshold lower_thresholds @@ Z.sub i one; + + let negI = Z.add one @@ Z.neg i in + addThreshold octagon_thresholds @@ i; + addThreshold octagon_thresholds @@ negI; + addThreshold octagon_thresholds @@ Z.add i i; + addThreshold octagon_thresholds @@ Z.add negI negI; + DoChildren + + (* Comparisons of type: 10 == expr, expr == 10, expr != 10, 10 != expr *) + | BinOp (Eq, (Const (CInt(i,_,_))), _, (TInt _)) + | BinOp (Eq, _, (Const (CInt(i,_,_))), (TInt _)) + | BinOp (Ne, _, (Const (CInt(i,_,_))), (TInt _)) + | BinOp (Ne, (Const (CInt(i,_,_))), _, (TInt _)) -> + addThreshold upper_thresholds @@ i; + addThreshold lower_thresholds @@ i; + + addThreshold octagon_thresholds @@ i; + addThreshold octagon_thresholds @@ Z.neg i; + let doubleI = Z.add i i in + addThreshold octagon_thresholds @@ doubleI; + addThreshold octagon_thresholds @@ Z.neg doubleI; + DoChildren + | _ -> DoChildren +end + +let default_thresholds = Thresholds.of_list ( + let thresh_pos = List.map (Int.pow 2) [0;2;4;8;16;32;48] in + let thresh_neg = List.map (fun x -> -x) thresh_pos in + List.map Z.of_int (thresh_neg @ thresh_pos @ [0]) + ) + +let conditional_widening_thresholds = ResettableLazy.from_fun (fun () -> + let upper = ref default_thresholds in + let lower = ref default_thresholds in + let octagon = ref default_thresholds in + let thisVisitor = new extractThresholdsFromConditionsVisitor(upper,lower,octagon) in + visitCilFileSameGlobals thisVisitor (!Cilfacade.current_file); + Thresholds.elements !upper, List.rev (Thresholds.elements !lower), Thresholds.elements !octagon ) + +let upper_thresholds () = + let (u,_,_) = ResettableLazy.force conditional_widening_thresholds in u + +let lower_thresholds () = + let (_,l,_) = ResettableLazy.force conditional_widening_thresholds in l + +let octagon_thresholds () = + let (_,_,o) = ResettableLazy.force conditional_widening_thresholds in o + class extractConstantsVisitor(widening_thresholds,widening_thresholds_incl_mul2) = object inherit nopCilVisitor @@ -19,11 +102,11 @@ class extractConstantsVisitor(widening_thresholds,widening_thresholds_incl_mul2) end let widening_thresholds = ResettableLazy.from_fun (fun () -> - let set = ref Thresholds.empty in - let set_incl_mul2 = ref Thresholds.empty in - let thisVisitor = new extractConstantsVisitor(set,set_incl_mul2) in - visitCilFileSameGlobals thisVisitor (!Cilfacade.current_file); - Thresholds.elements !set, Thresholds.elements !set_incl_mul2) + let set = ref Thresholds.empty in + let set_incl_mul2 = ref Thresholds.empty in + let thisVisitor = new extractConstantsVisitor(set,set_incl_mul2) in + visitCilFileSameGlobals thisVisitor (!Cilfacade.current_file); + Thresholds.elements !set, Thresholds.elements !set_incl_mul2) let thresholds () = fst @@ ResettableLazy.force widening_thresholds @@ -69,4 +152,5 @@ let exps = ResettableLazy.from_fun (fun () -> let reset_lazy () = ResettableLazy.reset widening_thresholds; + ResettableLazy.reset conditional_widening_thresholds; ResettableLazy.reset exps diff --git a/src/util/wideningThresholds.mli b/src/util/wideningThresholds.mli index a4c093c80c..df58fed65b 100644 --- a/src/util/wideningThresholds.mli +++ b/src/util/wideningThresholds.mli @@ -3,3 +3,6 @@ val thresholds_incl_mul2 : unit -> Z.t list val exps: GoblintCil.exp list ResettableLazy.t val reset_lazy : unit -> unit +val upper_thresholds : unit -> Z.t list +val lower_thresholds : unit -> Z.t list +val octagon_thresholds : unit -> Z.t list \ No newline at end of file diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml index 5208336704..d5fdac4859 100644 --- a/src/witness/svcomp.ml +++ b/src/witness/svcomp.ml @@ -1,51 +1,7 @@ open GoblintCil open Batteries -module Specification = -struct - type t = - | UnreachCall of string - | NoDataRace - | NoOverflow - - let of_string s = - let s = String.strip s in - let regexp = Str.regexp "CHECK( init(main()), LTL(G ! \\(.*\\)) )" in - if Str.string_match regexp s 0 then - let global_not = Str.matched_group 1 s in - if global_not = "data-race" then - NoDataRace - else if global_not = "overflow" then - NoOverflow - else - let call_regex = Str.regexp "call(\\(.*\\)())" in - if Str.string_match call_regex global_not 0 then - let f = Str.matched_group 1 global_not in - UnreachCall f - else - failwith "Svcomp.Specification.of_string: unknown global not expression" - else - failwith "Svcomp.Specification.of_string: unknown expression" - - let of_file path = - let s = BatFile.with_file_in path BatIO.read_all in - of_string s - - let of_option () = - let s = GobConfig.get_string "ana.specification" in - if Sys.file_exists s then - of_file s - else - of_string s - - let to_string spec = - let global_not = match spec with - | UnreachCall f -> "call(" ^ f ^ "())" - | NoDataRace -> "data-race" - | NoOverflow -> "overflow" - in - "CHECK( init(main()), LTL(G ! " ^ global_not ^ ") )" -end +module Specification = SvcompSpec module type Task = sig diff --git a/src/witness/svcompSpec.ml b/src/witness/svcompSpec.ml new file mode 100644 index 0000000000..9d5615da62 --- /dev/null +++ b/src/witness/svcompSpec.ml @@ -0,0 +1,45 @@ +open GoblintCil +open Batteries + +type t = + | UnreachCall of string + | NoDataRace + | NoOverflow + +let of_string s = + let s = String.strip s in + let regexp = Str.regexp "CHECK( init(main()), LTL(G ! \\(.*\\)) )" in + if Str.string_match regexp s 0 then + let global_not = Str.matched_group 1 s in + if global_not = "data-race" then + NoDataRace + else if global_not = "overflow" then + NoOverflow + else + let call_regex = Str.regexp "call(\\(.*\\)())" in + if Str.string_match call_regex global_not 0 then + let f = Str.matched_group 1 global_not in + UnreachCall f + else + failwith "Svcomp.Specification.of_string: unknown global not expression" + else + failwith "Svcomp.Specification.of_string: unknown expression" + +let of_file path = + let s = BatFile.with_file_in path BatIO.read_all in + of_string s + +let of_option () = + let s = GobConfig.get_string "ana.specification" in + if Sys.file_exists s then + of_file s + else + of_string s + +let to_string spec = + let global_not = match spec with + | UnreachCall f -> "call(" ^ f ^ "())" + | NoDataRace -> "data-race" + | NoOverflow -> "overflow" + in + "CHECK( init(main()), LTL(G ! " ^ global_not ^ ") )" diff --git a/tests/regression/54-unroll_arrays/03-large_index_type.c b/tests/regression/54-unroll_arrays/03-large_index_type.c index d2e902be83..91c8056b32 100644 --- a/tests/regression/54-unroll_arrays/03-large_index_type.c +++ b/tests/regression/54-unroll_arrays/03-large_index_type.c @@ -3,7 +3,7 @@ typedef long unsigned int size_t; -int main() { +int main() { int d[]; size_t num_uint64s; diff --git a/tests/regression/54-unroll_arrays/04-access_no_bounds.c b/tests/regression/54-unroll_arrays/04-access_no_bounds.c index d0a5634b53..70a2726045 100644 --- a/tests/regression/54-unroll_arrays/04-access_no_bounds.c +++ b/tests/regression/54-unroll_arrays/04-access_no_bounds.c @@ -18,7 +18,7 @@ static const uint8_t s_tolower_table[256] = { 220, 221, 222, 223, 224, 225, 226, 227, 228, 229, 230, 231, 232, 233, 234, 235, 236, 237, 238, 239, 240, 241, 242, 243, 244, 245, 246, 247, 248, 249, 250, 251, 252, 253, 254, 255}; -int main() { +int main() { size_t array_len = 10; void *array = malloc(array_len); @@ -31,4 +31,4 @@ int main() { } } -} \ No newline at end of file +} diff --git a/tests/regression/60-array_annotations/01-var_array_annotation.c b/tests/regression/60-array_annotations/01-var_array_annotation.c new file mode 100644 index 0000000000..5a209f1f3e --- /dev/null +++ b/tests/regression/60-array_annotations/01-var_array_annotation.c @@ -0,0 +1,20 @@ +// PARAM: --set ana.base.arrays.unrolling-factor 4 --enable annotation.goblint_array_domain + + +int main(void); + +int main(void) +{ + int x[4] __attribute__((goblint_array_domain("unroll"))); + + x[0] = 0; + x[1] = 1; + x[2] = 2; + x[3] = 3; + + __goblint_check(x[0] == 0); + __goblint_check(x[1] == 1); + __goblint_check(x[2] == 2); + __goblint_check(x[3] == 3); + +} diff --git a/tests/regression/60-array_annotations/02-function_array_annotation.c b/tests/regression/60-array_annotations/02-function_array_annotation.c new file mode 100644 index 0000000000..9a9d368bf3 --- /dev/null +++ b/tests/regression/60-array_annotations/02-function_array_annotation.c @@ -0,0 +1,31 @@ +// PARAM: --set ana.base.arrays.unrolling-factor 4 --enable annotation.goblint_array_domain + + +int main(void); + +void test(int x[4] __attribute__((goblint_array_domain("unroll")))){ + x[0] = 0; + x[1] = 1; + x[2] = 2; + x[3] = 3; + + __goblint_check(x[0] == 0); + __goblint_check(x[1] == 1); + __goblint_check(x[2] == 2); + __goblint_check(x[3] == 3); + +} + +int main(void) +{ + int z[4] __attribute__((goblint_array_domain("unroll"))) ; + + test(z); + + __goblint_check(z[0] == 0); + + __goblint_check(z[0] == 0); + __goblint_check(z[1] == 1); + __goblint_check(z[2] == 2); + __goblint_check(z[3] == 3); +} diff --git a/tests/regression/60-array_annotations/03-change_domain_array_annotation.c b/tests/regression/60-array_annotations/03-change_domain_array_annotation.c new file mode 100644 index 0000000000..6f8015edf3 --- /dev/null +++ b/tests/regression/60-array_annotations/03-change_domain_array_annotation.c @@ -0,0 +1,62 @@ +// PARAM: --set ana.base.arrays.unrolling-factor 5 --enable annotation.goblint_array_domain --enable ana.int.interval + + +int main(void); + +void test(int x[] __attribute__((goblint_array_domain("unroll")))){ + + x[0] = 0; + x[1] = 1; + x[2] = 2; + x[3] = 3; + + __goblint_check(x[0] == 0); + __goblint_check(x[1] == 1); + __goblint_check(x[2] == 2); + __goblint_check(x[3] == 3); + +} + +void partitioned(int* a __attribute__((goblint_array_domain("partitioned")))){ + + int i = 0; + + while(i < 42) { + a[i] = 4; + i++; + } + + __goblint_check(a[3] == 4); + + i = 0; + while(i<10) { + a[i] = -1; + i++; + } + + __goblint_check(a[3] == -1); + __goblint_check(a[i] == 4); + __goblint_check(a[i+5] == 4); + +} + +int main(void) +{ + int z[4] __attribute__((goblint_array_domain("trivial"))); + + test(z); + + __goblint_check(z[0] == 0); // UNKNOWN + + int a[42] __attribute__((goblint_array_domain("unroll"))); + + a[0] = 0; + a[4] = 4; + a[10] = 10; + a[11] = 11; + + __goblint_check(a[4] == 4); + __goblint_check(a[10] == 10); //UNKNOWN + + partitioned(a); +} diff --git a/tests/regression/60-array_annotations/04-structure_array_annotation.c b/tests/regression/60-array_annotations/04-structure_array_annotation.c new file mode 100644 index 0000000000..c57a12b0e6 --- /dev/null +++ b/tests/regression/60-array_annotations/04-structure_array_annotation.c @@ -0,0 +1,31 @@ +// PARAM: --set ana.base.arrays.unrolling-factor 4 --enable annotation.goblint_array_domain + +void w(int z[] ){ + if (z[2] == 4) { + z[2] = 3; + } else { + z[2] = 2; + } +} + +struct array { + int arr[5] __attribute__((goblint_array_domain("unroll"))); +}; + +int main(void) { + + struct array a = {{0,1,2,3}}; + + a.arr[2] = 4; + + w(a.arr); + + if (a.arr[2] == 3) + a.arr[2] = 5; + + w(a.arr); + + + __goblint_check(2 == a.arr[2]); + +} diff --git a/tests/regression/60-array_annotations/05-type_array_annotation.c b/tests/regression/60-array_annotations/05-type_array_annotation.c new file mode 100644 index 0000000000..c04b5a127c --- /dev/null +++ b/tests/regression/60-array_annotations/05-type_array_annotation.c @@ -0,0 +1,39 @@ +// PARAM: --set ana.base.arrays.unrolling-factor 4 --enable annotation.goblint_array_domain + +void t1(void) { + __attribute__((goblint_array_domain("unroll")))int x[4] ; + + x[0] = 0; + x[1] = 1; + x[2] = 2; + x[3] = 3; + + __goblint_check(x[0] == 0); + __goblint_check(x[1] == 1); + __goblint_check(x[2] == 2); + __goblint_check(x[3] == 3); + +} + +typedef int unrollInt __attribute__((goblint_array_domain("unroll"))); + +void t2(void) { + unrollInt x[4] ; + + x[0] = 0; + x[1] = 1; + x[2] = 2; + x[3] = 3; + + __goblint_check(x[0] == 0); + __goblint_check(x[1] == 1); + __goblint_check(x[2] == 2); + __goblint_check(x[3] == 3); + +} + +int main(void) +{ + t1(); + t2(); +} diff --git a/tests/regression/60-array_annotations/07-array_domain_project.c b/tests/regression/60-array_annotations/07-array_domain_project.c new file mode 100644 index 0000000000..fe3b76dc8e --- /dev/null +++ b/tests/regression/60-array_annotations/07-array_domain_project.c @@ -0,0 +1,40 @@ +// PARAM: --set ana.base.arrays.unrolling-factor 2 --enable annotation.goblint_array_domain +#include + +void main(void) { + unrollToTrivial(); +} + +int unrollToTrivial(void) +{ + int a[42] __attribute__((goblint_array_domain("unroll"))); + + a[0] = 0; + a[1] = 1; + a[2] = 2; + a[3] = 3; + + trivial(a); + + __goblint_check(a[0] == 7); //UNKNOWN + + //here unroll is used again + a[0] = 0; + a[1] = 1; + a[2] = 2; + a[3] = 3; + + __goblint_check(a[1] == 1); + __goblint_check(a[2] == 2); //UNKNOWN + +} + +void trivial(int* a __attribute__((goblint_array_domain("trivial")))){ + + __goblint_check(a[0] == 0); //UNKNOWN + __goblint_check(a[1] == 1); //UNKNOWN + __goblint_check(a[2] == 2); //UNKNOWN + __goblint_check(a[3] == 3); //UNKNOWN + + a[0] = 7; +}