Skip to content

Commit

Permalink
Merge pull request #517 from goblint/rm_SolverInteractiveWGlob
Browse files Browse the repository at this point in the history 
Remove SolverInteractiveWGlob
  • Loading branch information
@michael-schwarz
michael-schwarz authored Jan 6, 2022
2 parents c6f3943 + 380df84 commit d563ea5
Show file tree
Hide file tree
Showing 4 changed files with 2 additions and 192 deletions.
2 changes: 1 addition & 1 deletion g2html
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
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
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
25 changes: 0 additions & 25 deletions src/util/options.schema.json
View file
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

0 comments on commit d563ea5

Please sign in to comment.