diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml index 337a2c6cfddb2150e52bccb0c48a58437f905907..56c8a9ff5e11aea307b7d942ee04c0b852400193 100644 --- a/src/plugins/dive/build.ml +++ b/src/plugins/dive/build.ml @@ -259,16 +259,29 @@ let build_node_deps context node = match stmt.skind with | Instr _ when not effects.Studia.Writes.direct -> () | Instr instr -> - (* Keep only callstacks which are a compatible with the current one *) - let states = Db.Value.get_stmt_state_callstack ~after:false stmt in - let callstacks = match states with - | None -> assert false - | Some table -> - let module Table = Value_types.Callstack.Hashtbl in - Table.fold (fun cs _ acc -> cs :: acc) table [] + let callstacks = + if callstack <> [] && + Kernel_function.(equal + (find_englobing_kf stmt) + (Callstack.top_kf callstack)) + then + (* slight improvement which only work when there is no recursion + and which is only usefull because you currently can't have + all callstacks due to memexec -> in this particular case + we are sure not to miss the only admissible callstack *) + [callstack] + else + (* Keep only callstacks which are a compatible with the current one *) + let states = Db.Value.get_stmt_state_callstack ~after:false stmt in + let callstacks = match states with + | None -> assert false + | Some table -> + let module Table = Value_types.Callstack.Hashtbl in + Table.fold (fun cs _ acc -> cs :: acc) table [] + in + (* TODO: missing callstacks filtered by memexec *) + Callstack.filter_truncate callstacks callstack in - (* TODO: missing callstacks filtered by memexec *) - let callstacks = Callstack.filter_truncate callstacks callstack in (* Create a dependency for each of them *) List.iter (fun cs -> build_instr_deps cs stmt instr) callstacks | _ -> assert false diff --git a/src/plugins/dive/callstack.ml b/src/plugins/dive/callstack.ml index f9d5ae7157af009b2a6e8ff9fbef400c0363af09..490fe5dc5c6a6eb9218527e2c86e9fe7de885eb0 100644 --- a/src/plugins/dive/callstack.ml +++ b/src/plugins/dive/callstack.ml @@ -35,6 +35,11 @@ let pop cs = | [(_,Kglobal)] -> None | (kf,Kstmt stmt) :: t -> Some (kf,stmt,t) +let top_kf cs = + match cs with + | [] | (_,Kglobal) :: _ :: _ | [(_,Kstmt _)] -> assert false (* Invariant *) + | (kf,_) :: _ -> kf + let rec pop_downto top_kf = function | [] -> failwith "the callstack doesn't contain this function" | ((kf,_kinstr) :: tail) as cs -> @@ -62,10 +67,10 @@ let rec is_prefix cs1 cs2 = let truncate_to_sub full_cs sub_cs = let rec aux acc = function | [] -> None - | (s :: t) as cs -> - if is_prefix sub_cs cs - then Some (List.rev acc @ sub_cs) - else aux (s :: acc) t + | (s :: t) as cs -> + if is_prefix sub_cs cs + then Some (List.rev acc @ sub_cs) + else aux (s :: acc) t in aux [] full_cs diff --git a/src/plugins/dive/callstack.mli b/src/plugins/dive/callstack.mli index 7d3dce8a4b29636369fa7d247ddc4f8c45eccacf..c31f1ef3d08390e0045ee4a267a6596b0d9fd4ac 100644 --- a/src/plugins/dive/callstack.mli +++ b/src/plugins/dive/callstack.mli @@ -27,12 +27,13 @@ include Datatype.S_with_collections with type t := t (* The callstacks manipulated here have the following invariant: - the callstack is never an empty list - - the last item of the list has alwas a Kglobal + - the last item of the list has always a Kglobal - all elements of the list except the last have a Kstmt *) val init : Cil_types.kernel_function -> t val pop : t -> (Cil_types.kernel_function * Cil_types.stmt * t) option val pop_downto : Cil_types.kernel_function -> t -> t +val top_kf : t -> Cil_types.kernel_function val push : Cil_types.kernel_function * Cil_types.stmt -> t -> t val is_prefix : t -> t -> bool val truncate_to_sub : t -> t -> t option diff --git a/src/plugins/dive/tests/dive/global.i b/src/plugins/dive/tests/dive/global.i new file mode 100644 index 0000000000000000000000000000000000000000..d475e3862e4bc171284629d6eed890587c80f8bf --- /dev/null +++ b/src/plugins/dive/tests/dive/global.i @@ -0,0 +1,14 @@ +/* run.config +STDOPT: +"-dive-from main::z" +*/ + +float g; + +float main(float x) +{ + float y = x + 1; + g = y; + float z = g + x; + return z; +} + diff --git a/src/plugins/dive/tests/dive/oracle/global.dot b/src/plugins/dive/tests/dive/oracle/global.dot new file mode 100644 index 0000000000000000000000000000000000000000..e5d9191e202a8921e5487f4b55984c229f3fffa0 --- /dev/null +++ b/src/plugins/dive/tests/dive/oracle/global.dot @@ -0,0 +1,22 @@ +digraph G { + cp0 [style="invis,dotted", ]; + cp1 [label=<z>, shape=box, ]; + cp2 [style="invis,dotted", ]; + cp3 [label=<g>, shape=box, fillcolor="#FFBBBB", color="#FF0000", + style="filled", ]; + cp4 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000", + style="filled", ]; + cp5 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000", + style="filled", ]; + + subgraph cluster_cs_1 { label=<main>; cp5;cp4;cp1;cp0; + }; + subgraph cluster_file_1 { label=<tests/dive/global.i>; cp3;cp2; + }; + + cp3 -> cp1; + cp4 -> cp1; + cp4 -> cp5; + cp5 -> cp3; + + } \ No newline at end of file diff --git a/src/plugins/dive/tests/dive/oracle/global.res.oracle b/src/plugins/dive/tests/dive/oracle/global.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..18bb2bf74bd45b8a6a8bb7bd2faf4cb4222cb9f0 --- /dev/null +++ b/src/plugins/dive/tests/dive/oracle/global.res.oracle @@ -0,0 +1,8 @@ +[kernel] Parsing tests/dive/global.i (no preprocessing) +[eva] Analyzing a complete application starting at main +[eva] Computing initial state +[eva] Initial state computed +[eva:alarm] tests/dive/global.i:11: Warning: + non-finite float value. assert \is_finite((float)(g + x)); +[eva] done for function main +[dive] output to tests/dive/result/global.dot diff --git a/src/plugins/dive/tests/dive/oracle/various.dot b/src/plugins/dive/tests/dive/oracle/various.dot index 500799fd2fa7fd54bfd0584dac7180019bf1e4ed..4ce0ff968e2f3b97fd2b9987d3dfcf5f8a39d62c 100644 --- a/src/plugins/dive/tests/dive/oracle/various.dot +++ b/src/plugins/dive/tests/dive/oracle/various.dot @@ -47,8 +47,8 @@ digraph G { subgraph cluster_file_1 { label=<tests/dive/various.i>; cp6;cp5; }; - cp1 -> cp2 [style="bold", ]; - cp2 -> cp1 [style="bold", ]; + cp1 -> cp2; + cp2 -> cp1; cp2 -> cp18; cp4 -> cp1; cp4 -> cp4;