From 4f9b2e5319370237fb649d62a88117e3b6781bb0 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Wed, 26 Jul 2023 14:08:32 +0200
Subject: [PATCH] Add default requires for prototypes in safe mode
---
src/kernel_internals/typing/populate_spec.ml | 118 ++++++++++++-------
src/kernel_services/ast_data/property.ml | 14 ++-
2 files changed, 84 insertions(+), 48 deletions(-)
diff --git a/src/kernel_internals/typing/populate_spec.ml b/src/kernel_internals/typing/populate_spec.ml
index 3164f227db5..76f20f9e9b5 100644
--- a/src/kernel_internals/typing/populate_spec.ml
+++ b/src/kernel_internals/typing/populate_spec.ml
@@ -28,6 +28,7 @@ type mode = ACSL | Safe | Frama_C | Other of string
type config = {
exits: mode;
assigns: mode;
+ requires: mode;
allocates: mode;
terminates: mode;
}
@@ -37,12 +38,21 @@ type 'a result = Kept | Generated of 'a
let default = Cil.default_behavior_name
let emitter =
- Emitter.create "gen"
- [ Funspec ; Property_status ] ~correctness:[] ~tuning:[]
+ Emitter.create "PopulateSpec"
+ [ Funspec; Property_status ] ~correctness:[] ~tuning:[]
let emit_status status ppt =
Property_status.emit emitter ~hyps:[] ppt status
+let completes_generic (type clause) completes table =
+ let exception Ok of clause list in
+ let collect l b = Hashtbl.find table b :: l in
+ let collect bhvs =
+ try let r = List.fold_left collect [] bhvs in raise (Ok r)
+ with Not_found -> ()
+ in
+ try List.iter collect completes; None with Ok l -> Some l
+
module type Generator =
sig
@@ -104,17 +114,10 @@ struct
let exits = List.filter (fun (k, _ ) -> Exits = k) b.b_post_cond in
if exits <> [] then Hashtbl.add table b.b_name exits
in
- List.iter iter spec.spec_behavior ;
+ List.iter iter spec.spec_behavior;
table
- let completes completes table =
- let exception Ok of clause list in
- let collect l b = Hashtbl.find table b :: l in
- let collect bhvs =
- try let r = List.fold_left collect [] bhvs in raise (Ok r)
- with Not_found -> ()
- in
- try List.iter collect completes ; None with Ok l -> Some l
+ let completes = completes_generic
let acsl_default () = []
@@ -165,24 +168,13 @@ struct
let collect_behaviors spec =
let table = Hashtbl.create 17 in
- let iter { b_name ; b_assigns } =
+ let iter { b_name; b_assigns } =
if b_assigns <> WritesAny then Hashtbl.add table b_name b_assigns
in
- List.iter iter spec.spec_behavior ;
+ List.iter iter spec.spec_behavior;
table
- let completes (completes : string list list) (table : behaviors) =
- let assigns = function
- | WritesAny -> raise Not_found
- | Writes l -> Writes l
- in
- let exception Ok of assigns list in
- let collect l b = (assigns @@ Hashtbl.find table b) :: l in
- let collect bhvs =
- try let r = List.fold_left collect [] bhvs in raise (Ok r)
- with Not_found -> ()
- in
- try List.iter collect completes ; None with Ok l -> Some l
+ let completes = completes_generic
let acsl_default () =
WritesAny
@@ -257,6 +249,54 @@ struct
end
+module Requires_generator =
+struct
+
+ type clause = identified_predicate list
+ type behaviors = (string, clause) Hashtbl.t
+
+ let has_behavior name behaviors =
+ Hashtbl.mem behaviors name
+
+ let collect_behaviors spec =
+ let table = Hashtbl.create 17 in
+ let iter { b_name; b_requires } =
+ if b_requires <> [] then Hashtbl.add table b_name b_requires
+ in
+ List.iter iter spec.spec_behavior;
+ table
+
+ let completes = completes_generic
+
+ let acsl_default () = []
+
+ let safe_default has_body =
+ if has_body
+ then []
+ else [ Logic_const.(new_predicate pfalse) ]
+
+ let frama_c_default _ =
+ acsl_default ()
+
+ let combine_default (clauses : clause list) =
+ let flatten_require clause =
+ List.map (fun p -> p.ip_content.tp_statement) clause
+ |> List.sort_uniq Cil_datatype.PredicateStructEq.compare
+ |> Logic_const.pands
+ in
+ let preds =
+ List.map flatten_require clauses
+ |> Logic_const.pors
+ in
+ [ Logic_const.new_predicate preds ]
+
+ let custom_default _mode _kf _spec =
+ acsl_default ()
+
+ let emit _ _ _ _ = ()
+
+end
+
module Allocates_generator =
struct
type clause = allocation
@@ -267,24 +307,13 @@ struct
let collect_behaviors spec =
let table = Hashtbl.create 17 in
- let iter { b_name ; b_allocation } =
+ let iter { b_name; b_allocation } =
if b_allocation <> FreeAllocAny then Hashtbl.add table b_name b_allocation
in
- List.iter iter spec.spec_behavior ;
+ List.iter iter spec.spec_behavior;
table
- let completes (completes : string list list) (table : behaviors) =
- let allocation = function
- | FreeAllocAny -> raise Not_found
- | alloc -> alloc
- in
- let exception Ok of allocation list in
- let collect l b = (allocation @@ Hashtbl.find table b) :: l in
- let collect bhvs =
- try let r = List.fold_left collect [] bhvs in raise (Ok r)
- with Not_found -> ()
- in
- try List.iter collect completes ; None with Ok l -> Some l
+ let completes = completes_generic
let acsl_default () =
FreeAlloc([],[])
@@ -359,7 +388,7 @@ struct
acsl_default ()
let combine_default _ =
- acsl_default ()
+ assert false
let custom_default _mode _kf _spec =
acsl_default ()
@@ -386,6 +415,7 @@ end
module Exits = Make(Exits_generator)
module Assigns = Make(Assigns_generator)
+module Requires = Make(Requires_generator)
module Allocates = Make(Allocates_generator)
module Terminates = Make(Terminates_generator)
@@ -401,6 +431,7 @@ let get_mode = function
let build_config mode = {
exits = mode;
assigns = mode;
+ requires = mode;
allocates = mode;
terminates = mode;
}
@@ -416,6 +447,7 @@ let get_config () =
match k with
| "exits" -> {conf with exits = mode}
| "assigns" -> {conf with assigns = mode}
+ | "requires" -> {conf with requires = mode}
| "allocates" -> {conf with allocates = mode}
| "terminates" -> {conf with terminates = mode}
| s ->
@@ -430,6 +462,7 @@ let do_populate kf original_spec =
let exits = Exits.get_default config.exits kf original_spec in
let assigns = Assigns.get_default config.assigns kf original_spec in
+ let requires = Requires.get_default config.requires kf original_spec in
let allocates = Allocates.get_default config.allocates kf original_spec in
let terminates = Terminates.get_default config.terminates kf original_spec in
@@ -441,6 +474,7 @@ let do_populate kf original_spec =
let bhv = Cil.mk_behavior () in
let bhv = { bhv with b_post_cond = generated bhv.b_post_cond exits } in
let bhv = { bhv with b_assigns = generated bhv.b_assigns assigns } in
+ let bhv = { bhv with b_requires = generated bhv.b_requires requires } in
let bhv = { bhv with b_allocation = generated bhv.b_allocation allocates } in
let spec = Cil.empty_funspec () in
@@ -468,8 +502,8 @@ let () = Ast.add_linked_state Is_populated.self
let populate_funspec kf spec =
if Is_populated.mem kf then false
else begin
- do_populate kf spec ;
- Is_populated.add kf () ;
+ do_populate kf spec;
+ Is_populated.add kf ();
true
end
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index 95c554429b7..8a10e8ec185 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -1351,12 +1351,14 @@ let ip_assigns_of_code_annot kf st ca = match ca.annot_content with
let ip_from_of_code_annot kf st ca = match ca.annot_content with
| AAssigns(_,WritesAny) -> []
| AAssigns (_,Writes l) ->
- let treat_from acc (out, froms) = match froms with FromAny -> acc
- | From _ ->
- let ip =
- Option.get (ip_of_from kf st (Id_loop ca) (out, froms))
- in
- ip::acc
+ let treat_from acc (out, froms) =
+ match froms with
+ | FromAny -> acc
+ | From _ ->
+ let ip =
+ Option.get (ip_of_from kf st (Id_loop ca) (out, froms))
+ in
+ ip::acc
in
List.fold_left treat_from [] l
| _ -> []
--
GitLab