1+ open Goblint_lib ;
2+ open Batteries ;
3+ open Js_of_ocaml ;
4+ open Lwt . Infix ;
5+ module Cabs2cil = GoblintCil . Cabs2cil ;
6+
7+ exception InitFailed ( string) ;
8+
9+ let init_cil = environment => {
10+ // Restore the environment hash table, which
11+ // syntacticsearch uses to map temporary variables created
12+ // by CIL to their original counterparts.
13+ Hashtbl . clear(Cabs2cil . environment);
14+ environment
15+ |> Hashtbl . enum
16+ |> Enum . iter(((k, v)) => Hashtbl . add(Cabs2cil . environment, k, v));
17+ };
18+
19+ // Each Goblint analysis module is assigned an ID, and this
20+ // ID depends on the module registration order, which might
21+ // differ from build to build. This function reorders the
22+ // analysis list to match the native version of Goblint.
23+ let renumber_goblint_analyses = registered_name => {
24+ let old_registered = Hashtbl . copy(MCP . registered);
25+ let old_registered_name = Hashtbl . copy(MCP . registered_name);
26+ Hashtbl . clear(MCP . registered);
27+ Hashtbl . clear(MCP . registered_name);
28+ Hashtbl . iter((name, id) => {
29+ let old_id = Hashtbl . find(old_registered_name, name);
30+ let spec = Hashtbl . find(old_registered, old_id);
31+ Hashtbl . replace(MCP . registered, id, spec);
32+ Hashtbl . replace(MCP . registered_name, name, id);
33+ }, registered_name);
34+ };
35+
36+ let init_goblint = (solver, spec, registered_name, config, cil) => {
37+ AfterConfig . run() ; // This registers the "base" analysis
38+
39+ try (renumber_goblint_analyses(registered_name)) {
40+ | Not_found =>
41+ raise (InitFailed ("Failed to renumber Goblint analyses" ))
42+ };
43+
44+ Sys . chdir("/" ); // Don't remove this
45+
46+ Sys_js . create_file(~name= "/goblint/solver.marshalled" , ~content= solver);
47+ Sys_js . create_file(~name= "/goblint/config.json" , ~content= config);
48+ Sys_js . create_file(~name= "/goblint/spec_marshal" , ~content= spec);
49+
50+ GobConfig . merge_file(Fpath . v("/goblint/config.json" ));
51+
52+ GobConfig . set_bool("dbg.verbose" , true );
53+ // TODO: Uncomment this to improve performance in future
54+ // GobConfig.set_bool("verify", false);
55+
56+ // For some reason, the standard Batteries output channels
57+ // appear to be closed by default and writing to them
58+ // raises [BatInnerIO.Output_closed]. This fixes it.
59+ let out = IO . output_channel(Stdlib . stdout);
60+ Messages . formatter := Format . formatter_of_output(out);
61+
62+ GobConfig . set_string("load_run" , "goblint" );
63+
64+ // These two will be set by config.json. Reset them.
65+ GobConfig . set_string("save_run" , "" );
66+ GobConfig . set_bool("gobview" , false );
67+
68+ GobConfig . set_auto("trans.activated[+]" , "'expeval'" );
69+
70+ Cilfacade . init() ;
71+ Maingoblint . handle_extraspecials() ;
72+ Maingoblint . handle_flags() ;
73+
74+ // NOTE: Commenting this out since it breaks the node view. Semantic search
75+ // may depend on this code but it is currently broken because of unrelated
76+ // (and uknown) reasons anyway.
77+ // Cil.iterGlobals(cil, glob =>
78+ // switch (glob) {
79+ // | GFun(fd, _) =>
80+ // Cil.prepareCFG(fd);
81+ // Cil.computeCFGInfo(fd, true);
82+ // | _ => ()
83+ // }
84+ // );
85+ Cilfacade . current_file := cil;
86+
87+ let goblint = GvGoblint . unmarshal(spec, cil);
88+
89+ (goblint, cil);
90+ };
91+
92+ // function for reloading specific files when rerunning analysis
93+ let reload = (cil) => {
94+ [
95+ // files to be reloaded
96+ "./solver.marshalled" ,
97+ "./warnings.marshalled" ,
98+ "./stats.marshalled" ,
99+
100+ // required for solver, solver alone cannot update
101+ "./spec_marshal" ,
102+ "./analyses.marshalled" ,
103+ "./config.json" ,
104+ ]
105+ |> List . map(HttpClient . get)
106+ |> Lwt . all
107+ >>= (l) => {
108+ Lwt . return(switch (l) {
109+ | [ solver , warnings , stats , spec , analyses , config ] => {
110+
111+ let goblintAndCil =
112+ switch (solver, spec, analyses, config) {
113+ | (Ok (s ), Ok (spec ), Ok (t ), Ok (c )) => {
114+ let t = Marshal . from_string(t, 0 );
115+ Some (init_goblint(s, spec, t, c, cil))
116+ }
117+ | _ => {
118+ Util . error_without_fail("Failed to load Goblint state" );
119+ None
120+ }
121+ };
122+ print_endline("Initialized Goblint" );
123+
124+ let warnings =
125+ switch (warnings) {
126+ | Ok (s ) => Some (Marshal . from_string(s, 0 ))
127+ | _ => Util . error_without_fail("Failed to load the warning table" ); None
128+ };
129+ print_endline("Restored the warning table" );
130+
131+ let stats =
132+ switch (stats) {
133+ | Ok (s ) => Some (Marshal . from_string(s, 0 ))
134+ | _ => Util . error_without_fail("Failed to load runtime stats" ); None
135+ };
136+
137+ Some ((goblintAndCil, warnings, stats))
138+ }
139+ | _ => None
140+ })
141+ }
142+ };
0 commit comments