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

Merge branch 'feature/patrick/lazy-fitting-layout-for-wp-cast' into 'master' 

[WP] better fitting detection for C cast - with an algo more lazy

See merge request frama-c/frama-c!2204
parents 9273a873 da04f80a
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
+ 137
− 86
View file @ 75f2a486
......@@ -503,6 +503,7 @@ let rec size_of_object = function
and size_of_typ t = size_of_object (object_of t)
and size_of_field f = size_of_typ f.ftype
and size_of_comp c =
(* union field are considered as struct field *)
List.fold_left
(fun s f -> s + size_of_field f)
0 c.cfields
......@@ -1067,36 +1068,74 @@ module Layout : sig
end =
struct
type atom = P of typ | I of c_int | F of c_float | U of Cil_types.compinfo
type atom = P of typ | I of c_int | F of c_float
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
let eqatom a1 a2 =
let eq_atom a1 a2 =
match a1 , a2 with
| P _ , P _ -> true
| U u1 , U u2 -> Compinfo.equal u1 u2
| I i1 , I i2 -> i1 = i2
| F f1 , F f2 -> f1 = f2
| _ -> false
type slot = A of atom
| S of Cil_types.compinfo (* delayed layout of a C struct *)
| U of Cil_types.compinfo (* delayed layout of a C union *)
let pp_slot fmt = function
| A a -> pp_atom fmt a
| S s -> Format.fprintf fmt "{struct %a}" Printer.pp_compinfo s
| U u -> Format.fprintf fmt "{union %a}" Printer.pp_compinfo u
let eq_slot a1 a2 = (* syntactic equality *)
match a1 , a2 with
| A a1 , A a2 -> eq_atom a1 a2
| S c1 , S c2 | U c1, U c2 -> Compinfo.equal c1 c2
| _ -> false
let rec get_slot = function
| C_int i -> A (I i)
| C_float f -> A (F f)
| C_pointer t -> A (P t)
| C_comp ( { cfields = [f] } as c ) ->
begin (* union having only one field is equivalent to a struct *)
match Ctypes.object_of f.ftype with
| C_array _ -> (if c.cstruct then S c else U c)
| cobj -> get_slot cobj
end
| C_comp c -> if c.cstruct then S c else U c
| C_array _ -> assert false
type block =
| Str of atom * int
| Arr of layout * int (* non-homogeneous, more than one *)
| Str of slot * int
| Arr of c_object * int (* delayed layout of a C type *)
| Garbled
and layout = block list
let rec pp_block fmt = function
| Str(a,n) when n=1 -> pp_atom fmt a
| Str(a,n) -> Format.fprintf fmt "%a[%d]" pp_atom a n
| Arr(ly,n) -> Format.fprintf fmt "%a[%d]" pp_layout ly n
let pp_block fmt = function
| Str(a,n) when n=1 -> pp_slot fmt a
| Str(a,n) -> Format.fprintf fmt "%a[%d]" pp_slot a n
| Arr(o,n) -> Format.fprintf fmt "{ctype %a}[%d]" Ctypes.pretty o n
| Garbled -> Format.fprintf fmt "..."
and pp_layout fmt = function
let add_slot a n w =
assert (n >= 1) ;
match w with
| Str(b,m) :: w when eq_slot a b -> Str(b,m+n)::w
| _ -> Str(a,n) :: w
let add_block p w =
match p , w with
| Str(a,n) , Str(b,m)::w when eq_slot a b -> Str(b,n+m)::w
| Garbled , Garbled::_ -> w
| _ -> p :: w
type layout = block list
let pp_layout fmt = function
| [b] -> pp_block fmt b
| bs ->
begin
......@@ -1105,100 +1144,100 @@ struct
Format.fprintf fmt " }@]" ;
end
let add_atom a ly =
match ly with
| Str(b,m) :: w when eqatom a b -> Str(b,m+1)::w
| _ -> Str(a,1) :: ly
let add_block p ly =
match p , ly with
| Str(a,n) , Str(b,m)::w when eqatom a b -> Str(b,n+m)::w
| Garbled , Garbled::_ -> ly
| _ -> p :: ly
(* requires n > 1 *)
let add_many ly n w =
match ly with
| [] -> w
| [Str(a,m)] -> add_block (Str(a,n*m)) w
| Garbled::_ -> add_block Garbled w
| ly -> Arr(ly,n) :: w
let rec rlayout w = function
| 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 add_atom (U c) w (* unions with several fields *)
let rec add_many cobj n w = (* returns [layout obj]*n @ [w] *)
assert (n > 1) ;
match cobj, w with
| C_array { arr_flat = Some a }, _ when a.arr_cell_nbr = 1 ->
add_many (Ctypes.object_of a.arr_cell) n w
| C_array _, Arr(o, m)::w when 0 = compare_ptr_conflated o cobj -> Arr(o, m+n)::w
| C_array _, _ -> Arr(cobj, n)::w
| _ -> add_slot (get_slot cobj) n w
let rec rlayout w = function (* returns [layout obj] @ [w] *)
| C_array { arr_flat = Some a } ->
let ly = rlayout [] (Ctypes.object_of a.arr_cell) in
let cobj = Ctypes.object_of a.arr_cell in
if a.arr_cell_nbr = 1
then ly @ w (* ly is in reversed order *)
else add_many (List.rev ly) a.arr_cell_nbr w
then rlayout w cobj
else add_many cobj a.arr_cell_nbr w
| C_array { arr_element = e } ->
if Wp_parameters.ExternArrays.get () then
let ly = rlayout [] (Ctypes.object_of e) in
add_many (List.rev ly) max_int w
add_many (Ctypes.object_of e) max_int w
else
add_block Garbled w
| cobj -> add_slot (get_slot cobj) 1 w
and flayout w f = rlayout w (Ctypes.object_of f.ftype)
let layout (obj : c_object) : layout = rlayout [] obj
let layout (obj : c_object) : layout = List.rev (rlayout [] obj)
let clayout (c: Cil_types.compinfo) : layout =
let flayout w f = rlayout w (Ctypes.object_of f.ftype) in
List.fold_left flayout [] (List.rev c.cfields)
let add_compound (c: Cil_types.compinfo) w : layout =
List.fold_left flayout w (List.rev c.cfields)
type comparison = Srem of layout | Drem of layout | Equal | Mismatch
let ulayout (c: Cil_types.compinfo) : layout = add_compound c []
let add_array o n w =
assert (n > 0) ;
if n=1 then rlayout w o else Arr(o, n)::w
type comparison = Srem of layout | Drem of layout | Equal | Mismatch
let decr_slot a n w =
assert (n >= 1);
if n=1 then w else Str(a, n-1)::w
let add_array ly n w =
if n=1 then ly @ w else add_many ly n w
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)
let rec equal u v =
match compare ~dst:u ~src:v with
| Equal -> true
| _ -> false
and compare_slot ~dst ~src =
match dst, src with
| A a1, A a2 -> if eq_atom a1 a2 then Equal else Mismatch
| S c1, S c2 | U c1, U c2 when Compinfo.equal c1 c2 -> Equal
| S c1, _ -> compare ~dst:(clayout c1) ~src:[Str(src,1)]
| _, S c2 -> compare ~dst:[Str(dst,1)] ~src:(clayout c2)
| U c1, U c2 -> (* for union, the layouts must be equal *)
if equal (clayout c1) (clayout c2) then Equal else Mismatch
| U _, A _ -> Mismatch
| A _, U _ -> Mismatch
and compare ~dst ~src =
match dst , src with
| [] , [] -> Equal (* src = dst *)
| [] , obj -> Srem obj (* src = dst @ obj *)
| obj , [] -> Drem obj (* dst = src @ obj *)
| [] , [] -> Equal (* src = dst *)
| [] , 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 equal_atom a b then
if n < m then
let w2 = Str(a,m-n)::w2 in
compare w1 w2
else if n > m then
let w1 = Str(a,n-m)::w1 in
compare w1 w2
else
(* n = m *)
compare w1 w2
else Mismatch
begin
match compare_slot a b with
| Mismatch -> Mismatch
| Drem a'->
let w1 = a' @ decr_slot a n w1 in
let w2 = decr_slot b m w2 in
compare w1 w2
| Srem b' ->
let w1 = decr_slot a n w1 in
let w2 = b' @ decr_slot b m w2 in
compare w1 w2
| Equal ->
if n < m then
let w2 = Str(a,m-n)::w2 in
compare w1 w2
else if n > m then
let w1 = Str(a,n-m)::w1 in
compare w1 w2
else
(* n = m *)
compare w1 w2
end
| Arr(u,n) , Arr(v,m) ->
begin
match compare ~dst:u ~src:v with
match compare ~dst:(layout u) ~src:(layout v) with
| Mismatch -> Mismatch
| Drem u' ->
let w1 = u' @ add_array u (n-1) w1 in
let w2 = add_array v (m-1) w2 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 w1 = add_array u (n-1) w1 in
let w2 = v' @ add_array v (m-1) w2 in
compare w1 w2
| Equal ->
......@@ -1212,10 +1251,10 @@ struct
(* n = m *)
compare w1 w2
end
| Arr(v,n) , Str _ ->
compare ~dst:(v @ add_array v (n-1) w1) ~src
| Arr(u,n) , Str _ ->
compare ~dst:((layout u) @ add_array u (n-1) w1) ~src
| Str _ , Arr(v,n) ->
compare ~dst ~src:(v @ add_array v (n-1) w2)
compare ~dst ~src:((layout v) @ add_array v (n-1) w2)
let rec repeated ~dst ~src =
match dst , src with
......@@ -1226,10 +1265,22 @@ struct
match p , q with
| Garbled , _ | _ , Garbled -> false
| Str(a,n) , Str(b,m) -> (* dst =?= repeated(src,n/m) *)
equal_atom a b && n >= m && (n mod m = 0)
begin
match compare_slot ~dst:a ~src:b with
| Mismatch -> false
| Drem a' ->
let w1 = a' @ decr_slot a n [] in
let w2 = decr_slot b m [] in
let cmp = compare ~dst:w1 ~src:w2 in
repeated_result ~src cmp
| Srem _ ->
false
| Equal -> (* dst =?= repeated(src,n/m) *)
n >= m && (n mod m = 0)
end
| Arr(u,n) , Arr(v,m) ->
begin
match compare ~dst:u ~src:v with
match compare ~dst:(layout u) ~src:(layout v) with
| Mismatch -> false
| Drem u' ->
let w1 = u' @ add_array u (n-1) [] in
......
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