Skip to content

Commit

Permalink
Merge branch 'goblint:master' into master
Browse files Browse the repository at this point in the history
  • Loading branch information
ManuelLerchner authored Nov 19, 2024
2 parents 47b7a56 + 065f990 commit 4a542be
Show file tree
Hide file tree
Showing 29 changed files with 406 additions and 122 deletions.
26 changes: 26 additions & 0 deletions .semgrep/fold.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
rules:
- id: fold-exists
patterns:
- pattern-either:
- pattern: $D.fold ... false
- pattern: $D.fold_left ... false
- pattern: $D.fold_right ... false
- pattern: fold ... false
- pattern: fold_left ... false
- pattern: fold_right ... false
message: consider replacing fold with exists
languages: [ocaml]
severity: WARNING

- id: fold-for_all
patterns:
- pattern-either:
- pattern: $D.fold ... true
- pattern: $D.fold_left ... true
- pattern: $D.fold_right ... true
- pattern: fold ... true
- pattern: fold_left ... true
- pattern: fold_right ... true
message: consider replacing fold with for_all
languages: [ocaml]
severity: WARNING
8 changes: 8 additions & 0 deletions .semgrep/tracing.yml
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,16 @@ rules:
- pattern: Messages.tracec
- pattern: Messages.traceu
- pattern: Messages.traceli
- pattern: M.trace
- pattern: M.tracel
- pattern: M.tracei
- pattern: M.tracec
- pattern: M.traceu
- pattern: M.traceli
- pattern-not-inside: if Messages.tracing then ...
- pattern-not-inside: if Messages.tracing && ... then ...
- pattern-not-inside: if M.tracing then ...
- pattern-not-inside: if M.tracing && ... then ...
message: trace functions should only be called if tracing is enabled at compile time
languages: [ocaml]
severity: WARNING
1 change: 1 addition & 0 deletions conf/svcomp-validate.json
Original file line number Diff line number Diff line change
Expand Up @@ -67,6 +67,7 @@
"wideningThresholds",
"loopUnrollHeuristic",
"memsafetySpecification",
"noOverflows",
"termination",
"tmpSpecialAnalysis"
]
Expand Down
13 changes: 2 additions & 11 deletions conf/svcomp.json
Original file line number Diff line number Diff line change
Expand Up @@ -66,6 +66,7 @@
"wideningThresholds",
"loopUnrollHeuristic",
"memsafetySpecification",
"noOverflows",
"termination",
"tmpSpecialAnalysis"
]
Expand Down Expand Up @@ -107,17 +108,7 @@
"after-lock": false,
"other": false,
"accessed": false,
"exact": true,
"exclude-vars": [
"tmp\\(___[0-9]+\\)?",
"cond",
"RETURN",
"__\\(cil_\\)?tmp_?[0-9]*\\(_[0-9]+\\)?",
".*____CPAchecker_TMP_[0-9]+",
"__VERIFIER_assert__cond",
"__ksymtab_.*",
"\\(ldv_state_variable\\|ldv_timer_state\\|ldv_timer_list\\|ldv_irq_\\(line_\\|data_\\)?[0-9]+\\|ldv_retval\\)_[0-9]+"
]
"exact": true
}
},
"pre": {
Expand Down
16 changes: 10 additions & 6 deletions src/analyses/base.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2172,11 +2172,7 @@ struct
in
List.filter_map (create_thread ~multiple (Some (Mem id, NoOffset)) (Some ptc_arg)) start_funvars_with_unknown
end
| _, _ when get_bool "sem.unknown_function.spawn" ->
(* TODO: Remove sem.unknown_function.spawn check because it is (and should be) really done in LibraryFunctions.
But here we consider all non-ThreadCreate functions also unknown, so old-style LibraryFunctions access
definitions using `Write would still spawn because they are not truly unknown functions (missing from LibraryFunctions).
Need this to not have memmove spawn in SV-COMP. *)
| _, _ ->
let shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Spawn; deep = false } args in
let deep_args = LibraryDesc.Accesses.find desc.accs { kind = Spawn; deep = true } args in
let shallow_flist = collect_invalidate ~deep:false ~ctx ctx.local shallow_args in
Expand All @@ -2185,7 +2181,6 @@ struct
let addrs = List.concat_map AD.to_var_may flist in
if addrs <> [] then M.debug ~category:Analyzer "Spawning non-unique functions from unknown function: %a" (d_list ", " CilType.Varinfo.pretty) addrs;
List.filter_map (create_thread ~multiple:true None None) addrs
| _, _ -> []

let assert_fn ctx e refine =
(* make the state meet the assertion in the rest of the code *)
Expand Down Expand Up @@ -2656,6 +2651,15 @@ struct
| Unknown, "__goblint_assume_join" ->
let id = List.hd args in
Priv.thread_join ~force:true (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) id st
| ThreadSelf, _ ->
begin match lv, ThreadId.get_current (Analyses.ask_of_ctx ctx) with
| Some lv, `Lifted tid ->
set ~ctx st (eval_lv ~ctx st lv) (Cilfacade.typeOfLval lv) (Thread (ValueDomain.Threads.singleton tid))
| Some lv, _ ->
invalidate_ret_lv st
| None, _ ->
st
end
| Alloca size, _ -> begin
match lv with
| Some lv ->
Expand Down
12 changes: 6 additions & 6 deletions src/analyses/basePriv.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1040,11 +1040,11 @@ struct
let s = MustLockset.remove m (current_lockset ask) in
let t = current_thread ask in
let side_cpa = CPA.filter (fun x _ ->
GWeak.fold (fun s' tm acc ->
GWeak.exists (fun s' tm ->
(* TODO: swap 2^M and T partitioning for lookup by t here first? *)
let v = ThreadMap.find t tm in
(MustLockset.mem m s' && not (VD.is_bot v)) || acc
) (G.weak (getg (V.global x))) false
(MustLockset.mem m s' && not (VD.is_bot v))
) (G.weak (getg (V.global x)))
) st.cpa
in
sideg (V.mutex m) (G.create_sync (GSync.singleton s side_cpa));
Expand Down Expand Up @@ -1098,9 +1098,9 @@ struct
let unlock ask getg sideg (st: BaseComponents (D).t) m =
let s = MustLockset.remove m (current_lockset ask) in
let side_cpa = CPA.filter (fun x _ ->
GWeak.fold (fun s' v acc ->
(MustLockset.mem m s' && not (VD.is_bot v)) || acc
) (G.weak (getg (V.global x))) false
GWeak.exists (fun s' v ->
(MustLockset.mem m s' && not (VD.is_bot v))
) (G.weak (getg (V.global x)))
) st.cpa
in
sideg (V.mutex m) (G.create_sync (GSync.singleton s side_cpa));
Expand Down
10 changes: 4 additions & 6 deletions src/analyses/threadAnalysis.ml
Original file line number Diff line number Diff line change
Expand Up @@ -95,9 +95,7 @@ struct
let startstate v = D.bot ()

let threadenter ctx ~multiple lval f args =
if multiple then
(let tid = ThreadId.get_current_unlift (Analyses.ask_of_ctx ctx) in
ctx.sideg tid (true, TS.bot (), false));
(* ctx is of creator, side-effects to denote non-uniqueness are performed in threadspawn *)
[D.bot ()]

let threadspawn ctx ~multiple lval f args fctx =
Expand All @@ -106,9 +104,9 @@ struct
let repeated = D.mem tid ctx.local in
let eff =
match creator with
| `Lifted ctid -> (repeated, TS.singleton ctid, false)
| `Top -> (true, TS.bot (), false)
| `Bot -> (false, TS.bot (), false)
| `Lifted ctid -> (repeated || multiple, TS.singleton ctid, false)
| `Top -> (true, TS.bot (), false)
| `Bot -> (multiple, TS.bot (), false)
in
ctx.sideg tid eff;
D.join ctx.local (D.singleton tid)
Expand Down
76 changes: 54 additions & 22 deletions src/autoTune.ml
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,34 @@ class functionVisitor(calling, calledBy, argLists, dynamicallyCalled) = object
DoChildren
end

exception Found
class findAllocsInLoops = object
inherit nopCilVisitor

val mutable inloop = false

method! vstmt stmt =
let outOfLoop stmt =
match stmt.skind with
| Loop _ -> inloop <- false; stmt
| _ -> stmt
in
match stmt.skind with
| Loop _ -> inloop <- true; ChangeDoChildrenPost(stmt, outOfLoop)
| _ -> DoChildren

method! vinst = function
| Call (_, Lval (Var f, NoOffset), args,_,_) when LibraryFunctions.is_special f ->
Goblint_backtrace.protect ~mark:(fun () -> Cilfacade.FunVarinfo f) ~finally:Fun.id @@ fun () ->
let desc = LibraryFunctions.find f in
begin match desc.special args with
| Malloc _
| Alloca _ when inloop -> raise Found
| _ -> DoChildren
end
| _ -> DoChildren
end

type functionCallMaps = {
calling: FunctionSet.t FunctionCallMap.t;
calledBy: (FunctionSet.t * int) FunctionCallMap.t;
Expand Down Expand Up @@ -157,7 +185,7 @@ let hasFunction pred =
Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo var) @@ fun () ->
if LibraryFunctions.is_special var then
let desc = LibraryFunctions.find var in
GobOption.exists (fun args -> pred (desc.special args)) (functionArgs var)
GobOption.exists (fun args -> pred desc args) (functionArgs var)
else
false
in
Expand All @@ -169,7 +197,7 @@ let hasFunction pred =
match unrollType var.vtype with
| TFun (_, args, _, _) ->
let args = BatOption.map_default (List.map (fun (x,_,_) -> MyCFG.unknown_exp)) [] args in
pred (desc.special args)
pred desc args
| _ -> false
else
false
Expand All @@ -191,9 +219,10 @@ let enableAnalyses anas =

let notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadid"; "threadJoins"; "threadreturn"; "mhp"; "region"; "pthreadMutexType"]
let reduceThreadAnalyses () =
let isThreadCreate = function
let isThreadCreate (desc: LibraryDesc.t) args =
match desc.special args with
| LibraryDesc.ThreadCreate _ -> true
| _ -> false
| _ -> LibraryDesc.Accesses.find_kind desc.accs Spawn args <> []
in
let hasThreadCreate = hasFunction isThreadCreate in
if not @@ hasThreadCreate then (
Expand Down Expand Up @@ -229,18 +258,28 @@ let focusOnTermination (spec: Svcomp.Specification.t) =
let focusOnTermination () =
List.iter focusOnTermination (Svcomp.Specification.of_option ())

let focusOnSpecification (spec: Svcomp.Specification.t) =
let concurrencySafety (spec: Svcomp.Specification.t) =
match spec with
| UnreachCall s -> ()
| NoDataRace -> (*enable all thread analyses*)
Logs.info "Specification: NoDataRace -> enabling thread analyses \"%s\"" (String.concat ", " notNeccessaryThreadAnalyses);
enableAnalyses notNeccessaryThreadAnalyses;
| NoOverflow -> (*We focus on integer analysis*)
set_bool "ana.int.def_exc" true
| _ -> ()

let focusOnSpecification () =
List.iter focusOnSpecification (Svcomp.Specification.of_option ())
let noOverflows (spec: Svcomp.Specification.t) =
match spec with
| NoOverflow ->
(*We focus on integer analysis*)
set_bool "ana.int.def_exc" true;
begin
try
ignore @@ visitCilFileSameGlobals (new findAllocsInLoops) (!Cilfacade.current_file);
set_int "ana.malloc.unique_address_count" 1
with Found -> set_int "ana.malloc.unique_address_count" 0;
end
| _ -> ()

let focusOn (f : SvcompSpec.t -> unit) =
List.iter f (Svcomp.Specification.of_option ())

(*Detect enumerations and enable the "ana.int.enums" option*)
exception EnumFound
Expand Down Expand Up @@ -446,7 +485,8 @@ let wideningOption factors file =
}

let activateTmpSpecialAnalysis () =
let isMathFun = function
let isMathFun (desc: LibraryDesc.t) args =
match desc.special args with
| LibraryDesc.Math _ -> true
| _ -> false
in
Expand Down Expand Up @@ -487,15 +527,6 @@ let isActivated a = get_bool "ana.autotune.enabled" && List.mem a @@ get_string_

let isTerminationTask () = List.mem Svcomp.Specification.Termination (Svcomp.Specification.of_option ())

let specificationIsActivated () =
isActivated "specification" && get_string "ana.specification" <> ""

let specificationTerminationIsActivated () =
isActivated "termination"

let specificationMemSafetyIsActivated () =
isActivated "memsafetySpecification"

let chooseConfig file =
let factors = collectFactors visitCilFileSameGlobals file in
let fileCompplexity = estimateComplexity factors file in
Expand All @@ -515,8 +546,9 @@ let chooseConfig file =
if isActivated "mallocWrappers" then
findMallocWrappers ();

if specificationIsActivated () then
focusOnSpecification ();
if isActivated "concurrencySafetySpecification" then focusOn concurrencySafety;

if isActivated "noOverflows" then focusOn noOverflows;

if isActivated "enums" && hasEnums file then
set_bool "ana.int.enums" true;
Expand Down
36 changes: 18 additions & 18 deletions src/cdomain/value/cdomains/stringDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -20,12 +20,12 @@ let reset_lazy () =


type t = string option [@@deriving eq, ord, hash]
(** [None] means top. *)

let hash x =
if get_string_domain () = Disjoint then
hash x
else
13859
match get_string_domain () with
| Disjoint | Flat -> hash x
| Unit -> 13859

let show = function
| Some x -> "\"" ^ x ^ "\""
Expand All @@ -39,10 +39,9 @@ include Printable.SimpleShow (
)

let of_string x =
if get_string_domain () = Unit then
None
else
Some x
match get_string_domain () with
| Unit -> None
| Disjoint | Flat -> Some x
let to_string x = x

(* only keep part before first null byte *)
Expand Down Expand Up @@ -91,24 +90,25 @@ let join x y =
| _, None -> None
| Some a, Some b when a = b -> Some a
| Some a, Some b (* when a <> b *) ->
if get_string_domain () = Disjoint then
raise Lattice.Uncomparable
else
None
match get_string_domain () with
| Disjoint -> raise Lattice.Uncomparable
| Flat -> None
| Unit -> assert false

let meet x y =
match x, y with
| None, a
| a, None -> a
| Some a, Some b when a = b -> Some a
| Some a, Some b (* when a <> b *) ->
if get_string_domain () = Disjoint then
raise Lattice.Uncomparable
else
raise Lattice.BotValue
match get_string_domain () with
| Disjoint -> raise Lattice.Uncomparable
| Flat -> raise Lattice.BotValue
| Unit -> assert false

let repr x =
if get_string_domain () = Disjoint then
match get_string_domain () with
| Disjoint ->
x (* everything else is kept separate, including strings if not limited *)
else
| Flat | Unit ->
None (* all strings together if limited *)
4 changes: 2 additions & 2 deletions src/cdomain/value/cdomains/threadIdDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -83,10 +83,10 @@ struct
(v, None)

let is_main = function
| ({vname; _}, None) -> List.mem vname @@ GobConfig.get_string_list "mainfun"
| ({vname; _}, None) -> GobConfig.get_bool "ana.thread.include-node" && List.mem vname @@ GobConfig.get_string_list "mainfun"
| _ -> false

let is_unique _ = false (* TODO: should this consider main unique? *)
let is_unique = is_main
let may_create _ _ = true
let is_must_parent _ _ = false
end
Expand Down
Loading

0 comments on commit 4a542be

Please sign in to comment.