Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove SolverInteractiveWGlob #517

Merged
merged 4 commits into from
Jan 6, 2022
Merged

Remove SolverInteractiveWGlob #517

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
9de69f8
Remove SolverInteractiveWGlob
michael-schwarz Jan 4, 2022
cebc5f2
Update g2html
michael-schwarz Jan 4, 2022
081af21
Bump g2html
michael-schwarz Jan 5, 2022
380df84
Bump g2html
michael-schwarz Jan 6, 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
2 changes: 1 addition & 1 deletion g2html
Open in desktop
Submodule g2html updated 5 files
+0 −1,433 src/fi/iki/elonen/NanoHTTPD.java
+0 −2 src/g2html/Config.java
+0 −81 src/g2html/GoblintInstance.java
+0 −186 src/g2html/GoblintServer.java
+1 −18 src/g2html/Main.java
2 changes: 1 addition & 1 deletion src/framework/cfgTools.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -636,7 +636,7 @@ let dead_code_cfg (file:file) (module Cfg : CfgBidir) live =
match glob with
| GFun (fd,loc) ->
(* ignore (Printf.printf "fun: %s\n" fd.svar.vname); *)
let base_dir = Goblintutil.create_dir ((if get_bool "interact.enabled" then get_string "interact.out"^"/" else "")^"cfgs") in
let base_dir = Goblintutil.create_dir "cfgs" in
let c_file_name = Str.global_substitute (Str.regexp Filename.dir_sep) (fun _ -> "%2F") fd.svar.vdecl.file in
let dot_file_name = fd.svar.vname^".dot" in
let file_dir = Goblintutil.create_dir (Filename.concat base_dir c_file_name) in
Expand Down
165 changes: 0 additions & 165 deletions src/solvers/generic.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,171 +32,6 @@ module LoadRunSolver: GenericEqBoxSolver =
module LoadRunIncrSolver: GenericEqBoxIncrSolver =
Constraints.EqIncrSolverFromEqSolver (LoadRunSolver)


module SolverInteractiveWGlob
(S:Analyses.GlobConstrSys)
(LH:Hashtbl.S with type key=S.LVar.t)
(GH:Hashtbl.S with type key=S.GVar.t) =
struct
open S
open Printf
open Cil

let enabled = ref false
let step = ref 1
let stopped = ref false

let interact_init () =
enabled := get_bool "interact.enabled";
stopped := get_bool "interact.paused"

let _ =
let open Sys in
set_signal sigtstp (Signal_handle (fun i -> stopped := true));
set_signal sigusr1 (Signal_handle (fun i -> stopped := false));
set_signal sigusr2 (Signal_handle (fun i -> step := 1))

let loc_start f =
fprintf f "<?xml version=\"1.0\" ?>\n<?xml-stylesheet type=\"text/xsl\" href=\"../node.xsl\"?>\n<loc>"

let glob_start f =
fprintf f "<?xml version=\"1.0\" ?>\n<?xml-stylesheet type=\"text/xsl\" href=\"../globals.xsl\"?>\n<globs>"

let loc_end f =
fprintf f "</loc>\n"

let glob_end f =
fprintf f "</globs>\n"

let write_one_call v d f =
fprintf f "%a%a</call>\n" LVar.printXml v D.printXml d

let write_one_glob v d f =
fprintf f "<glob><key>%a</key>\n%a</glob>\n" GVar.printXml v G.printXml d

let mkdirs =
List.fold_left (fun p d -> Goblintutil.create_dir (p^"/"^d)) "."

