Skip to content
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
22 commits
Select commit Hold shift + click to select a range
4b7df8b
Add option for restarting unknowns belonging to global variables sele…
jerhard Jan 27, 2022
b7d195e
Add test for manual restarting
jerhard Jan 27, 2022
37aefd6
Add test for manual restarting of globals when reads and writes occur…
jerhard Jan 27, 2022
1e20f20
Change global_from_name to globals_from_names working on a list, remo…
jerhard Jan 27, 2022
c501575
Issue warning if both automatic and manual restarting are active inst…
jerhard Jan 27, 2022
f9d0124
Remove unnecessary debug printout
jerhard Jan 27, 2022
253a44c
Add logic for destabilize_front, handling superstable to destabilize_…
jerhard Jan 27, 2022
7fcc4b2
Reformat code for user-triggered global restarting
jerhard Jan 27, 2022
83dab64
Collect varinfos instead of Cil.globals for manually restarted globals
jerhard Jan 27, 2022
2e6f194
Reuse Printable.String instead of creating a new module for it
jerhard Jan 27, 2022
dd8cf51
Annotate that earlyglobs is reason for imprecision
jerhard Jan 27, 2022
e7d591e
Comment that check is a hack to determine whether unknown relates to …
jerhard Jan 27, 2022
f5ee094
Allow manual restarting of functions
jerhard Jan 28, 2022
3589663
Add test case for manual restarting of function with partial contexts
jerhard Jan 28, 2022
2e688a2
Fix json in diff so to restart function foo
jerhard Jan 28, 2022
ebb9b60
Change call to destabilize to destabilize_normal.
jerhard Jan 28, 2022
2f98aa0
Manual restarting: check whether unkown is a leaf, and warn if it is …
jerhard Jan 31, 2022
293ba9e
Add pretty printing of unknown in printout.
jerhard Jan 31, 2022
6afc783
Manual global restarting: Warn about globals that should be restarted…
jerhard Jan 31, 2022
2a1665b
Move contents from cilUtil to varQuery
jerhard Jan 31, 2022
8268dc0
Move documentation comment to .mli file
jerhard Feb 1, 2022
ac4cb98
Rename option incremental.restart_globs.globs to incremental.restart.…
jerhard Feb 11, 2022
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
35 changes: 35 additions & 0 deletions src/framework/varQuery.ml
Original file line number Diff line number Diff line change
Expand Up @@ -4,3 +4,38 @@ type t =
[@@deriving ord]

type 'v f = 'v -> unit

let varinfo_from_global (g : Cil.global) : Cil.varinfo option = match g with
| GFun (f, _) -> Some f.svar
| GVar (v, _, _) -> Some v
| GVarDecl (v, _) -> Some v
| _ -> None

let varquery_from_global (g : Cil.global) : t option = match g with
| GFun (f, _) -> Some (Node {node = FunctionEntry f; fundec = Some f})
| GVar (v, _, _) -> Some (Global v)
| GVarDecl (v, _) -> Some (Global v)
| _ -> None

(** Takes a [Cil.file] and a list of names of globals.contents
Returns a list of [VarQuery.t]s of globals whose [vname] is contained in the argument list,
and the list of names for which no global with the name could be found. *)
let varqueries_from_names (file: Cil.file) (names: string list): t list * string list =
let module SM = Set.Make(Printable.Strings) in
let set = SM.of_list names in

(* Find list of [Cil.global]s that have one of the queried names, and a set of the found names *)
let globals, matched =
Cil.foldGlobals file (fun ((globs, matched) as acc) g ->
match varinfo_from_global g, varquery_from_global g with
| Some v, Some vq ->
begin match SM.mem v.vname set with
| true -> (vq::globs, SM.add v.vname matched)
| _ -> acc
end
| None, None -> acc
| _, _ -> assert false
) ([], SM.empty) in
(* List of queried but not found names *)
let unmatched = List.filter (fun s -> not @@ SM.mem s matched) names in
globals, unmatched
6 changes: 6 additions & 0 deletions src/framework/varQuery.mli
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
type t =
Global of Cil.varinfo
| Node of { node : Node.t; fundec : Cil.fundec option; }
val compare : t -> t -> int
type 'v f = 'v -> unit
val varqueries_from_names : Cil.file -> string list -> t list * string list
2 changes: 1 addition & 1 deletion src/maingoblint.ml
Original file line number Diff line number Diff line change
Expand Up @@ -455,7 +455,7 @@ let diff_and_rename current_file =
let max_ids = UpdateCil.update_ids old_file max_ids current_file version_map changes in
let restarting = GobConfig.get_string_list "incremental.restart_globs.globs" in

let restarting, not_found = CilUtil.varquery_from_names current_file restarting in
let restarting, not_found = VarQuery.varqueries_from_names current_file restarting in

if not (List.is_empty not_found) then begin
List.iter
Expand Down
47 changes: 0 additions & 47 deletions src/util/cilUtil.ml

This file was deleted.