From f91260fb589507c1d4f85c902af38a21a9ad03cf Mon Sep 17 00:00:00 2001
From: Lionel Blatter <Lionel.BLATTER@cea.fr>
Date: Thu, 25 Jun 2020 22:55:03 +0200
Subject: [PATCH] Add support for recursive Extended annotation in AST
---
src/kernel_internals/typing/mergecil.ml | 37 +++++++++++--------
src/kernel_services/ast_data/cil_types.mli | 1 +
.../ast_printing/cil_types_debug.ml | 1 +
.../ast_queries/acsl_extension.ml | 1 +
src/kernel_services/ast_queries/cil.ml | 3 ++
.../ast_queries/logic_utils.ml | 6 ++-
src/plugins/value/utils/widen_hints_ext.ml | 1 +
7 files changed, 32 insertions(+), 18 deletions(-)
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index 805f4e06efe..21989d0a2e8 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -442,28 +442,33 @@ let hash_list f l =
| _ -> acc
in aux 47 3 l
-let hash_ext_kind = function
- | Ext_id i -> Datatype.Int.hash i
- | Ext_terms terms -> 29 * (hash_list Logic_utils.hash_term terms)
- | Ext_preds preds -> 47 * (hash_list Logic_utils.hash_predicate preds)
-
-let compare_ext_kind k1 k2 =
- match k1, k2 with
- | Ext_id i1, Ext_id i2 -> Datatype.Int.compare i1 i2
- | Ext_id _, _ -> 1 | _, Ext_id _ -> -1
- | Ext_terms terms1, Ext_terms terms2 ->
- Extlib.list_compare Logic_utils.compare_term terms1 terms2
- | Ext_terms _, _ -> 1 | _, Ext_terms _ -> -1
- | Ext_preds p1, Ext_preds p2 ->
- Extlib.list_compare Logic_utils.compare_predicate p1 p2
module ExtMerging =
Merging
(struct
type t = acsl_extension
- let hash (e : acsl_extension) =
+ let rec hash (e : acsl_extension) =
+ let hash_ext_kind = function
+ | Ext_id i -> Datatype.Int.hash i
+ | Ext_terms terms -> 29 * (hash_list Logic_utils.hash_term terms)
+ | Ext_preds preds -> 47 * (hash_list Logic_utils.hash_predicate preds)
+ | Ext_annot annots -> 5 * (hash_list hash annots)
+ in
Datatype.String.hash e.ext_name + 5 * hash_ext_kind e.ext_kind
- let compare (e1 : acsl_extension) (e2 : acsl_extension) =
+ let rec compare (e1 : acsl_extension) (e2 : acsl_extension) =
+ let compare_ext_kind k1 k2 =
+ match k1, k2 with
+ | Ext_id i1, Ext_id i2 -> Datatype.Int.compare i1 i2
+ | Ext_id _, _ -> 1 | _, Ext_id _ -> -1
+ | Ext_terms terms1, Ext_terms terms2 ->
+ Extlib.list_compare Logic_utils.compare_term terms1 terms2
+ | Ext_terms _, _ -> 1 | _, Ext_terms _ -> -1
+ | Ext_preds p1, Ext_preds p2 ->
+ Extlib.list_compare Logic_utils.compare_predicate p1 p2
+ | Ext_preds _, _ -> 1 | _, Ext_preds _ -> -1
+ | Ext_annot a1 , Ext_annot a2 ->
+ Extlib.list_compare compare a1 a2
+ in
let res = Datatype.String.compare e1.ext_name e2.ext_name in
if res <> 0 then res
else
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index 48697d89dc5..5f182a4a885 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -1692,6 +1692,7 @@ and acsl_extension_kind =
| Ext_id of int (** id used internally by the extension itself. *)
| Ext_terms of term list
| Ext_preds of predicate list
+ | Ext_annot of acsl_extension list
(** a list of predicates, the most common case of for extensions *)
(** Where are we expected to find corresponding extension keyword.
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index 9f6037a6b45..45e5515947e 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -921,6 +921,7 @@ and pp_acsl_extension_kind fmt = function
| Ext_id(int) -> Format.fprintf fmt "Ext_id(%a)" pp_int int
| Ext_terms(term_list) -> Format.fprintf fmt "Ext_terms(%a)" (pp_list pp_term) term_list
| Ext_preds(predicate_list) -> Format.fprintf fmt "Ext_preds(%a)" (pp_list pp_predicate) predicate_list
+ | Ext_annot(annotation_list ) -> Format.fprintf fmt "Ext_annots(%a)" (pp_list pp_acsl_extension) annotation_list
and pp_behavior fmt behavior =
Format.fprintf fmt
diff --git a/src/kernel_services/ast_queries/acsl_extension.ml b/src/kernel_services/ast_queries/acsl_extension.ml
index ff6f3c5060c..0d3efe6680d 100644
--- a/src/kernel_services/ast_queries/acsl_extension.ml
+++ b/src/kernel_services/ast_queries/acsl_extension.ml
@@ -47,6 +47,7 @@ let default_printer printer fmt = function
| Ext_id i -> Format.fprintf fmt "%d" i
| Ext_terms ts -> Pretty_utils.pp_list ~sep:",@ " printer#term fmt ts
| Ext_preds ps -> Pretty_utils.pp_list ~sep:",@ " printer#predicate fmt ps
+ | Ext_annot an -> Pretty_utils.pp_list ~sep:",@ " printer#extended fmt an
let default_short_printer name _printer fmt _ext_kind =
Format.fprintf fmt "%s" name
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 04582c3557e..f99204de3a4 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -1994,6 +1994,9 @@ and childrenCilExtended vis p =
| Ext_preds preds ->
let preds' = mapNoCopy (visitCilPredicate vis) preds in
if preds == preds' then p else Ext_preds preds'
+ | Ext_annot annots ->
+ let annots' = mapNoCopy (visitCilExtended vis) annots in
+ if annots == annots' then p else Ext_annot annots'
and visitCilPredicates vis ps = mapNoCopy (visitCilIdPredicate vis) ps
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 7fd192b397e..481fc909734 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -1186,7 +1186,7 @@ let is_same_pragma p1 p2 =
| Impact_pragma p1, Impact_pragma p2 -> is_same_impact_pragma p1 p2
| (Loop_pragma _ | Slice_pragma _ | Impact_pragma _), _ -> false
-let is_same_extension x1 x2 =
+let rec is_same_extension x1 x2 =
Datatype.String.equal x1.ext_name x2.ext_name &&
(x1.ext_has_status = x2.ext_has_status) &&
match x1.ext_kind, x2.ext_kind with
@@ -1195,7 +1195,9 @@ let is_same_extension x1 x2 =
is_same_list is_same_term t1 t2
| Ext_preds p1, Ext_preds p2 ->
is_same_list is_same_predicate p1 p2
- | (Ext_id _ | Ext_preds _ | Ext_terms _), _ -> false
+ | Ext_annot a1, Ext_annot a2 ->
+ is_same_list is_same_extension a1 a2
+ | (Ext_id _ | Ext_preds _ | Ext_terms _ | Ext_annot _ ), _ -> false
let is_same_code_annotation (ca1:code_annotation) (ca2:code_annotation) =
match ca1.annot_content, ca2.annot_content with
diff --git a/src/plugins/value/utils/widen_hints_ext.ml b/src/plugins/value/utils/widen_hints_ext.ml
index bcf81060871..449c0c67520 100644
--- a/src/plugins/value/utils/widen_hints_ext.ml
+++ b/src/plugins/value/utils/widen_hints_ext.ml
@@ -148,6 +148,7 @@ let printer _pp fmt ext =
match ext with
| Ext_id _ -> assert false
| Ext_preds _ -> assert false
+ | Ext_annot _ -> assert false
| Ext_terms terms ->
match widen_hint_terms_of_terms terms with
| Some (hint_lval, hint_terms) ->
--
GitLab