let warning_id = ref 1
let writeXmlWarnings () =
let one_text f Messages.Piece.{loc; text = m; _} =
match loc with
| Some l ->
BatPrintf.fprintf f "\n<text file=\"%s\" line=\"%d\" column=\"%d\">%s</text>" l.file l.line l.column (GU.escape m)
| None ->
() (* TODO: not outputting warning without location *)
in
let one_w f (m: Messages.Message.t) = match m.multipiece with
| Single piece -> one_text f piece
| Group {group_text = n; pieces = e} ->
fprintf f "<group name=\"%s\">%a</group>\n" n (List.print ~first:"" ~last:"" ~sep:"" one_text) e
in
let one_w x f = fprintf f "\n<warning>%a</warning>" one_w x in
let res_dir = mkdirs [get_string "interact.out" ^ "/warn"] in
let write_warning x =
let full_name = res_dir ^ "/warn" ^ string_of_int !warning_id ^ ".xml" in
incr warning_id;
File.with_file_out ~mode:[`create;`excl;`text] full_name (one_w x)
in
List.iter write_warning !Messages.Table.messages_list

module SSH = Hashtbl.Make (struct include String let hash (x:string) = Hashtbl.hash x end)
let funs = SSH.create 100
module NH = Hashtbl.Make (Node)
let liveness = NH.create 100
let updated_l = NH.create 100
let updated_g = GH.create 100

let write_files lh gh =
let res_dir = mkdirs [get_string "interact.out"; "nodes"] in
let created_files = Hashtbl.create 100 in
let one_var v d =
let fname = LVar.var_id v in
let full_name = res_dir ^ "/" ^ fname ^ ".xml" in
if not (Sys.file_exists full_name) then begin
File.with_file_out ~mode:[`excl;`create;`text] full_name loc_start;
Hashtbl.add created_files full_name ()
end;
File.with_file_out ~mode:[`append;`excl;`text] full_name (write_one_call v d)
in
LH.iter one_var lh;
let full_gname = res_dir ^ "/globals.xml" in
File.with_file_out ~mode:[`excl;`create;`text] full_gname glob_start;
let one_glob v d =
File.with_file_out ~mode:[`append;`excl;`text] full_gname (write_one_glob v d)
in
GH.iter one_glob gh;
File.with_file_out ~mode:[`append;`excl;`text] full_gname glob_end;
let close_vars f _ =
File.with_file_out ~mode:[`append;`excl;`text] f loc_end
in
Hashtbl.iter close_vars created_files

let write_updates () =
let dir = get_string "interact.out" in
let full_name = dir ^ "/updates.xml" in
let write_updates f =
fprintf f "<?xml version=\"1.0\" ?>\n<?xml-stylesheet type=\"text/xsl\" href=\"updates.xsl\"?>\n<updates>\n";
NH.iter (fun v () -> fprintf f "%a</call>\n" Var.printXml v) updated_l;
GH.iter (fun v () -> fprintf f "<global>\n%a</global>\n" GVar.printXml v) updated_g;
let g n _ = fprintf f "<warning warn=\"warn%d\" />\n" (n + !warning_id) in
List.iteri g !Messages.Table.messages_list;
(* List.iter write_warning !Messages.messages_list *)
fprintf f "</updates>\n";
in
File.with_file_out ~mode:[`excl;`create;`text] full_name write_updates

let write_index () =
let dir = get_string "interact.out" in
let full_name = dir ^ "/index.xml" in
let write_index f =
let print_funs f fs =
Set.iter (fun n -> fprintf f "<function name=\"%s\"></function>\n" n) fs
in
fprintf f "<?xml version=\"1.0\" ?>\n<?xml-stylesheet type=\"text/xsl\" href=\"report.xsl\"?>\n<report>\n";
SSH.iter (fun file funs -> fprintf f "<file name=\"%s\">%a</file>" file print_funs funs) funs;
fprintf f "</report>\n";
in
File.with_file_out ~mode:[`excl;`create;`text] full_name write_index

let delete_old_results () =
let dir = get_string "interact.out" in
if Sys.file_exists dir && Sys.is_directory dir then
try Goblintutil.rm_rf dir with _ -> ()

let write_all hl hg =
delete_old_results ();
write_files hl hg;
write_index ();
if !stopped then
write_updates ();
writeXmlWarnings (); (* must be after write_update! *)
!write_cfgs (NH.mem liveness);
NH.clear updated_l;
GH.clear updated_g

let update_var_event_local hl hg x o n =
if !enabled && not (D.is_bot n) then begin
let node = LVar.node x in
let file = (Node.find_fundec node).svar in
NH.replace updated_l node ();
NH.replace liveness node ();
SSH.replace funs file.vdecl.file (Set.add file.vname (SSH.find_default funs file.vdecl.file Set.empty));
if !stopped then begin
write_all hl hg;
decr step;
while !stopped && !step <=0 do Unix.sleep 1 done
end
end

let update_var_event_global hl hg x o n =
GH.replace updated_g x ()

let done_event hl hg =
if !enabled then
write_all hl hg
end

module SolverStats (S:EqConstrSys) (HM:Hashtbl.S with type key = S.v) =
struct
open S
Expand Down
27 changes: 1 addition & 26 deletions src/util/options.schema.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -173,31 +173,6 @@
"type": "boolean",
"default": false
},
"interact": {
"title": "interact",
"type": "object",
"properties": {
"out": {
"title": "interact.out",
"description": "The result directory in interactive mode.",
"type": "string",
"default": "result"
},
"enabled": {
"title": "interact.enabled",
"description": "Is interactive mode enabled.",
"type": "boolean",
"default": false
},
"paused": {
"title": "interact.paused",
"description": "Start interactive in pause mode.",
"type": "boolean",
"default": false
}
},
"additionalProperties": false
},
"phases": {
"title": "phases",
"description":
Expand Down Expand Up @@ -1809,4 +1784,4 @@
}
},
"additionalProperties": false
}
}