Commit a0ada244 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[kernel] Simplifies merge assigns

parent 637af0a0
...@@ -109,44 +109,40 @@ ...@@ -109,44 +109,40 @@
let loc_ext d = { extended_node = d; extended_loc = loc () } let loc_ext d = { extended_node = d; extended_loc = loc () }
let concat_deps ds1 ds2 = let filter_from l = function
let fold ds d = if List.exists (is_same_lexpr d) ds then ds else d :: ds in | FromAny ->
let ds = List.fold_left fold [] ds1 in l, FromAny
let ds = List.fold_left fold ds ds2 in | From ds ->
List.rev ds let f ds d = if List.exists (is_same_lexpr d) ds then ds else d :: ds in
l, From(List.(rev (fold_left f [] ds)))
let filter_from (l, d) =
match d with
| From ds -> l, From (concat_deps [] ds)
| _ -> l, d
let concat_froms a1 a2 = let concat_froms a1 a2 =
let compare_pair (l1,_) (l2,_) = is_same_lexpr l1 l2 in let compare_pair (b1,_) (b2,_) = is_same_lexpr b1 b2 in
(* NB: the following has an horrible complexity, but the order of (* NB: the following has an horrible complexity, but the order of
clauses in the input is preserved. *) clauses in the input is preserved. *)
let concat_one acc (_,d2 as f2) = let concat_one acc (l, f2) =
let f2 = filter_from f2 in let (_, f2) as p = filter_from l f2 in
try try
let (_,d1) = List.find (compare_pair f2) acc let (_,f1) = List.find (compare_pair p) acc
in in
match (d1, d2) with match (f1, f2) with
| _,FromAny -> | _,FromAny ->
(* the new fundeps does not give more information than the one (* the new fundeps does not give more information than the one
which is already present. Just ignore it. which is already present. Just ignore it.
*) *)
acc acc
| FromAny, From _ -> | FromAny, _ ->
(* the new fundeps is strictly more precise than the old one. (* the new fundeps is strictly more precise than the old one.
We replace the old dependency by the new one, but keep We replace the old dependency by the new one, but keep
the location at its old place in the list. This ensures the location at its old place in the list. This ensures
that we get the exact same clause if we try to that we get the exact same clause if we try to
link the original contract with its pretty-printed version. *) link the original contract with its pretty-printed version. *)
Extlib.replace compare_pair f2 acc Extlib.replace compare_pair p acc
| From _, From _ -> | From _, From _ ->
(* we keep the two functional dependencies, (* we keep the two functional dependencies,
as they have to be proved separately. *) as they have to be proved separately. *)
acc @ [f2] acc @ [p]
with Not_found -> acc @ [f2] with Not_found -> acc @ [p]
in List.fold_left concat_one a1 a2 in List.fold_left concat_one a1 a2
let concat_allocation fa1 fa2 = let concat_allocation fa1 fa2 =
......
...@@ -2912,23 +2912,17 @@ class cil_printer () = object (self) ...@@ -2912,23 +2912,17 @@ class cil_printer () = object (self)
(function (a,_) -> not (Logic_const.is_exit_status a.it_content)) (function (a,_) -> not (Logic_const.is_exit_status a.it_content))
l l
in in
let remove_duplicates l = let unique_assigned_locs =
let same t1 t2 = Cil_datatype.Term.equal t1.it_content t2.it_content in let same t1 t2 = Cil_datatype.Term.equal t1.it_content t2.it_content in
let rec aux l acc = let f l (a,_) = if List.exists (same a) l then l else a :: l in
match l with List.rev (List.fold_left f [] without_result)
| [] -> acc
| (x,_) :: l when List.exists (same x) acc -> aux l acc
| (x,_) :: l -> aux l (x :: acc)
in
List.rev (aux l [])
in in
let l = remove_duplicates without_result in
fprintf fmt "@[<h>%t%a@]" fprintf fmt "@[<h>%t%a@]"
(fun fmt -> if without_result <> [] then (fun fmt -> if without_result <> [] then
Format.fprintf fmt "%a " self#pp_acsl_keyword kw) Format.fprintf fmt "%a " self#pp_acsl_keyword kw)
(Pretty_utils.pp_list ~sep:",@ " ~suf:";@]" (Pretty_utils.pp_list ~sep:",@ " ~suf:";@]"
(fun fmt t -> self#identified_term fmt t)) (fun fmt t -> self#identified_term fmt t))
l unique_assigned_locs
method private assigns_deps kw fmt = function method private assigns_deps kw fmt = function
| WritesAny -> () | WritesAny -> ()
......
Markdown is supported
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