diff --git a/Changelog b/Changelog
index d922b63db20b3d4d1f01d2274345b390f5f64e76..b40c2f25437adc84c5f5c151b1f37c265c36e6bb 100644
--- a/Changelog
+++ b/Changelog
@@ -18,6 +18,7 @@
Open Source Release <next-release>
###############################################################################
+- Alias [2024-08-22] no longer classify virtually all casts as unsafe
o! Kernel [2024-08-08] New Machine module to manage theMachine and machdeps.
Cil functions related to theMachine are deprecated.
-! Kernel [2024-08-08] New minimal OCaml version: 4.14
diff --git a/src/plugins/alias/src/simplified.ml b/src/plugins/alias/src/simplified.ml
index 485f732d48b55eb7f4df3beb67d9a46870c74e3c..8cd1e463ef9c1fd4212036b47845e6ee699cb2aa 100644
--- a/src/plugins/alias/src/simplified.ml
+++ b/src/plugins/alias/src/simplified.ml
@@ -38,16 +38,25 @@ let clear_cache () =
exception Explicit_pointer_address of location
-let check_cast_compatibility e typ =
- let type_of_e = Cil.typeOf e in
- (* emit a warning for unsafe casts, but not for the NULL pointer *)
- if Cil.need_cast typ type_of_e && not (Cil.isZero e) then
+let check_cast_compatibility e to_type =
+ let rec cast_preserves_indirection_level from_type to_type =
+ let recurse = cast_preserves_indirection_level in
+ match Cil.unrollType from_type, Cil.unrollType to_type with
+ | TPtr (from_type, _), TPtr (to_type, _) -> recurse from_type to_type
+ | TPtr _, _ -> false
+ | _, TPtr _ -> false
+ | _ -> true
+ in
+ let from_type = Cil.typeOf e in
+ if Cil.need_cast to_type from_type && not (Cil.isZero e)
+ && not (cast_preserves_indirection_level from_type to_type) then
+ (* emit a warning for unsafe casts, but not for the NULL pointer *)
Options.warning
~once:true
~source:(fst @@ e.eloc)
~wkey:Options.Warn.unsafe_cast
"unsafe cast from %a to %a; analysis may be unsound"
- Printer.pp_typ type_of_e Printer.pp_typ typ
+ Printer.pp_typ from_type Printer.pp_typ to_type
let rec simplify_offset o =
match o with
diff --git a/src/plugins/alias/tests/basic/oracle/cast1.res.oracle b/src/plugins/alias/tests/basic/oracle/cast1.res.oracle
index 176c4f381f9259dffabbb0b7f4de5fa873fbf492..d7b0ae75d4e62417b64597a43515ff02672ca6c2 100644
--- a/src/plugins/alias/tests/basic/oracle/cast1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/cast1.res.oracle
@@ -13,13 +13,9 @@
[alias] May-aliases after instruction float *d = (float *)0; are <none>
[alias] May-alias graph after instruction float *d = (float *)0; is <empty>
[alias] analysing instruction: a = (int *)c;
-[alias:unsafe-cast] cast1.c:10: Warning:
- unsafe cast from float * to int *; analysis may be unsound
[alias] May-aliases after instruction a = (int *)c; are { a; c }
[alias] May-alias graph after instruction a = (int *)c; is 0:{ a; c } → 1:{ }
[alias] analysing instruction: d = (float *)b;
-[alias:unsafe-cast] cast1.c:11: Warning:
- unsafe cast from int * to float *; analysis may be unsound
[alias] May-aliases after instruction d = (float *)b; are { a; c } { b; d }
[alias] May-alias graph after instruction d = (float *)b; is
0:{ a; c } → 1:{ } 4:{ b; d } → 5:{ }
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 32f600115b8584bdd15261cae93e8887982b4f0f..26a1a05e81152b01f02fe55ab5fcaf87f01bf0fc 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/origin.res.oracle
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/origin.res.oracle
@@ -8,8 +8,6 @@
[alias] analysing instruction: tmp = (void (*)(void))*((char *)(v.t));
[alias:unsafe-cast] origin.c:8: Warning:
unsafe cast from char to void (*)(void); analysis may be unsound
-[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.t[0..]; tmp }
[alias] May-alias graph after instruction tmp = (void (*)(void))*((char *)(v.t));
diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/origin_simpl.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/origin_simpl.res.oracle
index c2c8ab976e07eaa3512215cc56e5a9eeba759cae..5f05212a15c9aa4d83a85a16c83d24480a858cb1 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/origin_simpl.res.oracle
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/origin_simpl.res.oracle
@@ -3,8 +3,6 @@
[alias] analysing instruction: tmp = (void *)*((int *)(t));
[alias:unsafe-cast] origin_simpl.c:9: Warning:
unsafe cast from int to void *; analysis may be unsound
-[alias:unsafe-cast] origin_simpl.c:9: Warning:
- unsafe cast from char * to int *; analysis may be unsound
[alias] May-aliases after instruction tmp = (void *)*((int *)(t)); are
{ t[0..]; tmp }
[alias] May-alias graph after instruction tmp = (void *)*((int *)(t)); is
diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/reduce_by_valid.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/reduce_by_valid.res.oracle
index df25a14949b787d251929bde47d8b0b3e01912f3..048ac1e66ae4998c3509c4e0aa14d04a0d0cf53f 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/reduce_by_valid.res.oracle
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/reduce_by_valid.res.oracle
@@ -5,14 +5,10 @@
casting function to int *
[alias] analysing function: f
[alias] analysing instruction: int *q = (int *)(& f);
-[alias:unsafe-cast] reduce_by_valid.c:5: Warning:
- unsafe cast from void (*)(void) to int *; analysis may be unsound
[alias] May-aliases after instruction int *q = (int *)(& f); are <none>
[alias] May-alias graph after instruction int *q = (int *)(& f); is
0:{ q } → 1:{ f }
[alias] analysing instruction: int *p = (int *)(& f);
-[alias:unsafe-cast] reduce_by_valid.c:5: Warning:
- unsafe cast from void (*)(void) to int *; analysis may be unsound
[alias] May-aliases after instruction int *p = (int *)(& f); are { q; p }
[alias] May-alias graph after instruction int *p = (int *)(& f); is
0:{ q } → 5:{ f } 4:{ p } → 5:{ f }
diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/union_vmap.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/union_vmap.res.oracle
index ad021ebd893df1e93035660331c2ecabcfbdd3d9..8b91112f928bf36edabd178a666c41e4b27fa4cd 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/union_vmap.res.oracle
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/union_vmap.res.oracle
@@ -7,15 +7,11 @@
<empty>
[alias] Summary of function CPS_SplitWord:
formals: line returns: line state: <none>
-[alias:unsafe-cast] union_vmap.c:11: Warning:
- unsafe cast from char const * to char *; analysis may be unsound
[alias] May-aliases after instruction char *s2 = CPS_SplitWord((char *)"a"); are
<none>
[alias] May-alias graph after instruction char *s2 = CPS_SplitWord((char *)"a");
is 4:{ s2 } → 3:{ }
[alias] analysing instruction: char *s3 = CPS_SplitWord((char *)"b");
-[alias:unsafe-cast] union_vmap.c:12: Warning:
- unsafe cast from char const * to char *; analysis may be unsound
[alias] May-aliases after instruction char *s3 = CPS_SplitWord((char *)"b"); are
<none>
[alias] May-alias graph after instruction char *s3 = CPS_SplitWord((char *)"b");
diff --git a/src/plugins/alias/tests/offsets/oracle/nested1.res.oracle b/src/plugins/alias/tests/offsets/oracle/nested1.res.oracle
index f9bd813190c345c46dd5df0a24f27e1ae9707ec1..2affa633b02404a8cd5408b036c878b46d3dbb70 100644
--- a/src/plugins/alias/tests/offsets/oracle/nested1.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/nested1.res.oracle
@@ -58,8 +58,6 @@
9:{ z2 } → 10:{ } 11:{ t } → 12:{ } 13:{ a } → 14:{ }
15:{ b } → 16:{ }
[alias] analysing instruction: z1->s = (struct struct_1_t *)tab_y[0];
-[alias:unsafe-cast] nested1.c:47: Warning:
- unsafe cast from st_1_t * to struct struct_1_t *; analysis may be unsound
[alias] May-aliases after instruction z1->s = (struct struct_1_t *)tab_y[0]; are
{ z1->s; tab_y[0..] }
[alias] May-alias graph after instruction z1->s = (struct struct_1_t *)tab_y[0];
@@ -68,8 +66,6 @@
9:{ z2 } → 10:{ } 11:{ t } → 12:{ } 13:{ a } → 14:{ }
15:{ b } → 16:{ } 17:{ } → 2:{ x1; x2 }
[alias] analysing instruction: z2->s = (struct struct_1_t *)tab_y[1];
-[alias:unsafe-cast] nested1.c:48: Warning:
- unsafe cast from st_1_t * to struct struct_1_t *; analysis may be unsound
[alias] May-aliases after instruction z2->s = (struct struct_1_t *)tab_y[1]; are
{ z1->s; z2->s; tab_y[0..] }
[alias] May-alias graph after instruction z2->s = (struct struct_1_t *)tab_y[1];
@@ -94,8 +90,6 @@
10:{ } -c→ 20:{ b } 11:{ t } → 12:{ } 18:{ } → 2:{ x1; x2 }
19:{ a } → 14:{ } 20:{ b } → 16:{ }
[alias] analysing instruction: t->t = (struct struct_2_t *)z1;
-[alias:unsafe-cast] nested1.c:51: Warning:
- 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)->s; z1->s; z2->s; tab_y[0..] } { t->t; z1 }
{ (t->t)->c; z1->c; a } { z2->c; b }
diff --git a/src/plugins/alias/tests/offsets/oracle/nested2.res.oracle b/src/plugins/alias/tests/offsets/oracle/nested2.res.oracle
index 85015cf9c50e50606ab4352c4a8c0b61ea586f17..c8228e82bb78b6e4676ca12d9336313bb122f853 100644
--- a/src/plugins/alias/tests/offsets/oracle/nested2.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/nested2.res.oracle
@@ -27,8 +27,6 @@
[alias] May-alias graph after instruction *a = 0; is
0:{ z1 } → 1:{ } 2:{ t } → 3:{ } 4:{ a } → 5:{ }
[alias] analysing instruction: z1->s[0] = (struct struct_1_t *)(& x1);
-[alias:unsafe-cast] nested2.c:42: Warning:
- unsafe cast from st_1_t * to struct struct_1_t *; analysis may be unsound
[alias] May-aliases after instruction z1->s[0] = (struct struct_1_t *)(& x1); are
<none>
[alias] May-alias graph after instruction z1->s[0] = (struct struct_1_t *)(& x1);
@@ -36,8 +34,6 @@
0:{ z1 } → 1:{ } 1:{ } -s→ 6:{ } 2:{ t } → 3:{ }
4:{ a } → 5:{ } 6:{ } → 7:{ } 7:{ } → 8:{ x1 }
[alias] analysing instruction: z1->s[1] = (struct struct_1_t *)(& x2);
-[alias:unsafe-cast] nested2.c:43: Warning:
- unsafe cast from st_1_t * to struct struct_1_t *; analysis may be unsound
[alias] May-aliases after instruction z1->s[1] = (struct struct_1_t *)(& x2); are
<none>
[alias] May-alias graph after instruction z1->s[1] = (struct struct_1_t *)(& x2);
@@ -51,8 +47,6 @@
2:{ t } → 3:{ } 6:{ } → 7:{ } 7:{ } → 8:{ x1; x2 }
12:{ a } → 5:{ }
[alias] analysing instruction: t->t = (struct struct_2_t *)z1;
-[alias:unsafe-cast] nested2.c:45: Warning:
- 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)->s[0..]; z1->s[0..] }
diff --git a/src/plugins/alias/tests/offsets/oracle/structure1.res.oracle b/src/plugins/alias/tests/offsets/oracle/structure1.res.oracle
index e637a626f9b16410fe49a58e18203b19e122598e..44ebcfc96e36af55f2a3cb05fb6d0c224756808d 100644
--- a/src/plugins/alias/tests/offsets/oracle/structure1.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/structure1.res.oracle
@@ -21,8 +21,6 @@
[alias] May-alias graph after instruction p_x->a = 3; is
0:{ p_x } → 1:{ x } 4:{ p_y } → 5:{ y }
[alias] analysing instruction: p_x = (st_1_t *)p_y;
-[alias:unsafe-cast] structure1.c:28: Warning:
- unsafe cast from st_2_t * to st_1_t *; analysis may be unsound
[alias] May-aliases after instruction p_x = (st_1_t *)p_y; are { p_x; p_y }
[alias] May-alias graph after instruction p_x = (st_1_t *)p_y; is
0:{ p_x; p_y } → 1:{ x; y }
diff --git a/src/plugins/alias/tests/offsets/oracle/structure2.res.oracle b/src/plugins/alias/tests/offsets/oracle/structure2.res.oracle
index b278d558f710585ab6b6063d25fe40f7be6335b2..6a8741ba3fce4a3eced1e9352c1cede595ec1918 100644
--- a/src/plugins/alias/tests/offsets/oracle/structure2.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/structure2.res.oracle
@@ -9,16 +9,12 @@
[alias] May-alias graph after instruction st_1_t x2 = {.a = 1, .b = 2}; is
<empty>
[alias] analysing instruction: st_2_t y = {.s = (struct struct_1_t *)(& x1), .c = 4};
-[alias:unsafe-cast] structure2.c:21: Warning:
- unsafe cast from st_1_t * to struct struct_1_t *; analysis may be unsound
[alias] May-aliases after instruction
st_2_t y = {.s = (struct struct_1_t *)(& x1), .c = 4}; are <none>
[alias] May-alias graph after instruction
st_2_t y = {.s = (struct struct_1_t *)(& x1), .c = 4}; is
0:{ y } -s→ 1:{ } 1:{ } → 2:{ x1 }
[alias] analysing instruction: y.s = (struct struct_1_t *)(& x2);
-[alias:unsafe-cast] structure2.c:23: Warning:
- unsafe cast from st_1_t * to struct struct_1_t *; analysis may be unsound
[alias] May-aliases after instruction y.s = (struct struct_1_t *)(& x2); are
<none>
[alias] May-alias graph after instruction y.s = (struct struct_1_t *)(& x2); is
diff --git a/src/plugins/alias/tests/offsets/oracle/structure4.res.oracle b/src/plugins/alias/tests/offsets/oracle/structure4.res.oracle
index 6a11ec706edc4f080c198122381ea9542094cf2e..5202212a7ef9f6fbe6eabf5f896035c85a7d45eb 100644
--- a/src/plugins/alias/tests/offsets/oracle/structure4.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/structure4.res.oracle
@@ -23,8 +23,6 @@
[alias] May-alias graph after instruction y1 = & x1; is
0:{ y1 } → 1:{ x1 } 2:{ z } → 3:{ }
[alias] analysing instruction: z->s = (struct struct_1_t *)y1;
-[alias:unsafe-cast] structure4.c:37: Warning:
- unsafe cast from st_1_t * to struct struct_1_t *; analysis may be unsound
[alias] May-aliases after instruction z->s = (struct struct_1_t *)y1; are
{ z->s; y1 }
[alias] May-alias graph after instruction z->s = (struct struct_1_t *)y1; is
diff --git a/src/plugins/alias/tests/offsets/oracle/structure5.res.oracle b/src/plugins/alias/tests/offsets/oracle/structure5.res.oracle
index efd088f070c7ee0d048c76e31d7ffa1e665d8c84..971bf53b27bdb82c90533b39d350d004e10ebf78 100644
--- a/src/plugins/alias/tests/offsets/oracle/structure5.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/structure5.res.oracle
@@ -39,8 +39,6 @@
0:{ y1 } → 1:{ x1 } 2:{ z } → 3:{ } 4:{ t } → 5:{ }
6:{ a } → 7:{ }
[alias] analysing instruction: z->s = (struct struct_1_t *)y1;
-[alias:unsafe-cast] structure5.c:41: Warning:
- unsafe cast from st_1_t * to struct struct_1_t *; analysis may be unsound
[alias] May-aliases after instruction z->s = (struct struct_1_t *)y1; are
{ z->s; y1 }
[alias] May-alias graph after instruction z->s = (struct struct_1_t *)y1; is
@@ -52,8 +50,6 @@
2:{ z } → 3:{ } 3:{ } -s→ 10:{ y1 } 3:{ } -c→ 11:{ a }
4:{ t } → 5:{ } 10:{ y1 } → 1:{ x1 } 11:{ a } → 7:{ }
[alias] analysing instruction: t->t = (struct struct_2_t *)z;
-[alias:unsafe-cast] structure5.c:43: Warning:
- 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 *)z; are
{ (t->t)->s; z->s; y1 } { t->t; z } { (t->t)->c; z->c; a }
[alias] May-alias graph after instruction t->t = (struct struct_2_t *)z; is