From 6f67d6a6a150400b80f77cce4bb1ee88f7643480 Mon Sep 17 00:00:00 2001
From: Virgile Robles <virgile.robles@protonmail.ch>
Date: Mon, 25 Jan 2021 18:05:09 +0100
Subject: [PATCH] Replacement assoc list more generic
---
meta_annotate.ml | 6 +++---
meta_deduce.ml | 2 +-
meta_dispatch.ml | 2 +-
meta_dispatch.mli | 2 +-
meta_parse.ml | 22 +++++++++++++++++++---
meta_parse.mli | 6 +++++-
6 files changed, 30 insertions(+), 10 deletions(-)
diff --git a/meta_annotate.ml b/meta_annotate.ml
index c3a16fb..a20ef3b 100644
--- a/meta_annotate.ml
+++ b/meta_annotate.ml
@@ -242,7 +242,7 @@ class calling_visitor flags all_mp table = object (self)
method calling_instance stmt called =
let addr_term = addr_of_tlval called in
- let assoc_list = [("\\called", addr_term)] in
+ let assoc_list = [("\\called", RepVariable addr_term)] in
List.iter (self # instantiate stmt assoc_list) mp_todo
method! vinst = function
@@ -317,7 +317,7 @@ class writing_visitor flags all_mp table = object(self)
| TVar lv, _ when flags.simpl && Meta_simplify.is_not_orig_variable lv -> ()
| written ->
let addr_term = addr_of_tlval written in
- let assoc_list = [("\\written", addr_term)] in
+ let assoc_list = [("\\written", RepVariable addr_term)] in
List.iter (self # instantiate ~post stmt assoc_list) mp_todo
(* Inspect function specs to see what it assigns and instantiate the
@@ -384,7 +384,7 @@ class reading_visitor flags all_mp table = object (self)
(* Instantiates the property while replacing \read terms *)
method reading_instance ?post stmt written =
let addr_term = addr_of_tlval written in
- let assoc_list = [("\\read", addr_term)] in
+ let assoc_list = [("\\read", RepVariable addr_term)] in
List.iter (self#instantiate ~post stmt assoc_list) mp_todo
(* Hashtable : stmt -> set of tlvals used in it. Used to avoid duplicate
diff --git a/meta_deduce.ml b/meta_deduce.ml
index 23a946c..58dca2d 100644
--- a/meta_deduce.ml
+++ b/meta_deduce.ml
@@ -118,7 +118,7 @@ let dummy_term loc = {
let dummy_unpack mp =
let terms = ["\\written"; "\\read"; "\\called"] in
- let assoc = List.map (fun t -> (t, dummy_term mp.mp_loc)) terms in
+ let assoc = List.map (fun t -> (t, RepVariable (dummy_term mp.mp_loc))) terms in
mp.mp_property (Kernel_function.dummy ()) assoc
let predicate_counter = ref 1
diff --git a/meta_dispatch.ml b/meta_dispatch.ml
index 2a05910..923996f 100644
--- a/meta_dispatch.ml
+++ b/meta_dispatch.ml
@@ -26,7 +26,7 @@ open Meta_options
type unpacked_metaproperty = {
ump_emitter : Emitter.t;
- ump_property : Kernel_function.t -> ?stmt:stmt -> (string * term) list -> predicate;
+ ump_property : Kernel_function.t -> ?stmt:stmt -> (string * replaced_kind) list -> predicate;
ump_ip : Property.t;
ump_counter : int ref;
ump_admit : bool;
diff --git a/meta_dispatch.mli b/meta_dispatch.mli
index 3232d36..dd72b00 100644
--- a/meta_dispatch.mli
+++ b/meta_dispatch.mli
@@ -26,7 +26,7 @@ open Meta_options
type unpacked_metaproperty = {
ump_emitter : Emitter.t;
- ump_property : Kernel_function.t -> ?stmt:stmt -> (string * term) list -> predicate;
+ ump_property : Kernel_function.t -> ?stmt:stmt -> (string * replaced_kind) list -> predicate;
ump_ip : Property.t;
ump_counter : int ref;
ump_admit : bool;
diff --git a/meta_parse.ml b/meta_parse.ml
index a76054e..252d8b4 100644
--- a/meta_parse.ml
+++ b/meta_parse.ml
@@ -59,11 +59,16 @@ type mp_translation =
| MtDefault (* translation activated, with unspecified mode *)
| MtNone
+(* Kinds of keywords that can be replaced in a MP instantiation *)
+type replaced_kind =
+ | RepVariable of term (* replace variable by term *)
+ | RepApp of (string * term) list (* replace application with arg by associated term *)
+
type metaproperty = {
mp_name : string;
mp_target : target;
mp_context : context;
- mp_property : Kernel_function.t -> (string * term) list -> predicate;
+ mp_property : Kernel_function.t -> (string * replaced_kind) list -> predicate;
mp_proof_method : mp_proof_method;
mp_translation : mp_translation;
mp_loc : Cil_types.location
@@ -142,7 +147,11 @@ let meta_type_term termassoc quantifiers kf loc orig_ctxt meta_ctxt env expr =
| PLapp ("\\bound", _, [bound]) ->
Meta_bindings.parse_bound meta_ctxt loc quantifiers bound
| PLvar vname when List.mem vname mp_terms ->
- begin try List.assoc vname termassoc
+ begin try
+ begin match List.assoc vname termassoc with
+ | RepVariable a -> a
+ | _ -> assert false
+ end
with _ -> meta_ctxt.error loc
"Variable %s forbidden in this context" vname
end
@@ -197,8 +206,15 @@ let rec process_targets tc expr = match expr.lexpr_node with
| _ -> TgSet (StrSet.singleton @@ process_single_target tc expr)
let pp_aslist fmt l =
+ let pp_replaced_kind fmt = function
+ | RepVariable v -> Printer.pp_term fmt v
+ | RepApp l ->
+ let pp_singular fmt (a, b) =
+ Format.fprintf fmt "(%s, %a)" a Printer.pp_term b
+ in Format.pp_print_list pp_singular fmt l
+ in
let pp_assoc fmt (a, b) =
- Format.fprintf fmt "(%s, %a)" a Printer.pp_term b
+ Format.fprintf fmt "(%s, %a)" a pp_replaced_kind b
in Format.pp_print_list pp_assoc fmt l
let delay_prop tc name lexpr kf aslist =
diff --git a/meta_parse.mli b/meta_parse.mli
index 712af94..a2efca8 100644
--- a/meta_parse.mli
+++ b/meta_parse.mli
@@ -53,11 +53,15 @@ type mp_translation =
| MtDefault
| MtNone
+type replaced_kind =
+ | RepVariable of term (* replace variable by term *)
+ | RepApp of (string * term) list (* replace application with arg by associated term *)
+
type metaproperty = {
mp_name : string;
mp_target : target;
mp_context : context;
- mp_property : Kernel_function.t -> (string * term) list -> predicate;
+ mp_property : Kernel_function.t -> (string * replaced_kind) list -> predicate;
mp_proof_method : mp_proof_method;
mp_translation : mp_translation;
mp_loc : Cil_types.location
--
GitLab