diff --git a/src/plugins/alias/abstract_state.ml b/src/plugins/alias/abstract_state.ml
index 04ac839880f0bbafce7d228d3cc25fe95f59520a..dd031ad6cadbabbc6a3186ee9acf3589bf82393e 100644
--- a/src/plugins/alias/abstract_state.ml
+++ b/src/plugins/alias/abstract_state.ml
@@ -117,7 +117,6 @@ let pretty ?(debug=false) =
(** invariants of type t must be true before and after each functon call *)
let assert_invariants (x:t) : unit =
- (* Format.printf "DEBUG Checking invariants@.%a@." (pretty ~debug:true) x; *)
(* check that all vertex of the graph have entries in pending and
vmap, and are integer between 0 and cmpt, and have at most 1
successor *)
@@ -144,6 +143,13 @@ let assert_invariants (x:t) : unit =
in
VMap.iter assert_vmap x.vmap
+(* for debuging *)
+let assert_invariants x =
+ try assert_invariants x
+ with
+ Assert_failure f -> (Format.printf "DEBUG FAILED INVARIANTS@.%a@." (pretty ~debug:true) x; raise (Assert_failure f))
+
+
(* find the vertex of an lval *)
let find_vertex (lv:lval) (x:t) =
LMap.find lv x.lmap
@@ -339,11 +345,11 @@ let join (x:t) (v1:V.t) (v2:V.t) : t =
let cjoin (x:t) (v1:V.t) (v2:V.t) : t =
assert_invariants x;
- let pt2= G.succ x.graph v2 in
+ let pt2 = G.succ x.graph v2 in
if pt2 = []
then
- let old_set = try VMap.find v2 x.pending with Not_found -> VSet.empty in
- let new_pending = VMap.add v2 (VSet.add v2 old_set) x.pending in
+ let old_set = try VMap.find v1 x.pending with Not_found -> VSet.empty in
+ let new_pending = VMap.add v1 (VSet.add v2 old_set) x.pending in
{x with pending=new_pending}
else
join x v1 v2
@@ -371,7 +377,8 @@ let assignment_x_y (a:t) (x:lval) (y:lval) : t =
assert_invariants a;
let (v1,a) = find_or_create_vertex x a in
let (v2,a) = find_or_create_vertex y a in
- cjoin a v1 v2
+ let new_a = cjoin a v1 v2 in
+ assert_invariants new_a ; new_a
(* assignment x = &y *)
@@ -379,10 +386,12 @@ let assignment_x_addr_y (a:t) (x:lval) (y:lval) : t =
assert_invariants a;
let v1, a = find_or_create_vertex x a in
let list_v2, a = addr_of y a in
- List.fold_left
+ let new_a = List.fold_left
(fun a_acc v2 -> join a_acc v1 v2)
a
list_v2
+ in
+ assert_invariants new_a ; new_a
(* TODO is that correct ?*)
@@ -391,38 +400,51 @@ let assignment_x_ptr_y (a:t) (x:lval) (y:lval) : t =
assert_invariants a;
let v1, a = find_or_create_vertex x a in
let list_v2, a = points_to y a in
+ let new_a =
match list_v2 with
[] -> let v2 = find_vertex y a in set_type a v2 v1
| [v2] -> cjoin a v1 v2
| _ -> failwith "assignment_x_ptr_y not implemented"
+ in
+ assert_invariants new_a ; new_a
(* assignment x = allocate(y) *)
let assignment_x_allocate_y (a:t) (x:lval) : t =
+ assert_invariants a;
let (v1,a) = find_or_create_vertex x a in
let (v2,a) = create_cst_vertex a in
- set_type a v1 v2
+ let new_a = set_type a v1 v2 in
+ assert_invariants new_a ; new_a
(* assignment *x = y *)
let assignment_ptr_x_y (a:t) (x:lval) (y:lval) : t =
+ assert_invariants a;
let v2, a = find_or_create_vertex y a in
let list_v1, a = points_to x a in
+ let new_a =
match list_v1 with
[] -> let v1 = find_vertex x a in set_type a v1 v2
| [v1] -> cjoin a v1 v2
| _ -> failwith "assignment_ptr_x_y not implemented"
+ in
+ assert_invariants new_a ; new_a
(* assignment *x = cst *)
let assignment_ptr_x_cst (a:t) (x:lval) : t =
+ assert_invariants a;
(* Format.printf "DEBUG (assignment_ptr_x_cst) on lval %a and state:@. %a @." Lval.pretty x print_debug a; *)
let v2, a = create_cst_vertex a in
let (list_v1, a) : V.t list * t = points_to x a in
+ let new_a =
match list_v1 with
[] -> let v1 = find_vertex x a in set_type a v1 v2
| _ -> let f_fold (acc:t) (v1:V.t) : t = cjoin acc v1 v2
in List.fold_left f_fold a list_v1
+ in
+ assert_invariants new_a ; new_a
-
+
(* we don't need to iterate on loops *)
let equal (_:t) (_:t) = true
@@ -726,7 +748,7 @@ let call (state:t) (res:lval option) (args:exp list) (summary:summary) :t =
let formals = summary.formals in
let sum_state =
match summary.state with
- None -> failwith "this should not hapen"
+ None -> failwith "BUG this should not happen"
| Some s -> s
in
assert (List.length args = List.length formals);
@@ -740,7 +762,7 @@ let call (state:t) (res:lval option) (args:exp list) (summary:summary) :t =
let new_state =List.fold_left2
(fun acc param formal ->
begin
- match formal,find_basic_lval param with
+ match formal, find_basic_lval param with
((Var v1, NoOffset), BLval (Var v2,NoOffset)) ->
(* case x = y *)
assignment_x_y acc (Var v1, NoOffset) (Var v2, NoOffset)
diff --git a/src/plugins/alias/analysis.ml b/src/plugins/alias/analysis.ml
index 1b7f808f59cd62c3ab5b995815f8da4f22f94f58..0aa96174c78a9d9b04d5ecb5e82c3c518a48345e 100644
--- a/src/plugins/alias/analysis.ml
+++ b/src/plugins/alias/analysis.ml
@@ -168,7 +168,8 @@ struct
| Call(res,ef,es,(loc,_)) -> (* !function_compute_ref ef *)
begin
let summary = match Kernel_function.get_called ef with
- | Some kf -> (try Function_table.find kf with Not_found -> None)
+ | Some kf -> (try Function_table.find kf
+ with Not_found -> !function_compute_ref kf ; Function_table.find kf)
| None -> Options.abort ~source:loc
"Unsupported function pointer (skipped)"
in
@@ -219,15 +220,23 @@ let doFunction (kf:kernel_function) =
Options.feedback ~level:2 "entering in function %a."
Kernel_function.pretty kf;
if Kernel_function.has_definition kf then
- let first_stmts = try [Kernel_function.find_first_stmt kf] with Kernel_function.No_Statement -> [] in
+ let first_stmts =
+ try [Kernel_function.find_first_stmt kf]
+ with Kernel_function.No_Statement -> [] in
List.iter (fun stmt -> T.StmtStartData.add stmt (Some Abstract_state.initial_value)) first_stmts;
F.compute first_stmts;
- let return_stmt = Kernel_function.find_return kf in
- let final_state : Abstract_state.t option = try Stmt_table.find return_stmt with Not_found -> None in
- let summary: Abstract_state.summary =
- Abstract_state.make_summary final_state kf
- in
- Function_table.add kf (Some summary)
+ if not (Kernel_function.is_main kf) then
+ (* if main, do nothing *)
+ let return_stmt = Kernel_function.find_return kf in
+ let final_state : Abstract_state.t option =
+ try Stmt_table.find return_stmt
+ with
+ Not_found -> failwith "Houston, we have a problem"
+ in
+ let summary: Abstract_state.summary =
+ Abstract_state.make_summary final_state kf
+ in
+ Function_table.add kf (Some summary)
let () = function_compute_ref := doFunction
diff --git a/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle b/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle
index d58abf402f98a746214a5a17d87fa6d608ce6754..5265a9c8a9a141547dd5f8dd69ef2b999fc3e8b7 100644
--- a/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle
@@ -5,36 +5,35 @@ After statement a = b; :
<list of may-alias>
{ a; b } are aliased
<end of list>
-
+
After statement b = c; :
<list of may-alias>
{ a; b; c } are aliased
<end of list>
-
+
After statement *a = 4; :
<list of may-alias>
{ a; b; c } are aliased
<end of list>
-
+
After statement *c = e; :
<list of may-alias>
{ a; b; c } are aliased
<end of list>
-
+
After statement a = d; :
<list of may-alias>
{ a; b; c; d } are aliased
<end of list>
-
+
After statement __retres = 0; :
<list of may-alias>
{ a; b; c; d } are aliased
<end of list>
-
+
After statement return __retres; :
<list of may-alias>
{ a; b; c; d } are aliased
<end of list>
-
[alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle b/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle
index c84a067cd851a6bcbb84fd145d5698de0a7b07a4..aaabce7aebc5fef10f58f0cadc6f3f48e13413c2 100644
--- a/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle
@@ -4,28 +4,27 @@
After statement *a = b; :
<list of may-alias>
<end of list>
-
+
After statement *c = d; :
<list of may-alias>
<end of list>
-
+
After statement a = c; :
<list of may-alias>
{ a; c } are aliased
{ b; d } are aliased
<end of list>
-
+
After statement __retres = 0; :
<list of may-alias>
{ a; c } are aliased
{ b; d } are aliased
<end of list>
-
+
After statement return __retres; :
<list of may-alias>
{ a; c } are aliased
{ b; d } are aliased
<end of list>
-
[alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/assignment3.res.oracle b/src/plugins/alias/tests/basic/oracle/assignment3.res.oracle
index 0561d9e9ab9c8d15ad9e861e746f8542f4ab4292..97a840081bc0a497e8c6f1c54a712ca28a06266a 100644
--- a/src/plugins/alias/tests/basic/oracle/assignment3.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/assignment3.res.oracle
@@ -4,18 +4,17 @@
After statement a = & b; :
<list of may-alias>
<end of list>
-
+
After statement *c = b; :
<list of may-alias>
<end of list>
-
+
After statement __retres = 0; :
<list of may-alias>
<end of list>
-
+
After statement return __retres; :
<list of may-alias>
<end of list>
-
[alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/cast1.res.oracle b/src/plugins/alias/tests/basic/oracle/cast1.res.oracle
index c695eede8c71619a3236d7593960d90f6115a079..5ce038e47f6e21cc643a24c553ab59f732720314 100644
--- a/src/plugins/alias/tests/basic/oracle/cast1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/cast1.res.oracle
@@ -5,24 +5,23 @@ After statement a = (int *)c; :
<list of may-alias>
{ a; c } are aliased
<end of list>
-
+
After statement d = (float *)b; :
<list of may-alias>
{ a; c } are aliased
{ b; d } are aliased
<end of list>
-
+
After statement __retres = 0; :
<list of may-alias>
{ a; c } are aliased
{ b; d } are aliased
<end of list>
-
+
After statement return __retres; :
<list of may-alias>
{ a; c } are aliased
{ b; d } are aliased
<end of list>
-
[alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/conditional1.res.oracle b/src/plugins/alias/tests/basic/oracle/conditional1.res.oracle
index 65e65c6dd5dc377ebe180470ac7ade7b2a528405..0556445f9b9f808fc5309972895acc97534d6104 100644
--- a/src/plugins/alias/tests/basic/oracle/conditional1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/conditional1.res.oracle
@@ -4,31 +4,30 @@
After statement if (a) a = b; else a = c; :
<list of may-alias>
<end of list>
-
+
After statement a = b; :
<list of may-alias>
{ a; b } are aliased
<end of list>
-
+
After statement a = c; :
<list of may-alias>
{ a; c } are aliased
<end of list>
-
+
After statement *a = 4; :
<list of may-alias>
{ a; b } are aliased
<end of list>
-
+
After statement __retres = 0; :
<list of may-alias>
{ a; b } are aliased
<end of list>
-
+
After statement return __retres; :
<list of may-alias>
{ a; b } are aliased
<end of list>
-
[alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/function1.res.oracle b/src/plugins/alias/tests/basic/oracle/function1.res.oracle
index 1e21b12466eec359b94fec19ff37dbb9572c5101..2506c2557304a1a3df317bdaacee05ecb9bcff0d 100644
--- a/src/plugins/alias/tests/basic/oracle/function1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/function1.res.oracle
@@ -1,45 +1,44 @@
[kernel] Parsing function1.c (with preprocessing)
[alias] Parsing done
-[alias] Skiping swap(a,b); (doInstr not implemented)
-[alias] Skiping swap(a,b); (doInstr not implemented)
-[alias] Skiping swap(c,d); (doInstr not implemented)
-[alias] Skiping swap(c,d); (doInstr not implemented)
+[alias] Skiping swap(a,b); (summary not found)
+[alias] Skiping swap(a,b); (summary not found)
+[alias] Skiping swap(c,d); (summary not found)
+[alias] Skiping swap(c,d); (summary not found)
[alias] Functions done
After statement z = x; :
<list of may-alias>
{ x; z } are aliased
<end of list>
-
+
After statement x = y; :
<list of may-alias>
{ x; y; z } are aliased
<end of list>
-
+
After statement y = z; :
<list of may-alias>
{ x; y; z } are aliased
<end of list>
-
+
After statement swap(a,b); :
<list of may-alias>
<end of list>
-
+
After statement swap(c,d); :
<list of may-alias>
<end of list>
-
+
After statement __retres = 0; :
<list of may-alias>
<end of list>
-
+
After statement return; :
<list of may-alias>
{ x; y; z } are aliased
<end of list>
-
+
After statement return __retres; :
<list of may-alias>
<end of list>
-
[alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/while_for1.res.oracle b/src/plugins/alias/tests/basic/oracle/while_for1.res.oracle
index c0fe770c0e1944ff02dc2de032a84bbdf5fcfb84..9383a1891db6013dca39eeadd7fd4dda3ce44f8c 100644
--- a/src/plugins/alias/tests/basic/oracle/while_for1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/while_for1.res.oracle
@@ -2,6 +2,7 @@
[alias] Parsing done
[alias] Skipping assignment odata[idx] = 0.5 * idata[idx] (not implemented)
[alias] Skipping assignment odata[idx] = 0.5 * idata[idx] (not implemented)
+[alias] Skipping assignment odata[idx] = 0.5 * idata[idx] (not implemented)
[alias] Functions done
After statement while (1) {
idx = 0;
@@ -12,7 +13,7 @@ After statement while (1) {
} :
<list of may-alias>
<end of list>
-
+
After statement idx = 0;
while (idx < 10) {
odata[idx] = 0.5 * idata[idx];
@@ -20,37 +21,51 @@ After statement idx = 0;
} :
<list of may-alias>
<end of list>
-
+
+After statement idx = 0; :
+ <list of may-alias>
+<end of list>
+
After statement idx = 0; :
<list of may-alias>
<end of list>
-
+
+After statement while (idx < 10) {
+ odata[idx] = 0.5 * idata[idx];
+ idx ++;
+ } :
+ <list of may-alias>
+<end of list>
+
After statement while (idx < 10) {
odata[idx] = 0.5 * idata[idx];
idx ++;
} :
<list of may-alias>
<end of list>
-
+
After statement if (! (idx < 10)) break; :
<list of may-alias>
<end of list>
-
+
After statement break; :
<list of may-alias>
<end of list>
-
+
+After statement odata[idx] = 0.5 * idata[idx]; :
+ <list of may-alias>
+<end of list>
+
After statement odata[idx] = 0.5 * idata[idx]; :
<list of may-alias>
<end of list>
-
+
After statement odata[idx] = 0.5 * idata[idx]; :
<list of may-alias>
<end of list>
-
+
After statement idx ++; :
<list of may-alias>
<end of list>
-
[alias] Analysis complete