Skip to content

Commit

Permalink
Remove phases (issue #460)
Browse files Browse the repository at this point in the history
  • Loading branch information
sim642 committed Aug 10, 2022
1 parent 5ad7631 commit e12db9e
Show file tree
Hide file tree
Showing 5 changed files with 26 additions and 78 deletions.
54 changes: 20 additions & 34 deletions src/maingoblint.ml
Original file line number Diff line number Diff line change
Expand Up @@ -405,42 +405,28 @@ let do_analyze change_info merged_AST =
L.pretty stf L.pretty exf L.pretty otf);
(* and here we run the analysis! *)

let do_all_phases ast funs =
let do_one_phase ast p =
phase := p;
if get_bool "dbg.verbose" then (
let aa = String.concat ", " @@ get_string_list "ana.activated" in
let at = String.concat ", " @@ get_string_list "trans.activated" in
print_endline @@ "Activated analyses for phase " ^ string_of_int p ^ ": " ^ aa;
print_endline @@ "Activated transformations for phase " ^ string_of_int p ^ ": " ^ at
);
try Control.analyze change_info ast funs
with e ->
let backtrace = Printexc.get_raw_backtrace () in (* capture backtrace immediately, otherwise the following loses it (internal exception usage without raise_notrace?) *)
let loc = !Tracing.current_loc in
Goblintutil.should_warn := true; (* such that the `about to crash` message gets printed *)
Messages.error ~category:Analyzer ~loc "About to crash!";
(* trigger Generic.SolverStats...print_stats *)
Goblintutil.(self_signal (signal_of_string (get_string "dbg.solver-signal")));
do_stats ();
print_newline ();
Printexc.raise_with_backtrace e backtrace (* re-raise with captured inner backtrace *)
(* Cilfacade.current_file := ast'; *)
in
(* new style is phases[i].ana.activated = [ana_1, ...]
phases[i].ana.x overwrites setting ana.x *)
let num_phases =
let np,na,nt = Tuple3.mapn (List.length % get_list) ("phases", "ana.activated", "trans.activated") in
(* TODO what about wrong usage like { phases = [...], ana.activated = [...] }? should child-lists add to parent-lists? *)
if get_bool "dbg.verbose" then print_endline @@ "Using new format for phases!";
if np = 0 && na = 0 && nt = 0 then failwith "No phases and no activated analyses or transformations!";
max np 1
in
ignore @@ Enum.iter (do_one_phase ast) (0 -- (num_phases - 1))
let control_analyze ast funs =
if get_bool "dbg.verbose" then (
let aa = String.concat ", " @@ get_string_list "ana.activated" in
let at = String.concat ", " @@ get_string_list "trans.activated" in
print_endline @@ "Activated analyses: " ^ aa;
print_endline @@ "Activated transformations: " ^ at
);
try Control.analyze change_info ast funs
with e ->
let backtrace = Printexc.get_raw_backtrace () in (* capture backtrace immediately, otherwise the following loses it (internal exception usage without raise_notrace?) *)
let loc = !Tracing.current_loc in
Goblintutil.should_warn := true; (* such that the `about to crash` message gets printed *)
Messages.error ~category:Analyzer ~loc "About to crash!";
(* trigger Generic.SolverStats...print_stats *)
Goblintutil.(self_signal (signal_of_string (get_string "dbg.solver-signal")));
do_stats ();
print_newline ();
Printexc.raise_with_backtrace e backtrace (* re-raise with captured inner backtrace *)
(* Cilfacade.current_file := ast'; *)
in

(* Analyze with the new experimental framework. *)
Stats.time "analysis" (do_all_phases merged_AST) funs
Stats.time "analysis" (control_analyze merged_AST) funs
)

let do_html_output () =
Expand Down
10 changes: 1 addition & 9 deletions src/util/gobConfig.ml
Original file line number Diff line number Diff line change
Expand Up @@ -24,10 +24,6 @@ open Printf

exception ConfigError of string


(* Phase of the analysis (moved from GoblintUtil b/c of circular build...) *)
let phase = ref 0

let building_spec = ref false


Expand Down Expand Up @@ -265,11 +261,7 @@ struct
let get_path_string f st =
try
let st = String.trim st in
let st, x =
let g st = st, get_value !json_conf (parse_path st) in
try g ("phases["^ string_of_int !phase ^"]."^st) (* try to find value in config for current phase first *)
with ConfTypeError -> g st (* do global lookup if undefined *)
in
let x = get_value !json_conf (parse_path st) in
if tracing then trace "conf-reads" "Reading '%s', it is %a.\n" st GobYojson.pretty x;
try f x
with Yojson.Safe.Util.Type_error (s, _) ->
Expand Down
2 changes: 1 addition & 1 deletion src/util/jsonSchema.ml
Original file line number Diff line number Diff line change
Expand Up @@ -112,7 +112,7 @@ let schema_defaults ?additional_field (schema: schema): Yojson.Safe.t =
element_defaults ?additional_field (root schema)

let create_schema element =
create @@ { element with id = Some "" } (* add id to make create defs check happy for phases Id_ref, doesn't get outputted apparently *)
create element

let rec element_require_all (element: element): element =
let kind' = match element.kind with
Expand Down
26 changes: 2 additions & 24 deletions src/util/options.ml
Original file line number Diff line number Diff line change
@@ -1,30 +1,8 @@
open Json_schema


let schema_of_yojson json =
(* workaround for json-data-encoding not handling recursive root reference correctly *)
(* remove the reference before parsing, hack it back afterwards *)
let json = JsonSchema.JQ.replace [`Field "properties"; `Field "phases"; `Field "items"] (`Assoc []) json in
let schema = JsonSchema.schema_of_yojson json in (* definitions_path doesn't work, "definitions" field still hardcoded *)
let element = Json_schema.root schema in
let element = match element with
| { kind = Object ({properties; _} as object_specs); _} ->
let rec modify = function
| [] -> assert false
| ("phases", ({ Json_schema.kind = Monomorphic_array (_, array_specs); _} as field_element), required, unknown) :: props ->
("phases", {field_element with Json_schema.kind = Monomorphic_array (Json_schema.element (Id_ref ""), array_specs)}, required, unknown) :: props
| prop :: props ->
prop :: modify props
in
{element with kind = Object {object_specs with properties = modify properties}}
| _ ->
assert false
in
JsonSchema.create_schema element

let schema =
(* schema_of_yojson (Yojson.Safe.from_file "options.schema.json") *)
schema_of_yojson (Yojson.Safe.from_string [%blob "options.schema.json"])
(* JsonSchema.schema_of_yojson (Yojson.Safe.from_file "options.schema.json") *)
JsonSchema.schema_of_yojson (Yojson.Safe.from_string [%blob "options.schema.json"])

let require_all = JsonSchema.schema_require_all schema

Expand Down
12 changes: 2 additions & 10 deletions src/util/options.schema.json
Original file line number Diff line number Diff line change
Expand Up @@ -129,14 +129,6 @@
"type": "boolean",
"default": false
},
"phases": {
"title": "phases",
"description":
"List of phases. Per-phase settings overwrite global ones.",
"type": "array",
"items": { "$ref": "#" },
"default": []
},
"save_run": {
"title": "save_run",
"description":
Expand Down Expand Up @@ -321,7 +313,7 @@
"properties": {
"activated": {
"title": "ana.activated",
"description": "Lists of activated analyses in this phase.",
"description": "Lists of activated analyses.",
"type": "array",
"items": { "type": "string" },
"default": [
Expand Down Expand Up @@ -1115,7 +1107,7 @@
"activated": {
"title": "trans.activated",
"description":
"Lists of activated transformations in this phase. Transformations happen after analyses.",
"Lists of activated transformations. Transformations happen after analyses.",
"type": "array",
"items": { "type": "string" },
"default": []
Expand Down

0 comments on commit e12db9e

Please sign in to comment.