From 7f1bcb820fcae3b4ea36f57b2fa727298aeb6f67 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 24 Sep 2019 14:49:24 +0200
Subject: [PATCH] [Override Std] Simplifies spec generation
---
src/plugins/override_std/basic_blocks.ml | 33 +++++++++++++++++++++
src/plugins/override_std/basic_blocks.mli | 18 +++++++++++
src/plugins/override_std/memcmp.ml | 25 +++++-----------
src/plugins/override_std/memcpy.ml | 25 +++++-----------
src/plugins/override_std/override_table.ml | 10 +++++--
src/plugins/override_std/override_table.mli | 2 +-
6 files changed, 73 insertions(+), 40 deletions(-)
diff --git a/src/plugins/override_std/basic_blocks.ml b/src/plugins/override_std/basic_blocks.ml
index 03456bd5299..2ea6dd4db1f 100644
--- a/src/plugins/override_std/basic_blocks.ml
+++ b/src/plugins/override_std/basic_blocks.ml
@@ -138,3 +138,36 @@ let pseparated_memories ?loc p1 len1 p2 len2 =
let b1 = tbuffer_range ?loc p1 len1 in
let b2 = tbuffer_range ?loc p2 len2 in
pseparated ?loc [ b1 ; b2 ]
+
+let make_behavior
+ ?(name=Cil.default_behavior_name)
+ ?(assumes=[]) ?(requires=[]) ?(ensures=[])?(assigns=WritesAny)
+ ?(alloc=FreeAllocAny) ?(extension=[])
+ () =
+ {
+ b_name = name ;
+ b_requires = requires ;
+ b_assumes = assumes ;
+ b_post_cond = ensures ;
+ b_assigns = assigns ;
+ b_allocation = alloc;
+ b_extended = extension
+ }
+
+let default_comp_disj bhvs =
+ let b_names = List.filter (fun b -> not (String.equal Cil.default_behavior_name b))
+ (List.fold_left (fun l b -> b.b_name :: l) [] bhvs)
+ in match b_names with
+ | [] -> [], []
+ | _ -> [b_names], [b_names]
+
+let make_funspec bhvs ?(termination=None)
+ ?(complete_disjoint=(default_comp_disj bhvs)) () =
+ let complete, disjoint = complete_disjoint in
+ {
+ spec_behavior = bhvs ;
+ spec_variant = None ;
+ spec_terminates = termination ;
+ spec_complete_behaviors = complete ;
+ spec_disjoint_behaviors = disjoint
+ }
diff --git a/src/plugins/override_std/basic_blocks.mli b/src/plugins/override_std/basic_blocks.mli
index 396374230ce..f0eb5ad242c 100644
--- a/src/plugins/override_std/basic_blocks.mli
+++ b/src/plugins/override_std/basic_blocks.mli
@@ -46,3 +46,21 @@ val pseparated_memories: ?loc:location -> term -> term -> term -> term -> predic
val plet_len_div_size:
?loc:location -> logic_type -> term -> (term -> predicate) -> predicate
+
+val make_behavior:
+ ?name:string ->
+ ?assumes:identified_predicate list ->
+ ?requires:identified_predicate list ->
+ ?ensures:(termination_kind * identified_predicate) list ->
+ ?assigns:assigns ->
+ ?alloc:allocation ->
+ ?extension:acsl_extension list ->
+ unit ->
+ behavior
+
+val make_funspec:
+ behavior list ->
+ ?termination:identified_predicate option ->
+ ?complete_disjoint:(string list list * string list list) ->
+ unit ->
+ funspec
diff --git a/src/plugins/override_std/memcmp.ml b/src/plugins/override_std/memcmp.ml
index 6ed6fc00fbb..39ede274dbb 100644
--- a/src/plugins/override_std/memcmp.ml
+++ b/src/plugins/override_std/memcmp.ml
@@ -66,8 +66,11 @@ let generate_ensures loc s1 s2 len =
{ (presult_memcmp_len_bytes ~loc s1 s2 len) with pred_name = [ "equals" ] }
]
-let generate_spec loc kf c_s1 c_s2 clen =
- Kernel.feedback "Spec for: %a" Kernel_function.pretty kf ;
+let generate_spec vi loc =
+ let (c_s1, c_s2, clen) = match Cil.getFormalsDecl vi with
+ | [ s1 ; s2 ; len ] -> s1, s2, len
+ | _ -> assert false
+ in
let t = c_s1.vtype in
let s1 = cvar_to_tvar c_s1 in
let s2 = cvar_to_tvar c_s2 in
@@ -75,21 +78,7 @@ let generate_spec loc kf c_s1 c_s2 clen =
let requires = generate_requires loc s1 s2 len in
let assigns = generate_assigns loc t s1 s2 len in
let ensures = generate_ensures loc s1 s2 len in
- Annotations.add_requires Options.emitter kf requires ;
- Annotations.add_assigns ~keep_empty:false Options.emitter kf assigns ;
- Annotations.add_ensures Options.emitter kf ensures ;
- ()
-
-let finalize_override vi loc =
- let spec = Cil.empty_funspec () in
- Globals.Functions.replace_by_declaration spec vi loc ;
- let kf = Globals.Functions.get vi in
- let (s1, s2, len) = match Cil.getFormalsDecl vi with
- | [ s1 ; s2 ; len ] -> s1, s2, len
- | _ -> assert false
- in
- generate_spec loc kf s1 s2 len ;
- GFunDecl(spec, vi, loc)
+ make_funspec [make_behavior ~requires ~assigns ~ensures ()] ()
let generate_prototype t =
let name = function_name ^ "_" ^ (string_of_typ t) in
@@ -107,7 +96,7 @@ let generate_prototype t =
module Table = Override_table.Make(struct
let function_name = function_name
let build_prototype = generate_prototype
- let finalize = finalize_override
+ let build_spec = generate_spec
end)
let type_from_parameter x =
diff --git a/src/plugins/override_std/memcpy.ml b/src/plugins/override_std/memcpy.ml
index 125339b2713..f54cb0fd0a2 100644
--- a/src/plugins/override_std/memcpy.ml
+++ b/src/plugins/override_std/memcpy.ml
@@ -68,8 +68,11 @@ let generate_ensures loc dest src len =
{ (pcopied_len_bytes ~loc dest src len) with pred_name = [ "copied"] }
]
-let generate_spec loc kf cdest csrc clen =
- Kernel.feedback "Spec for: %a" Kernel_function.pretty kf ;
+let generate_spec vi loc =
+ let (cdest, csrc, clen) = match Cil.getFormalsDecl vi with
+ | [ dest ; src ; len ] -> dest, src, len
+ | _ -> assert false
+ in
let t = cdest.vtype in
let dest = cvar_to_tvar cdest in
let src = cvar_to_tvar csrc in
@@ -77,21 +80,7 @@ let generate_spec loc kf cdest csrc clen =
let requires = generate_requires loc dest src len in
let assigns = generate_assigns loc t dest src len in
let ensures = generate_ensures loc dest src len in
- Annotations.add_requires Options.emitter kf requires ;
- Annotations.add_assigns ~keep_empty:false Options.emitter kf assigns ;
- Annotations.add_ensures Options.emitter kf ensures ;
- ()
-
-let finalize_override vi loc =
- let spec = Cil.empty_funspec () in
- Globals.Functions.replace_by_declaration spec vi loc ;
- let kf = Globals.Functions.get vi in
- let (dest, src, len) = match Cil.getFormalsDecl vi with
- | [ dest ; src ; len ] -> dest, src, len
- | _ -> assert false
- in
- generate_spec loc kf dest src len ;
- GFunDecl(spec, vi, loc)
+ make_funspec [make_behavior ~requires ~assigns ~ensures ()] ()
let generate_prototype t =
let name = function_name ^ "_" ^ (string_of_typ t) in
@@ -110,7 +99,7 @@ let generate_prototype t =
module Table = Override_table.Make(struct
let function_name = function_name
let build_prototype = generate_prototype
- let finalize = finalize_override
+ let build_spec = generate_spec
end)
let type_from_parameter x =
diff --git a/src/plugins/override_std/override_table.ml b/src/plugins/override_std/override_table.ml
index bb0daaae617..d9acb213bdc 100644
--- a/src/plugins/override_std/override_table.ml
+++ b/src/plugins/override_std/override_table.ml
@@ -29,7 +29,7 @@ end
module type Override_generator = sig
val function_name: String.t
val build_prototype: Cil_types.typ -> Cil_types.varinfo
- val finalize: Cil_types.varinfo -> Cil_types.location -> Cil_types.global
+ val build_spec: Cil_types.varinfo -> Cil_types.location -> Cil_types.funspec
end
module Make_internal_table (M: Override_generator) =
@@ -51,8 +51,12 @@ module Make (Generator: Override_generator) = struct
fct
let get_globals loc =
- let add_global _ vi l = (Generator.finalize vi loc) :: l in
- Internal_table.fold add_global []
+ let finalize vi =
+ let spec = Generator.build_spec vi loc in
+ Globals.Functions.replace_by_declaration spec vi loc ;
+ Cil_types.GFunDecl(Cil.empty_funspec(), vi, loc)
+ in
+ Internal_table.fold (fun _ vi l -> (finalize vi) :: l) []
let mark_as_computed = Internal_table.mark_as_computed
end
diff --git a/src/plugins/override_std/override_table.mli b/src/plugins/override_std/override_table.mli
index e7d42d245a0..9be836b5d99 100644
--- a/src/plugins/override_std/override_table.mli
+++ b/src/plugins/override_std/override_table.mli
@@ -23,7 +23,7 @@
module type Override_generator = sig
val function_name: String.t
val build_prototype: Cil_types.typ -> Cil_types.varinfo
- val finalize: Cil_types.varinfo -> Cil_types.location -> Cil_types.global
+ val build_spec: Cil_types.varinfo -> Cil_types.location -> Cil_types.funspec
end
module type Table = sig
--
GitLab