From dc9fadac19130c08bb2d4d9bac1264ca66322cc0 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 12 Oct 2021 16:05:47 +0200
Subject: [PATCH] [wp] Introduce a notion of coloring predicate
---
src/plugins/wp/Lang.ml | 34 ++++++++++++++++++++++------------
src/plugins/wp/Lang.mli | 12 +++++++++---
2 files changed, 31 insertions(+), 15 deletions(-)
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 7003dcb3557..d7ec3fb726f 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -430,6 +430,7 @@ and model = {
m_result : sort ;
m_typeof : tau option list -> tau ;
m_source : source ;
+ m_coloring : bool ;
}
and source =
@@ -448,6 +449,10 @@ let tau_of_lfun phi ts =
| Sbool -> Bool
| _ -> m.m_typeof ts
+let is_coloring_lfun = function
+ | ACSL _ | CTOR _ -> false
+ | Model { m_coloring } -> m_coloring
+
type balance = Nary | Left | Right
let not_found _ = raise Not_found
@@ -467,6 +472,7 @@ let symbolf
?(params=[])
?(sort=Logic.Sdata)
?(result:tau option)
+ ?(coloring=false)
?(typecheck:(tau option list -> tau) option)
name =
let buffer = Buffer.create 80 in
@@ -500,20 +506,21 @@ let symbolf
m_result = result ;
m_typeof = typeof ;
m_source = source ;
+ m_coloring = coloring ;
}
) (Format.formatter_of_buffer buffer) name
let extern_s
- ~library ?link ?category ?params ?sort ?result ?typecheck name =
+ ~library ?link ?category ?params ?sort ?result ?coloring ?typecheck name =
symbolf
- ~library ?category ?params ?sort ?result ?typecheck ?link "%s" name
+ ~library ?category ?params ?sort ?result ?coloring ?typecheck ?link "%s" name
let extern_f
- ~library ?link ?balance ?category ?params ?sort ?result ?typecheck name =
+ ~library ?link ?balance ?category ?params ?sort ?result ?coloring ?typecheck name =
symbolf
- ~library ?category ?params ?link ?balance ?sort ?result ?typecheck name
+ ~library ?category ?params ?link ?balance ?sort ?result ?coloring ?typecheck name
-let extern_p ~library ?bool ?prop ?link ?(params=[]) () =
+let extern_p ~library ?bool ?prop ?link ?(params=[]) ?(coloring=false) () =
let link =
match bool,prop,link with
| Some b , Some p , None -> infoprover (Engine.F_bool_prop(b,p))
@@ -526,10 +533,11 @@ let extern_p ~library ?bool ?prop ?link ?(params=[]) () =
m_params = params ;
m_result = Logic.Sprop;
m_typeof = not_found;
- m_source = Extern (new_extern ~library ~link ~debug)
+ m_source = Extern (new_extern ~library ~link ~debug) ;
+ m_coloring = coloring ;
}
-let extern_fp ~library ?(params=[]) ?link phi =
+let extern_fp ~library ?(params=[]) ?link ?(coloring=false) phi =
let link = match link with
| None -> infoprover (Engine.F_call phi)
| Some link -> map_infoprover (fun phi -> Engine.F_call(phi)) link in
@@ -541,19 +549,21 @@ let extern_fp ~library ?(params=[]) ?link phi =
m_source = Extern (new_extern
~library
~link
- ~debug:phi)
+ ~debug:phi) ;
+ m_coloring = coloring ;
}
-let generated_f ?context ?category ?params ?sort ?result name =
- symbolf ?context ?category ?params ?sort ?result name
+let generated_f ?context ?category ?params ?sort ?result ?coloring name =
+ symbolf ?context ?category ?params ?sort ?result ?coloring name
-let generated_p ?context name =
+let generated_p ?context ?(coloring=false) name =
Model {
m_category = Logic.Function ;
m_params = [] ;
m_result = Logic.Sprop;
m_typeof = not_found;
- m_source = generated ?context name
+ m_source = generated ?context name ;
+ m_coloring = coloring ;
}
let extern_t name ~link ~library =
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index d2c06c5839a..c878c17272d 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -92,6 +92,7 @@ and model = {
m_result : sort ;
m_typeof : tau option list -> tau ;
m_source : source ;
+ m_coloring : bool ;
}
and source =
@@ -123,6 +124,7 @@ val extern_s :
?params:sort list ->
?sort:sort ->
?result:tau ->
+ ?coloring:bool ->
?typecheck:(tau option list -> tau) ->
string -> lfun
@@ -134,6 +136,7 @@ val extern_f :
?params:sort list ->
?sort:sort ->
?result:tau ->
+ ?coloring:bool ->
?typecheck:(tau option list -> tau) ->
('a,Format.formatter,unit,lfun) format4 -> 'a
(** balance just give a default when link is not specified *)
@@ -144,16 +147,17 @@ val extern_p :
?prop:string ->
?link:Engine.link infoprover ->
?params:sort list ->
+ ?coloring:bool ->
unit -> lfun
val extern_fp : library:library -> ?params:sort list ->
- ?link:string infoprover -> string -> lfun
+ ?link:string infoprover -> ?coloring:bool -> string -> lfun
val generated_f : ?context:bool -> ?category:lfun category ->
- ?params:sort list -> ?sort:sort -> ?result:tau ->
+ ?params:sort list -> ?sort:sort -> ?result:tau -> ?coloring:bool ->
('a,Format.formatter,unit,lfun) format4 -> 'a
-val generated_p : ?context:bool -> string -> lfun
+val generated_p : ?context:bool -> ?coloring:bool -> string -> lfun
val extern_t:
string -> link:string infoprover -> library:library -> mdt
@@ -193,6 +197,8 @@ val parameters : (lfun -> sort list) -> unit (** definitions *)
val name_of_lfun : lfun -> string
val name_of_field : field -> string
+val is_coloring_lfun : lfun -> bool
+
(** {2 Logic Formulae} *)
module ADT : Logic.Data with type t = adt
--
GitLab