From ffb8b4cc9a3295d5a1ad2cceac7ea76fde587a0b Mon Sep 17 00:00:00 2001
From: Jan Rochel <jan.rochel@cea.fr>
Date: Wed, 6 Mar 2024 18:24:17 +0100
Subject: [PATCH] [alias] fix inverted offsets
The readout reconstructed offsets in the wrong order.
This fixes tests/known_bugs/union_readback.c
Fixes #1368
---
src/plugins/alias/src/abstract_state.ml | 4 +-
.../tests/fixed_bugs/oracle/origin.res.oracle | 8 +-
.../oracle/union_readback.res.oracle | 16 +++
.../union_readback.c | 0
.../tests/offsets/oracle/nested2.res.oracle | 10 +-
.../real_world/oracle/example1.res.oracle | 64 ++++++------
.../real_world/oracle/example2.res.oracle | 98 +++++++++----------
7 files changed, 107 insertions(+), 93 deletions(-)
create mode 100644 src/plugins/alias/tests/fixed_bugs/oracle/union_readback.res.oracle
rename src/plugins/alias/tests/{known_bugs => fixed_bugs}/union_readback.c (100%)
diff --git a/src/plugins/alias/src/abstract_state.ml b/src/plugins/alias/src/abstract_state.ml
index 811472106b7..1878a7f6e60 100644
--- a/src/plugins/alias/src/abstract_state.ml
+++ b/src/plugins/alias/src/abstract_state.ml
@@ -171,14 +171,14 @@ module Readout = struct
(fun e ->
let pred_lvals = checking_for_cycles s visited @@ E.src e in
let modify_lval lv = match E.label e with
- | Field f -> let lhost, o = lv in lhost, Field (f, o)
+ | Field f -> Cil.addOffsetLval (Field (f, NoOffset)) lv
| Pointer ->
(* TODO: This Cil.typeOfLval may crash with a fatal kernel
error for certain reconstructed lvals involving a union
type. See tests/known_bugs/union_readback.c *)
let ty = Cil.typeOfLval lv in
if Cil.isArrayType ty then
- let lhost, o = lv in lhost, Index (Simplified.nul_exp, o)
+ Cil.addOffsetLval (Index (Simplified.nul_exp, NoOffset)) lv
else
let () = if not @@ Cil.isPointerType ty then
Options.debug "unexpected type: %a" Printer.pp_typ ty
diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/origin.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/origin.res.oracle
index 61e807ea83e..be7875287ef 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/origin.res.oracle
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/origin.res.oracle
@@ -11,19 +11,19 @@
[alias:unsafe-cast] origin.c:8: Warning:
unsafe cast from int * to char *; analysis may be unsound
[alias] May-aliases after instruction tmp = (void (*)(void))*((char *)(v.t)); are
- { v[0..].t; tmp }
+ { v.t[0..]; tmp }
[alias] May-alias graph after instruction tmp = (void (*)(void))*((char *)(v.t));
is 0:{ tmp } → 1:{ f } 4:{ v } -t→ 5:{ } 5:{ } → 0:{ tmp }
[alias] analysing instruction: int g = (int)tmp;
[alias:unsafe-cast] origin.c:8: Warning:
unsafe cast from void (*)(void) to int; analysis may be unsound
-[alias] May-aliases after instruction int g = (int)tmp; are { v[0..].t; tmp }
+[alias] May-aliases after instruction int g = (int)tmp; are { v.t[0..]; tmp }
[alias] May-alias graph after instruction int g = (int)tmp; is
0:{ tmp } → 1:{ f } 4:{ v } -t→ 5:{ } 5:{ } → 0:{ tmp }
-[alias] May-aliases at the end of function f: { v[0..].t; tmp }
+[alias] May-aliases at the end of function f: { v.t[0..]; tmp }
[alias] May-alias graph at the end of function f:
0:{ tmp } → 1:{ f } 4:{ v } -t→ 5:{ } 5:{ } → 0:{ tmp }
[alias] Summary of function f:
formals: locals: g tmp→{ f } returns: <none>
- state: { v[0..].t; tmp }
+ state: { v.t[0..]; tmp }
[alias] Analysis complete
diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/union_readback.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/union_readback.res.oracle
new file mode 100644
index 00000000000..65fd01657cf
--- /dev/null
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/union_readback.res.oracle
@@ -0,0 +1,16 @@
+[kernel] Parsing union_readback.c (with preprocessing)
+[alias] analysing function: f
+[alias] analysing instruction: flag.r.v = o;
+[alias] May-aliases after instruction flag.r.v = o; are
+ { o; flag.r.v } { *o; *(flag.r.v) }
+[alias] May-alias graph after instruction flag.r.v = o; is
+ 0:{ flag } -r→ 1:{ } 1:{ } -v→ 2:{ o } 2:{ o } → 4:{ }
+ 4:{ } → 5:{ }
+[alias] May-aliases at the end of function f: { o; flag.r.v } { *o; *(flag.r.v) }
+[alias] May-alias graph at the end of function f:
+ 0:{ flag } -r→ 1:{ } 1:{ } -v→ 2:{ o } 2:{ o } → 4:{ }
+ 4:{ } → 5:{ }
+[alias] Summary of function f:
+ formals: o locals: flag returns: <none>
+ state: { o; flag.r.v } { *o; *(flag.r.v) }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/known_bugs/union_readback.c b/src/plugins/alias/tests/fixed_bugs/union_readback.c
similarity index 100%
rename from src/plugins/alias/tests/known_bugs/union_readback.c
rename to src/plugins/alias/tests/fixed_bugs/union_readback.c
diff --git a/src/plugins/alias/tests/offsets/oracle/nested2.res.oracle b/src/plugins/alias/tests/offsets/oracle/nested2.res.oracle
index 8cfb818473b..70e6a01b0b6 100644
--- a/src/plugins/alias/tests/offsets/oracle/nested2.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/nested2.res.oracle
@@ -55,7 +55,7 @@
unsafe cast from st_2_t * to struct struct_2_t *; analysis may be unsound
[alias] May-aliases after instruction t->t = (struct struct_2_t *)z1; are
{ t->t; z1 } { (t->t)->c; z1->c; a } { (t->t)->s; z1->s }
- { (*(t->t))[0..].s; (*z1)[0..].s }
+ { (t->t)->s[0..]; z1->s[0..] }
[alias] May-alias graph after instruction t->t = (struct struct_2_t *)z1; is
1:{ } -s→ 6:{ } 1:{ } -c→ 12:{ a } 2:{ t } → 3:{ }
3:{ } -t→ 13:{ z1 } 6:{ } → 7:{ } 7:{ } → 8:{ x1; x2 }
@@ -63,7 +63,7 @@
[alias] analysing instruction: t->d = a;
[alias] May-aliases after instruction t->d = a; are
{ t->t; z1 } { (t->t)->c; z1->c; t->d; a } { (t->t)->s; z1->s }
- { (*(t->t))[0..].s; (*z1)[0..].s }
+ { (t->t)->s[0..]; z1->s[0..] }
[alias] May-alias graph after instruction t->d = a; is
1:{ } -s→ 6:{ } 1:{ } -c→ 14:{ a } 2:{ t } → 3:{ }
3:{ } -t→ 13:{ z1 } 3:{ } -d→ 14:{ a } 6:{ } → 7:{ }
@@ -71,14 +71,14 @@
[alias] analysing instruction: __retres = 0;
[alias] May-aliases after instruction __retres = 0; are
{ t->t; z1 } { (t->t)->c; z1->c; t->d; a } { (t->t)->s; z1->s }
- { (*(t->t))[0..].s; (*z1)[0..].s }
+ { (t->t)->s[0..]; z1->s[0..] }
[alias] May-alias graph after instruction __retres = 0; is
1:{ } -s→ 6:{ } 1:{ } -c→ 14:{ a } 2:{ t } → 3:{ }
3:{ } -t→ 13:{ z1 } 3:{ } -d→ 14:{ a } 6:{ } → 7:{ }
7:{ } → 8:{ x1; x2 } 13:{ z1 } → 1:{ } 14:{ a } → 5:{ }
[alias] May-aliases at the end of function main:
{ t->t; z1 } { (t->t)->c; z1->c; t->d; a } { (t->t)->s; z1->s }
- { (*(t->t))[0..].s; (*z1)[0..].s }
+ { (t->t)->s[0..]; z1->s[0..] }
[alias] May-alias graph at the end of function main:
1:{ } -s→ 6:{ } 1:{ } -c→ 14:{ a } 2:{ t } → 3:{ }
3:{ } -t→ 13:{ z1 } 3:{ } -d→ 14:{ a } 6:{ } → 7:{ }
@@ -86,5 +86,5 @@
[alias] Summary of function main:
formals: locals: x1 x2 z1 t a __retres returns: __retres
state: { t->t; z1 } { (t->t)->c; z1->c; t->d; a } { (t->t)->s; z1->s }
- { (*(t->t))[0..].s; (*z1)[0..].s }
+ { (t->t)->s[0..]; z1->s[0..] }
[alias] Analysis complete
diff --git a/src/plugins/alias/tests/real_world/oracle/example1.res.oracle b/src/plugins/alias/tests/real_world/oracle/example1.res.oracle
index a83fa243f1a..d0c1c5e7a0b 100644
--- a/src/plugins/alias/tests/real_world/oracle/example1.res.oracle
+++ b/src/plugins/alias/tests/real_world/oracle/example1.res.oracle
@@ -14,22 +14,22 @@
0:{ x; tmp } → 1:{ } 4:{ idata } → 5:{ }
[alias] analysing instruction: idata = tmp->t2[*(tmp->n2)];
[alias] May-aliases after instruction idata = tmp->t2[*(tmp->n2)]; are
- { x; tmp } { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; idata }
+ { x; tmp } { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; idata }
[alias] May-alias graph after instruction idata = tmp->t2[*(tmp->n2)]; is
0:{ x; tmp } → 1:{ } 1:{ } -t2→ 6:{ } 4:{ idata } → 5:{ }
6:{ } → 4:{ idata }
[alias] analysing instruction: odata = tmp->t1[*(tmp->n1)];
[alias] May-aliases after instruction odata = tmp->t1[*(tmp->n1)]; are
- { x; tmp } { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; idata }
- { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+ { x; tmp } { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; idata }
+ { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; odata }
[alias] May-alias graph after instruction odata = tmp->t1[*(tmp->n1)]; is
0:{ x; tmp } → 1:{ } 1:{ } -t2→ 6:{ } 1:{ } -t1→ 10:{ }
4:{ idata } → 5:{ } 6:{ } → 4:{ idata } 8:{ odata } → 9:{ }
10:{ } → 8:{ odata }
[alias] analysing instruction: idx = 0;
[alias] May-aliases after instruction idx = 0; are
- { x; tmp } { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; idata }
- { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+ { x; tmp } { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; idata }
+ { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; odata }
[alias] May-alias graph after instruction idx = 0; is
0:{ x; tmp } → 1:{ } 1:{ } -t2→ 6:{ } 1:{ } -t1→ 10:{ }
4:{ idata } → 5:{ } 6:{ } → 4:{ idata } 8:{ odata } → 9:{ }
@@ -37,24 +37,24 @@
[alias] analysing instruction: tmp_1 = sin(*(idata + idx));
[alias:undefined:fn] example1.c:45: Warning: function sin has no definition
[alias] May-aliases after instruction tmp_1 = sin(*(idata + idx)); are
- { x; tmp } { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; idata }
- { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+ { x; tmp } { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; idata }
+ { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; odata }
[alias] May-alias graph after instruction tmp_1 = sin(*(idata + idx)); is
0:{ x; tmp } → 1:{ } 1:{ } -t2→ 6:{ } 1:{ } -t1→ 10:{ }
4:{ idata } → 5:{ } 6:{ } → 4:{ idata } 8:{ odata } → 9:{ }
10:{ } → 8:{ odata }
[alias] analysing instruction: *(odata + idx) = 0.5 * tmp_1;
[alias] May-aliases after instruction *(odata + idx) = 0.5 * tmp_1; are
- { x; tmp } { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; idata }
- { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+ { x; tmp } { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; idata }
+ { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; odata }
[alias] May-alias graph after instruction *(odata + idx) = 0.5 * tmp_1; is
0:{ x; tmp } → 1:{ } 1:{ } -t2→ 6:{ } 1:{ } -t1→ 10:{ }
4:{ idata } → 5:{ } 6:{ } → 4:{ idata } 8:{ odata } → 9:{ }
10:{ } → 8:{ odata }
[alias] analysing instruction: idx ++;
[alias] May-aliases after instruction idx ++; are
- { x; tmp } { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; idata }
- { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+ { x; tmp } { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; idata }
+ { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; odata }
[alias] May-alias graph after instruction idx ++; is
0:{ x; tmp } → 1:{ } 1:{ } -t2→ 6:{ } 1:{ } -t1→ 10:{ }
4:{ idata } → 5:{ } 6:{ } → 4:{ idata } 8:{ odata } → 9:{ }
@@ -72,24 +72,24 @@
<empty>
[alias] Summary of function swap:
[alias] May-aliases after instruction swap(tmp->n1); are
- { x; tmp } { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; idata }
- { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+ { x; tmp } { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; idata }
+ { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; odata }
[alias] May-alias graph after instruction swap(tmp->n1); is
0:{ x; tmp } → 1:{ } 1:{ } -t2→ 6:{ } 1:{ } -t1→ 10:{ }
4:{ idata } → 5:{ } 6:{ } → 4:{ idata } 8:{ odata } → 9:{ }
10:{ } → 8:{ odata }
[alias] analysing instruction: idata = tmp->t2[*(tmp->n2)];
[alias] May-aliases after instruction idata = tmp->t2[*(tmp->n2)]; are
- { x; tmp } { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; idata }
- { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+ { x; tmp } { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; idata }
+ { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; odata }
[alias] May-alias graph after instruction idata = tmp->t2[*(tmp->n2)]; is
0:{ x; tmp } → 1:{ } 1:{ } -t2→ 6:{ } 1:{ } -t1→ 10:{ }
4:{ idata } → 5:{ } 6:{ } → 4:{ idata } 8:{ odata } → 9:{ }
10:{ } → 8:{ odata }
[alias] analysing instruction: odata = tmp->t1[*(tmp->n1)];
[alias] May-aliases after instruction odata = tmp->t1[*(tmp->n1)]; are
- { x; tmp } { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; idata }
- { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+ { x; tmp } { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; idata }
+ { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; odata }
[alias] May-alias graph after instruction odata = tmp->t1[*(tmp->n1)]; is
0:{ x; tmp } → 1:{ } 1:{ } -t2→ 6:{ } 1:{ } -t1→ 10:{ }
4:{ idata } → 5:{ } 6:{ } → 4:{ idata } 8:{ odata } → 9:{ }
@@ -117,22 +117,22 @@
14:{ x; tmp } → 15:{ } 18:{ idata } → 19:{ }
[alias] analysing instruction: idata = tmp->t1[*(tmp->n1)];
[alias] May-aliases after instruction idata = tmp->t1[*(tmp->n1)]; are
- { x; tmp } { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; idata }
+ { x; tmp } { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; idata }
[alias] May-alias graph after instruction idata = tmp->t1[*(tmp->n1)]; is
14:{ x; tmp } → 15:{ } 15:{ } -t1→ 20:{ }
18:{ idata } → 19:{ } 20:{ } → 18:{ idata }
[alias] analysing instruction: odata = tmp->t2[*(tmp->n2)];
[alias] May-aliases after instruction odata = tmp->t2[*(tmp->n2)]; are
- { x; tmp } { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; idata }
- { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+ { x; tmp } { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; idata }
+ { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; odata }
[alias] May-alias graph after instruction odata = tmp->t2[*(tmp->n2)]; is
14:{ x; tmp } → 15:{ } 15:{ } -t1→ 20:{ } 15:{ } -t2→ 24:{ }
18:{ idata } → 19:{ } 20:{ } → 18:{ idata }
22:{ odata } → 23:{ } 24:{ } → 22:{ odata }
[alias] analysing instruction: idx = 0;
[alias] May-aliases after instruction idx = 0; are
- { x; tmp } { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; idata }
- { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+ { x; tmp } { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; idata }
+ { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; odata }
[alias] May-alias graph after instruction idx = 0; is
14:{ x; tmp } → 15:{ } 15:{ } -t1→ 20:{ } 15:{ } -t2→ 24:{ }
18:{ idata } → 19:{ } 20:{ } → 18:{ idata }
@@ -141,8 +141,8 @@
*(odata + idx) = (double)3 * *(idata + idx) + (double)1;
[alias] May-aliases after instruction
*(odata + idx) = (double)3 * *(idata + idx) + (double)1; are
- { x; tmp } { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; idata }
- { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+ { x; tmp } { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; idata }
+ { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; odata }
[alias] May-alias graph after instruction
*(odata + idx) = (double)3 * *(idata + idx) + (double)1; is
14:{ x; tmp } → 15:{ } 15:{ } -t1→ 20:{ } 15:{ } -t2→ 24:{ }
@@ -150,32 +150,32 @@
22:{ odata } → 23:{ } 24:{ } → 22:{ odata }
[alias] analysing instruction: idx ++;
[alias] May-aliases after instruction idx ++; are
- { x; tmp } { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; idata }
- { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+ { x; tmp } { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; idata }
+ { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; odata }
[alias] May-alias graph after instruction idx ++; is
14:{ x; tmp } → 15:{ } 15:{ } -t1→ 20:{ } 15:{ } -t2→ 24:{ }
18:{ idata } → 19:{ } 20:{ } → 18:{ idata }
22:{ odata } → 23:{ } 24:{ } → 22:{ odata }
[alias] analysing instruction: swap(tmp->n2);
[alias] May-aliases after instruction swap(tmp->n2); are
- { x; tmp } { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; idata }
- { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+ { x; tmp } { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; idata }
+ { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; odata }
[alias] May-alias graph after instruction swap(tmp->n2); is
14:{ x; tmp } → 15:{ } 15:{ } -t1→ 20:{ } 15:{ } -t2→ 24:{ }
18:{ idata } → 19:{ } 20:{ } → 18:{ idata }
22:{ odata } → 23:{ } 24:{ } → 22:{ odata }
[alias] analysing instruction: idata = tmp->t1[*(tmp->n1)];
[alias] May-aliases after instruction idata = tmp->t1[*(tmp->n1)]; are
- { x; tmp } { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; idata }
- { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+ { x; tmp } { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; idata }
+ { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; odata }
[alias] May-alias graph after instruction idata = tmp->t1[*(tmp->n1)]; is
14:{ x; tmp } → 15:{ } 15:{ } -t1→ 20:{ } 15:{ } -t2→ 24:{ }
18:{ idata } → 19:{ } 20:{ } → 18:{ idata }
22:{ odata } → 23:{ } 24:{ } → 22:{ odata }
[alias] analysing instruction: odata = tmp->t2[*(tmp->n2)];
[alias] May-aliases after instruction odata = tmp->t2[*(tmp->n2)]; are
- { x; tmp } { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; idata }
- { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+ { x; tmp } { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; idata }
+ { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; odata }
[alias] May-alias graph after instruction odata = tmp->t2[*(tmp->n2)]; is
14:{ x; tmp } → 15:{ } 15:{ } -t1→ 20:{ } 15:{ } -t2→ 24:{ }
18:{ idata } → 19:{ } 20:{ } → 18:{ idata }
diff --git a/src/plugins/alias/tests/real_world/oracle/example2.res.oracle b/src/plugins/alias/tests/real_world/oracle/example2.res.oracle
index f1b9a01af08..768b61717d0 100644
--- a/src/plugins/alias/tests/real_world/oracle/example2.res.oracle
+++ b/src/plugins/alias/tests/real_world/oracle/example2.res.oracle
@@ -18,22 +18,22 @@
0:{ x; tmp } → 1:{ } 4:{ idata } → 5:{ }
[alias] analysing instruction: idata = tmp->t2[*(tmp->n2)];
[alias] May-aliases after instruction idata = tmp->t2[*(tmp->n2)]; are
- { x; tmp } { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; idata }
+ { x; tmp } { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; idata }
[alias] May-alias graph after instruction idata = tmp->t2[*(tmp->n2)]; is
0:{ x; tmp } → 1:{ } 1:{ } -t2→ 6:{ } 4:{ idata } → 5:{ }
6:{ } → 4:{ idata }
[alias] analysing instruction: odata = tmp->t1[*(tmp->n1)];
[alias] May-aliases after instruction odata = tmp->t1[*(tmp->n1)]; are
- { x; tmp } { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; idata }
- { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+ { x; tmp } { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; idata }
+ { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; odata }
[alias] May-alias graph after instruction odata = tmp->t1[*(tmp->n1)]; is
0:{ x; tmp } → 1:{ } 1:{ } -t2→ 6:{ } 1:{ } -t1→ 10:{ }
4:{ idata } → 5:{ } 6:{ } → 4:{ idata } 8:{ odata } → 9:{ }
10:{ } → 8:{ odata }
[alias] analysing instruction: idx = 0;
[alias] May-aliases after instruction idx = 0; are
- { x; tmp } { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; idata }
- { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+ { x; tmp } { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; idata }
+ { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; odata }
[alias] May-alias graph after instruction idx = 0; is
0:{ x; tmp } → 1:{ } 1:{ } -t2→ 6:{ } 1:{ } -t1→ 10:{ }
4:{ idata } → 5:{ } 6:{ } → 4:{ idata } 8:{ odata } → 9:{ }
@@ -41,24 +41,24 @@
[alias] analysing instruction: tmp_1 = sin(*(idata + idx));
[alias:undefined:fn] example2.c:45: Warning: function sin has no definition
[alias] May-aliases after instruction tmp_1 = sin(*(idata + idx)); are
- { x; tmp } { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; idata }
- { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+ { x; tmp } { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; idata }
+ { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; odata }
[alias] May-alias graph after instruction tmp_1 = sin(*(idata + idx)); is
0:{ x; tmp } → 1:{ } 1:{ } -t2→ 6:{ } 1:{ } -t1→ 10:{ }
4:{ idata } → 5:{ } 6:{ } → 4:{ idata } 8:{ odata } → 9:{ }
10:{ } → 8:{ odata }
[alias] analysing instruction: *(odata + idx) = 0.5 * tmp_1;
[alias] May-aliases after instruction *(odata + idx) = 0.5 * tmp_1; are
- { x; tmp } { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; idata }
- { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+ { x; tmp } { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; idata }
+ { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; odata }
[alias] May-alias graph after instruction *(odata + idx) = 0.5 * tmp_1; is
0:{ x; tmp } → 1:{ } 1:{ } -t2→ 6:{ } 1:{ } -t1→ 10:{ }
4:{ idata } → 5:{ } 6:{ } → 4:{ idata } 8:{ odata } → 9:{ }
10:{ } → 8:{ odata }
[alias] analysing instruction: idx ++;
[alias] May-aliases after instruction idx ++; are
- { x; tmp } { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; idata }
- { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+ { x; tmp } { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; idata }
+ { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; odata }
[alias] May-alias graph after instruction idx ++; is
0:{ x; tmp } → 1:{ } 1:{ } -t2→ 6:{ } 1:{ } -t1→ 10:{ }
4:{ idata } → 5:{ } 6:{ } → 4:{ idata } 8:{ odata } → 9:{ }
@@ -76,47 +76,47 @@
<empty>
[alias] Summary of function swap:
[alias] May-aliases after instruction swap(tmp->n1); are
- { x; tmp } { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; idata }
- { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+ { x; tmp } { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; idata }
+ { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; odata }
[alias] May-alias graph after instruction swap(tmp->n1); is
0:{ x; tmp } → 1:{ } 1:{ } -t2→ 6:{ } 1:{ } -t1→ 10:{ }
4:{ idata } → 5:{ } 6:{ } → 4:{ idata } 8:{ odata } → 9:{ }
10:{ } → 8:{ odata }
[alias] analysing instruction: i ++;
[alias] May-aliases after instruction i ++; are
- { x; tmp } { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; idata }
- { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+ { x; tmp } { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; idata }
+ { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; odata }
[alias] May-alias graph after instruction i ++; is
0:{ x; tmp } → 1:{ } 1:{ } -t2→ 6:{ } 1:{ } -t1→ 10:{ }
4:{ idata } → 5:{ } 6:{ } → 4:{ idata } 8:{ odata } → 9:{ }
10:{ } → 8:{ odata }
[alias] analysing instruction: idata = tmp->t2[*(tmp->n2)];
[alias] May-aliases after instruction idata = tmp->t2[*(tmp->n2)]; are
- { x; tmp } { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; idata }
- { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+ { x; tmp } { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; idata }
+ { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; odata }
[alias] May-alias graph after instruction idata = tmp->t2[*(tmp->n2)]; is
0:{ x; tmp } → 1:{ } 1:{ } -t2→ 6:{ } 1:{ } -t1→ 10:{ }
4:{ idata } → 5:{ } 6:{ } → 4:{ idata } 8:{ odata } → 9:{ }
10:{ } → 8:{ odata }
[alias] analysing instruction: odata = tmp->t1[*(tmp->n1)];
[alias] May-aliases after instruction odata = tmp->t1[*(tmp->n1)]; are
- { x; tmp } { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; idata }
- { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+ { x; tmp } { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; idata }
+ { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; odata }
[alias] May-alias graph after instruction odata = tmp->t1[*(tmp->n1)]; is
0:{ x; tmp } → 1:{ } 1:{ } -t2→ 6:{ } 1:{ } -t1→ 10:{ }
4:{ idata } → 5:{ } 6:{ } → 4:{ idata } 8:{ odata } → 9:{ }
10:{ } → 8:{ odata }
[alias] analysing instruction: __retres = (void *)0;
[alias] May-aliases after instruction __retres = (void *)0; are
- { x; tmp } { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; idata }
- { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+ { x; tmp } { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; idata }
+ { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; odata }
[alias] May-alias graph after instruction __retres = (void *)0; is
0:{ x; tmp } → 1:{ } 1:{ } -t2→ 6:{ } 1:{ } -t1→ 10:{ }
4:{ idata } → 5:{ } 6:{ } → 4:{ idata } 8:{ odata } → 9:{ }
10:{ } → 8:{ odata }
[alias] May-aliases at the end of function f1:
- { x; tmp } { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; idata }
- { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+ { x; tmp } { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; idata }
+ { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; odata }
[alias] May-alias graph at the end of function f1:
0:{ x; tmp } → 1:{ } 1:{ } -t2→ 6:{ } 1:{ } -t1→ 10:{ }
4:{ idata } → 5:{ } 6:{ } → 4:{ idata } 8:{ odata } → 9:{ }
@@ -124,9 +124,8 @@
[alias] Summary of function f1:
formals: x locals: tmp idata odata idx i tmp_1 __retres
returns: __retres
- state: { x; tmp } { x->t2; tmp->t2 }
- { (*x)[0..].t2; (*tmp)[0..].t2; idata } { x->t1; tmp->t1 }
- { (*x)[0..].t1; (*tmp)[0..].t1; odata }
+ state: { x; tmp } { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; idata }
+ { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; odata }
[alias] analysing function: f2
[alias] analysing instruction: ty *tmp = x;
[alias] May-aliases after instruction ty *tmp = x; are { x; tmp }
@@ -146,22 +145,22 @@
14:{ x; tmp } → 15:{ } 18:{ idata } → 19:{ }
[alias] analysing instruction: idata = tmp->t1[*(tmp->n1)];
[alias] May-aliases after instruction idata = tmp->t1[*(tmp->n1)]; are
- { x; tmp } { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; idata }
+ { x; tmp } { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; idata }
[alias] May-alias graph after instruction idata = tmp->t1[*(tmp->n1)]; is
14:{ x; tmp } → 15:{ } 15:{ } -t1→ 20:{ }
18:{ idata } → 19:{ } 20:{ } → 18:{ idata }
[alias] analysing instruction: odata = tmp->t2[*(tmp->n2)];
[alias] May-aliases after instruction odata = tmp->t2[*(tmp->n2)]; are
- { x; tmp } { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; idata }
- { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+ { x; tmp } { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; idata }
+ { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; odata }
[alias] May-alias graph after instruction odata = tmp->t2[*(tmp->n2)]; is
14:{ x; tmp } → 15:{ } 15:{ } -t1→ 20:{ } 15:{ } -t2→ 24:{ }
18:{ idata } → 19:{ } 20:{ } → 18:{ idata }
22:{ odata } → 23:{ } 24:{ } → 22:{ odata }
[alias] analysing instruction: idx = 0;
[alias] May-aliases after instruction idx = 0; are
- { x; tmp } { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; idata }
- { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+ { x; tmp } { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; idata }
+ { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; odata }
[alias] May-alias graph after instruction idx = 0; is
14:{ x; tmp } → 15:{ } 15:{ } -t1→ 20:{ } 15:{ } -t2→ 24:{ }
18:{ idata } → 19:{ } 20:{ } → 18:{ idata }
@@ -170,8 +169,8 @@
*(odata + idx) = (double)3 * *(idata + idx) + (double)1;
[alias] May-aliases after instruction
*(odata + idx) = (double)3 * *(idata + idx) + (double)1; are
- { x; tmp } { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; idata }
- { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+ { x; tmp } { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; idata }
+ { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; odata }
[alias] May-alias graph after instruction
*(odata + idx) = (double)3 * *(idata + idx) + (double)1; is
14:{ x; tmp } → 15:{ } 15:{ } -t1→ 20:{ } 15:{ } -t2→ 24:{ }
@@ -179,55 +178,55 @@
22:{ odata } → 23:{ } 24:{ } → 22:{ odata }
[alias] analysing instruction: idx ++;
[alias] May-aliases after instruction idx ++; are
- { x; tmp } { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; idata }
- { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+ { x; tmp } { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; idata }
+ { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; odata }
[alias] May-alias graph after instruction idx ++; is
14:{ x; tmp } → 15:{ } 15:{ } -t1→ 20:{ } 15:{ } -t2→ 24:{ }
18:{ idata } → 19:{ } 20:{ } → 18:{ idata }
22:{ odata } → 23:{ } 24:{ } → 22:{ odata }
[alias] analysing instruction: swap(tmp->n2);
[alias] May-aliases after instruction swap(tmp->n2); are
- { x; tmp } { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; idata }
- { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+ { x; tmp } { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; idata }
+ { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; odata }
[alias] May-alias graph after instruction swap(tmp->n2); is
14:{ x; tmp } → 15:{ } 15:{ } -t1→ 20:{ } 15:{ } -t2→ 24:{ }
18:{ idata } → 19:{ } 20:{ } → 18:{ idata }
22:{ odata } → 23:{ } 24:{ } → 22:{ odata }
[alias] analysing instruction: i ++;
[alias] May-aliases after instruction i ++; are
- { x; tmp } { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; idata }
- { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+ { x; tmp } { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; idata }
+ { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; odata }
[alias] May-alias graph after instruction i ++; is
14:{ x; tmp } → 15:{ } 15:{ } -t1→ 20:{ } 15:{ } -t2→ 24:{ }
18:{ idata } → 19:{ } 20:{ } → 18:{ idata }
22:{ odata } → 23:{ } 24:{ } → 22:{ odata }
[alias] analysing instruction: idata = tmp->t1[*(tmp->n1)];
[alias] May-aliases after instruction idata = tmp->t1[*(tmp->n1)]; are
- { x; tmp } { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; idata }
- { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+ { x; tmp } { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; idata }
+ { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; odata }
[alias] May-alias graph after instruction idata = tmp->t1[*(tmp->n1)]; is
14:{ x; tmp } → 15:{ } 15:{ } -t1→ 20:{ } 15:{ } -t2→ 24:{ }
18:{ idata } → 19:{ } 20:{ } → 18:{ idata }
22:{ odata } → 23:{ } 24:{ } → 22:{ odata }
[alias] analysing instruction: odata = tmp->t2[*(tmp->n2)];
[alias] May-aliases after instruction odata = tmp->t2[*(tmp->n2)]; are
- { x; tmp } { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; idata }
- { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+ { x; tmp } { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; idata }
+ { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; odata }
[alias] May-alias graph after instruction odata = tmp->t2[*(tmp->n2)]; is
14:{ x; tmp } → 15:{ } 15:{ } -t1→ 20:{ } 15:{ } -t2→ 24:{ }
18:{ idata } → 19:{ } 20:{ } → 18:{ idata }
22:{ odata } → 23:{ } 24:{ } → 22:{ odata }
[alias] analysing instruction: __retres = (void *)0;
[alias] May-aliases after instruction __retres = (void *)0; are
- { x; tmp } { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; idata }
- { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+ { x; tmp } { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; idata }
+ { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; odata }
[alias] May-alias graph after instruction __retres = (void *)0; is
14:{ x; tmp } → 15:{ } 15:{ } -t1→ 20:{ } 15:{ } -t2→ 24:{ }
18:{ idata } → 19:{ } 20:{ } → 18:{ idata }
22:{ odata } → 23:{ } 24:{ } → 22:{ odata }
[alias] May-aliases at the end of function f2:
- { x; tmp } { x->t1; tmp->t1 } { (*x)[0..].t1; (*tmp)[0..].t1; idata }
- { x->t2; tmp->t2 } { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+ { x; tmp } { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; idata }
+ { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; odata }
[alias] May-alias graph at the end of function f2:
14:{ x; tmp } → 15:{ } 15:{ } -t1→ 20:{ } 15:{ } -t2→ 24:{ }
18:{ idata } → 19:{ } 20:{ } → 18:{ idata }
@@ -235,9 +234,8 @@
[alias] Summary of function f2:
formals: x locals: tmp idx idata odata i __retres
returns: __retres
- state: { x; tmp } { x->t1; tmp->t1 }
- { (*x)[0..].t1; (*tmp)[0..].t1; idata } { x->t2; tmp->t2 }
- { (*x)[0..].t2; (*tmp)[0..].t2; odata }
+ state: { x; tmp } { x->t1; tmp->t1 } { x->t1[0..]; tmp->t1[0..]; idata }
+ { x->t2; tmp->t2 } { x->t2[0..]; tmp->t2[0..]; odata }
[alias] analysing function: main
[alias] analysing instruction: a = (ty *)malloc(sizeof(ty));
[alias] May-aliases after instruction a = (ty *)malloc(sizeof(ty)); are <none>
--
GitLab