Skip to content

Commit dcc2b4d

Browse files
stilscherstilscher
authored
Merge pull request #19 from goblint/fix-c-file-loading
Fix loading of C source files
2 parents 72dadf7 + b14df8b commit dcc2b4d

File tree

8 files changed

+89
-30
lines changed

8 files changed

+89
-30
lines changed

‎public/index.html‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,7 @@
77

88
<title>Gobview</title>
99

10-
<link rel="icon"
11-
href="https://emojipedia-us.s3.dualstack.us-west-1.amazonaws.com/thumbs/240/emojione/211/bactrian-camel_1f42b.png" />
10+
<link rel="icon" href="https://avatars.githubusercontent.com/u/917621?s=96&v=4"/>
1211
</head>
1312

1413
<body>

‎runtime/stubs.js‎

Lines changed: 39 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -11,12 +11,38 @@ function unix_setitimer(which, newval) {
1111
return newval;
1212
}
1313

14-
//Provides: ml_z_mul_overflows
15-
function ml_z_mul_overflows(x) {
16-
// This is necessary until https://github.com/janestreet/zarith_stubs_js/pull/8 is fixed.
17-
return true;
14+
//Provides: unix_times
15+
//only used for timing statistics in Goblint
16+
function unix_times(x) {
17+
return 0;
1818
}
1919

20+
//Provides: max_float
21+
//from Goblint specific stubs for C float operations
22+
function max_float(x) {
23+
return Number.MAX_VALUE;
24+
}
25+
26+
//Provides: smallest_float
27+
//from Goblint specific stubs for C float operations
28+
//returns the smallest positive and normalized float
29+
function smallest_float(x) {
30+
return 2.2250738585072014e-308;
31+
}
32+
33+
//external of_int: int -> t
34+
//Provides: ml_z_of_int const
35+
//Requires: bigInt
36+
function ml_z_of_int(i) {
37+
return i | 0;
38+
}
39+
40+
//Provides: caml_thread_initialize const
41+
function caml_thread_initialize() {}
42+
43+
//Provides: caml_mutex_new const
44+
function caml_mutex_new() {}
45+
2046
//Provides: camlidl_apron_init
2147
function camlidl_apron_init() { return 0; }
2248

@@ -29,6 +55,9 @@ function camlidl_oct_oct_manager_alloc() { return 0; }
2955
//Provides: camlidl_polka_pk_manager_alloc_loose
3056
function camlidl_polka_pk_manager_alloc_loose() { return 0; }
3157

58+
//Provides: camlidl_polka_pk_manager_alloc_equalities
59+
function camlidl_polka_pk_manager_alloc_equalities() { return 0; }
60+
3261
//Provides: camlidl_box_box_manager_alloc
3362
function camlidl_box_box_manager_alloc() { return 0; }
3463

@@ -43,3 +72,9 @@ function camlidl_abstract1_ap_abstract1_top() { return 0; }
4372

4473
//Provides: camlidl_var_ap_var_hash
4574
function camlidl_var_ap_var_hash() { return 0; }
75+
76+
//Provides: camlidl_mpq_mpq_init
77+
function camlidl_mpq_mpq_init() { return 0; }
78+
79+
//Provides: camlidl_mpq_mpq_set_si
80+
function camlidl_mpq_mpq_set_si() { return 0; }

‎src/App.re‎

Lines changed: 11 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -89,7 +89,7 @@ let init_goblint = (solver, spec, registered_name, config, cil) => {
8989
(goblint, cil);
9090
};
9191

92-
let init = (solver, spec, config, meta, cil, analyses, warnings, stats) => {
92+
let init = (solver, spec, config, meta, cil, analyses, warnings, stats, file_loc) => {
9393
let cil =
9494
switch (cil) {
9595
| Ok(s) =>
@@ -128,9 +128,15 @@ let init = (solver, spec, config, meta, cil, analyses, warnings, stats) => {
128128
| _ => raise(InitFailed("Failed to load runtime stats"))
129129
};
130130

131+
let file_loc =
132+
switch (file_loc) {
133+
| Ok(s) => Marshal.from_string(s, 0)
134+
| _ => raise(InitFailed("Failed to load file path table"))
135+
};
136+
131137
print_endline("Rendering app...");
132138
React.Dom.renderToElementWithId(
133-
<Main cil goblint warnings meta stats />,
139+
<Main cil goblint warnings meta stats file_loc/>,
134140
"app",
135141
);
136142
};
@@ -153,15 +159,16 @@ let handle_error = exc => {
153159
"./analyses.marshalled",
154160
"./warnings.marshalled",
155161
"./stats.marshalled",
162+
"./file_loc.marshalled",
156163
]
157164
|> List.map(HttpClient.get)
158165
|> Lwt.all
159166
>>= (
160167
l =>
161168
Lwt.return(
162169
switch (l) {
163-
| [solver, spec, config, meta, cil, analyses, warnings, stats] =>
164-
try(init(solver, spec, config, meta, cil, analyses, warnings, stats)) {
170+
| [solver, spec, config, meta, cil, analyses, warnings, stats, file_loc] =>
171+
try(init(solver, spec, config, meta, cil, analyses, warnings, stats, file_loc)) {
165172
| exc => handle_error(exc)
166173
}
167174
| _ => ()

‎src/Main.re‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
open Batteries;
22

33
[@react.component]
4-
let make = (~cil, ~goblint, ~warnings, ~meta, ~stats) => {
4+
let make = (~cil, ~goblint, ~warnings, ~meta, ~stats, ~file_loc) => {
55
let (state, dispatch) =
66
React.useReducer(
77
Reducer.reducer,
8-
State.make(~cil, ~goblint, ~warnings, ~meta, ~stats, ()),
8+
State.make(~cil, ~goblint, ~warnings, ~meta, ~stats, ~file_loc, ()),
99
);
1010

1111
let fetch_file =
@@ -38,7 +38,7 @@ let make = (~cil, ~goblint, ~warnings, ~meta, ~stats) => {
3838
React.useEffect1(
3939
() => {
4040
switch (state.display) {
41-
| Some(File(f)) when Option.is_none(f.contents) => fetch_file(f.path)
41+
| Some(File(f)) when Option.is_none(f.contents) => fetch_file(Hashtbl.find(file_loc, f.path))
4242
| Some(Func(f)) when Option.is_none(f.dot) =>
4343
fetch_dot(f.name, f.file)
4444
| _ => ()

‎src/Panel.re‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -52,8 +52,7 @@ let make = (~state, ~dispatch) => {
5252
<div className="tab-content">
5353
<div className="tab-pane active">
5454
{switch (current) {
55-
| Some(Warnings) =>
56-
<WarningView warnings={state.warnings} dispatch />
55+
| Some(Warnings) => <WarningView warnings={state.warnings} dispatch />
5756
| Some(DeadCode) => <DeadCodeView locations dispatch />
5857
| Some(Parameters) => <ParameterView parameters />
5958
| Some(Statistics) => <GvStatisticsView stats={state.stats} />

‎src/dune‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@
1010
goblint-cil
1111
goblint-cil.syntacticsearch
1212
goblint.lib
13+
goblint.timing
1314
goblint.sites.js
1415
goblint.build-info.js
1516
integers_stubs_js

‎src/state/state.ml‎

Lines changed: 14 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -22,27 +22,37 @@ type t = {
2222
goblint : GvGoblint.solver_state;
2323
warnings : GvMessages.t;
2424
meta : Yojson.Safe.t;
25-
stats : Stats.t * Gc.stat;
25+
stats : Goblint_timing.tree * Gc.stat;
26+
file_loc : (string, string) Hashtbl.t;
2627
display : display option;
2728
inspect : inspect option;
2829
selected_sidebar : selected_sidebar;
2930
selected_panel : selected_panel option;
3031
search : Search.t;
3132
}
3233

34+
let timing_default : Goblint_timing.tree = {
35+
name = "";
36+
cputime = 0.0;
37+
walltime = 0.0;
38+
allocated = 0.0;
39+
count = 0;
40+
children = [];
41+
}
3342
let default =
3443
{
3544
cil = Cil.dummyFile;
3645
goblint = GvGoblint.empty;
3746
warnings = [];
3847
meta = `Null;
39-
stats = (Stats.top, Gc.quick_stat ());
48+
stats = (timing_default, Gc.quick_stat ());
49+
file_loc = Hashtbl.create 113;
4050
display = None;
4151
inspect = None;
4252
selected_sidebar = SelectedSidebar.Nodes;
4353
selected_panel = None;
4454
search = Search.default;
4555
}
4656

47-
let make ~cil ~goblint ~warnings ~meta ~stats () =
48-
{ default with cil; goblint; warnings; meta; stats }
57+
let make ~cil ~goblint ~warnings ~meta ~stats ~file_loc () =
58+
{ default with cil; goblint; warnings; meta; stats; file_loc }

‎src/ui/panel/gvStatisticsView.re‎

Lines changed: 19 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,21 +1,22 @@
11
open Batteries;
2-
module Stats = GoblintCil.Stats;
2+
3+
module Timing = Goblint_timing
34

45
let rec make_task_list = tasks =>
56
if (List.is_empty(tasks)) {
67
React.null;
78
} else {
89
<ul>
910
{tasks
10-
|> List.mapi((i, task: Stats.t) => {
11+
|> List.mapi((i, task: Timing.tree) => {
1112
let key = string_of_int(i);
1213
<li key>
1314
{task.name
1415
++ ": "
15-
++ string_of_float(task.time)
16+
++ string_of_float(task.cputime)
1617
++ " s"
1718
|> React.string}
18-
{task.sub |> List.rev |> make_task_list}
19+
{task.children |> List.rev |> make_task_list}
1920
</li>;
2021
})
2122
|> React.list}
@@ -26,16 +27,23 @@ let as_megabytes = words => Printf.sprintf("%.2f MB", words /. 131072.0);
2627

2728
[@react.component]
2829
let make = (~stats) => {
29-
let (time: Stats.t, gc: Gc.stat) = stats;
30+
let (time: Timing.tree, gc: Gc.stat) = stats;
3031
let total =
31-
time.sub |> List.fold_left((acc, sub: Stats.t) => acc +. sub.time, 0.0);
32+
time.children |> List.fold_left((acc, sub: Timing.tree) => acc +. sub.cputime, 0.0);
3233

3334
<div>
34-
<span>
35+
{if(total == 0.) {
36+
<div className="bg-warning">
37+
{"For timing statistics the analysis has to be run with -v (alternatively, either option dbg.verbose or dbg.timing.enabled can be activated)" |> React.string}
38+
</div>;
39+
} else {
40+
React.null
41+
}}
42+
<div>
3543
{"Total: " ++ string_of_float(total) ++ " s" |> React.string}
36-
</span>
37-
{time.sub |> List.rev |> make_task_list}
38-
<span>
44+
</div>
45+
{time.children |> List.rev |> make_task_list}
46+
<div>
3947
{Printf.sprintf(
4048
"Memory: total=%s, max=%s, minor=%s, major=%s, promoted=%s, minor collections=%d, major collections=%d, compactions=%d",
4149
as_megabytes(gc.minor_words +. gc.major_words -. gc.promoted_words),
@@ -48,6 +56,6 @@ let make = (~stats) => {
4856
gc.compactions,
4957
)
5058
|> React.string}
51-
</span>
59+
</div>
5260
</div>;
5361
};

0 commit comments

Comments
 (0)