Skip to content
Snippets Groups Projects
Commit 6be3084d authored by Patrick Baudin's avatar Patrick Baudin
Browse files

[wp] better fitting detection for C casts

parent 70819134
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/MemTyped.ml
+ 40
− 15
View file @ 6be3084d
......@@ -1062,14 +1062,15 @@ module Layout : sig
val fits: dst:c_object -> src:c_object -> bool
(* returns [true] in these cases:
- [dst] fits into [src]
- [dst] equals [src] *)
- [dst] fits into [src] (exists cobj; [src] = [dst] concat cobj)
- [dst] equals [src] ([dst] = [src]) *)
end =
struct
type atom = P of typ | I of c_int | F of c_float
type atom = P of typ | I of c_int | F of c_float | U of Cil_types.compinfo
let pp_atom fmt = function
| U ci -> Format.fprintf fmt "union %a" Printer.pp_compinfo ci
| P ty -> Printer.pp_typ fmt (TPtr(ty,[]))
| I i -> Ctypes.pp_int fmt i
| F f -> Ctypes.pp_float fmt f
......@@ -1077,7 +1078,10 @@ struct
let eqatom a1 a2 =
match a1 , a2 with
| P _ , P _ -> true
| _ -> (a1 = a2)
| U u1 , U u2 -> Compinfo.equal u1 u2
| I i1 , I i2 -> i1 = i2
| F f1 , F f2 -> f1 = f2
| _ -> false
type block =
| Str of atom * int
......@@ -1124,12 +1128,13 @@ struct
| C_int i -> add_atom (I i) w
| C_float f -> add_atom (F f) w
| C_pointer t -> add_atom (P t) w
| C_comp { cfields = [f] } ->
flayout w f (* unions containing only one field are
considered as structures *)
| C_comp c ->
if c.cstruct
then List.fold_left flayout w c.cfields
else
(* TODO: can be the longest common prefix *)
add_block Garbled w
else add_atom (U c) w (* unions with several fields *)
| C_array { arr_flat = Some a } ->
let ly = rlayout [] (Ctypes.object_of a.arr_cell) in
if a.arr_cell_nbr = 1
......@@ -1146,21 +1151,34 @@ struct
let layout (obj : c_object) : layout = List.rev (rlayout [] obj)
type comparison = Fit | Equal | Mismatch
let add_compound (c: Cil_types.compinfo) w : layout =
List.fold_left flayout w (List.rev c.cfields)
let ulayout (c: Cil_types.compinfo) : layout = add_compound c []
type comparison = Srem of layout | Drem of layout | Equal | Mismatch
let add_array ly n w =
if n=1 then ly @ w else add_many ly n w
let rec compare ~dst ~src =
let rec equal_atom a b =
(eqatom a b) ||
(match a,b with
| U u1, U u2 -> (* for union, the layouts must be equal *)
(match compare ~dst:(ulayout u1) ~src:(ulayout u2) with
| Equal -> true
| _ -> false)
| _, _ -> false)
and compare ~dst ~src =
match dst , src with
| [] , [] -> Equal (* src = dst *)
| [] , _ -> Fit (* exists obj ; src = dst concat obj *)
| _ , [] -> Mismatch
| [] , obj -> Srem obj (* src = dst @ obj *)
| obj , [] -> Drem obj (* dst = src @ obj *)
| p::w1 , q::w2 ->
match p , q with
| Garbled , _ | _ , Garbled -> Mismatch
| Str(a,n) , Str(b,m) ->
if eqatom a b then
if equal_atom a b then
if n < m then
let w2 = Str(a,m-n)::w2 in
compare w1 w2
......@@ -1175,7 +1193,14 @@ struct
begin
match compare ~dst:u ~src:v with
| Mismatch -> Mismatch
| Fit -> Mismatch
| Drem u' ->
let w1 = u' @ add_array u (n-1) w1 in
let w2 = add_array v (m-1) w2 in
compare w1 w2
| Srem v' ->
let w1 = add_array u (n-1) w1 in
let w2 = v' @ add_array v (m-1) w2 in
compare w1 w2
| Equal ->
if n < m then
let w2 = add_array v (m-n) w2 in
......@@ -1200,8 +1225,8 @@ struct
| C_pointer _ , C_pointer _ -> true
| _ ->
match compare ~dst:(layout dst) ~src:(layout src) with
| Equal | Fit -> true
| Mismatch -> false
| Equal | Srem _ -> true
| Drem _ | Mismatch -> false
let rec pretty fmt = function
| C_pointer ty -> Format.fprintf fmt "%a*" pretty (Ctypes.object_of ty)
......
src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle
+ 2
− 16
View file @ 6be3084d
......@@ -3,12 +3,6 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_typed/cast_fits.i:39: Warning:
Cast with incompatible pointers types (source: __anonstruct_L5_5*)
(target: __anonstruct_L6_6*)
[wp] tests/wp_typed/cast_fits.i:47: Warning:
Cast with incompatible pointers types (source: __anonunion_L7_7*)
(target: sint32*)
[wp] tests/wp_typed/cast_fits.i:13: Warning:
Cast with incompatible pointers types (source: __anonstruct_L2_2*)
(target: sint32*)
......@@ -70,11 +64,7 @@ Prove: x_1 = x.
------------------------------------------------------------
Goal Post-condition (file tests/wp_typed/cast_fits.i, line 37) in 'fits4':
tests/wp_typed/cast_fits.i:39: warning from Typed Model:
- Warning: Hide sub-term definition
Reason: Cast with incompatible pointers types (source: __anonstruct_L5_5*)
(target: __anonstruct_L6_6*)
Let x = Mchar_0[shiftfield_F6_c6(q)].
Let x = Mchar_0[shiftfield_F6_c6(p)].
Let x_1 = Mchar_0
[shiftfield_F3_c3(shift___anonstruct_L3_3(shiftfield_F5_ci5(p),
1))].
......@@ -91,11 +81,7 @@ Prove: x_1 = x.
------------------------------------------------------------
Goal Post-condition (file tests/wp_typed/cast_fits.i, line 45) in 'fits5':
tests/wp_typed/cast_fits.i:47: warning from Typed Model:
- Warning: Hide sub-term definition
Reason: Cast with incompatible pointers types (source: __anonunion_L7_7*)
(target: sint32*)
Let x = Mint_0[q].
Let x = Mint_0[p].
Let x_1 = Mint_0[shiftfield_F7_u7(p)].
Assume {
Type: is_sint32(x) /\ is_sint32(x_1).
......
src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle
+ 2
− 16
View file @ 6be3084d
......@@ -3,12 +3,6 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_typed/cast_fits.i:39: Warning:
Cast with incompatible pointers types (source: __anonstruct_L5_5*)
(target: __anonstruct_L6_6*)
[wp] tests/wp_typed/cast_fits.i:47: Warning:
Cast with incompatible pointers types (source: __anonunion_L7_7*)
(target: sint32*)
[wp] tests/wp_typed/cast_fits.i:13: Warning:
Cast with incompatible pointers types (source: __anonstruct_L2_2*)
(target: sint32*)
......@@ -70,11 +64,7 @@ Prove: x_1 = x.
------------------------------------------------------------
Goal Post-condition (file tests/wp_typed/cast_fits.i, line 37) in 'fits4':
tests/wp_typed/cast_fits.i:39: warning from Typed Model:
- Warning: Hide sub-term definition
Reason: Cast with incompatible pointers types (source: __anonstruct_L5_5*)
(target: __anonstruct_L6_6*)
Let x = Mchar_0[shiftfield_F6_c6(q)].
Let x = Mchar_0[shiftfield_F6_c6(p)].
Let x_1 = Mchar_0
[shiftfield_F3_c3(shift___anonstruct_L3_3(shiftfield_F5_ci5(p),
1))].
......@@ -91,11 +81,7 @@ Prove: x_1 = x.
------------------------------------------------------------
Goal Post-condition (file tests/wp_typed/cast_fits.i, line 45) in 'fits5':
tests/wp_typed/cast_fits.i:47: warning from Typed Model:
- Warning: Hide sub-term definition
Reason: Cast with incompatible pointers types (source: __anonunion_L7_7*)
(target: sint32*)
Let x = Mint_0[q].
Let x = Mint_0[p].
Let x_1 = Mint_0[shiftfield_F7_u7(p)].
Assume {
Type: is_sint32(x) /\ is_sint32(x_1).
......
src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.0.report.json
+ 20
− 12
View file @ 6be3084d
{ "wp:global": { "alt-ergo": { "total": 8, "valid": 3, "unknown": 5,
"rank": 7 },
"wp:main": { "total": 8, "valid": 3, "unknown": 5,
"rank": 7 } },
{ "wp:global": { "alt-ergo": { "total": 8, "valid": 5, "unknown": 3,
"rank": 8 },
"wp:main": { "total": 8, "valid": 5, "unknown": 3,
"rank": 8 } },
"wp:functions": { "fits1": { "fits1_ensures": { "alt-ergo": { "total": 1,
"valid": 1,
"rank": 6 },
......@@ -49,21 +49,29 @@
"valid": 1,
"rank": 7 } } },
"fits4": { "fits4_ensures": { "alt-ergo": { "total": 1,
"unknown": 1 },
"valid": 1,
"rank": 8 },
"wp:main": { "total": 1,
"unknown": 1 } },
"valid": 1,
"rank": 8 } },
"wp:section": { "alt-ergo": { "total": 1,
"unknown": 1 },
"valid": 1,
"rank": 8 },
"wp:main": { "total": 1,
"unknown": 1 } } },
"valid": 1,
"rank": 8 } } },
"fits5": { "fits5_ensures": { "alt-ergo": { "total": 1,
"unknown": 1 },
"valid": 1,
"rank": 6 },
"wp:main": { "total": 1,
"unknown": 1 } },
"valid": 1,
"rank": 6 } },
"wp:section": { "alt-ergo": { "total": 1,
"unknown": 1 },
"valid": 1,
"rank": 6 },
"wp:main": { "total": 1,
"unknown": 1 } } },
"valid": 1,
"rank": 6 } } },
"mismatch2": { "mismatch2_ensures": { "alt-ergo":
{ "total": 1,
"unknown": 1 },
......
src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.res.oracle
+ 6
− 12
View file @ 6be3084d
......@@ -3,12 +3,6 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] tests/wp_typed/cast_fits.i:39: Warning:
Cast with incompatible pointers types (source: __anonstruct_L5_5*)
(target: __anonstruct_L6_6*)
[wp] tests/wp_typed/cast_fits.i:47: Warning:
Cast with incompatible pointers types (source: __anonunion_L7_7*)
(target: sint32*)
[wp] tests/wp_typed/cast_fits.i:13: Warning:
Cast with incompatible pointers types (source: __anonstruct_L2_2*)
(target: sint32*)
......@@ -22,14 +16,14 @@
[wp] [Alt-Ergo] Goal typed_fits1_ensures : Valid
[wp] [Alt-Ergo] Goal typed_fits2_ensures : Valid
[wp] [Alt-Ergo] Goal typed_fits3_ensures : Valid
[wp] [Alt-Ergo] Goal typed_fits4_ensures : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_fits5_ensures : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_fits4_ensures : Valid
[wp] [Alt-Ergo] Goal typed_fits5_ensures : Valid
[wp] [Alt-Ergo] Goal typed_mismatch1_ensures : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_mismatch2_ensures : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_mismatch3_ensures : Unsuccess (Stronger)
[wp] Proved goals: 3 / 8
[wp] Proved goals: 5 / 8
Qed: 0
Alt-Ergo: 3 (unsuccess: 5)
Alt-Ergo: 5 (unsuccess: 3)
[wp] Report in: 'tests/wp_typed/oracle_qualif/cast_fits.0.report.json'
[wp] Report out: 'tests/wp_typed/result_qualif/cast_fits.0.report.json'
-------------------------------------------------------------
......@@ -38,8 +32,8 @@ fits1 - 1 (20..32) 1 100%
mismatch1 - - 1 0.0%
fits2 - 1 (20..32) 1 100%
fits3 - 1 (24..36) 1 100%
fits4 - - 1 0.0%
fits5 - - 1 0.0%
fits4 - 1 (28..40) 1 100%
fits5 - 1 (20..32) 1 100%
mismatch2 - - 1 0.0%
mismatch3 - - 1 0.0%
-------------------------------------------------------------
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment