From 3f3a191b1b8b7af06ccb33ddc85020504a774345 Mon Sep 17 00:00:00 2001
From: Christophe Garion <tofgarion@runbox.com>
Date: Fri, 24 Feb 2023 16:47:16 +0100
Subject: [PATCH] [wp_strategies] refactor documentation
---
.../lustrec_wp_strategies.ml | 2 +-
.../lustrec_wp_strategies_definitions.ml | 49 ++++++++++++-------
.../lustrec_wp_strategies_options.ml | 8 ++-
.../lustrec_wp_strategies_run.ml | 10 +++-
4 files changed, 47 insertions(+), 22 deletions(-)
diff --git a/lustrec_wp_strategies/lustrec_wp_strategies.ml b/lustrec_wp_strategies/lustrec_wp_strategies.ml
index 6643c65f..356921e2 100644
--- a/lustrec_wp_strategies/lustrec_wp_strategies.ml
+++ b/lustrec_wp_strategies/lustrec_wp_strategies.ml
@@ -1,3 +1,3 @@
(** LustreC WP strategies plug-in.
- No function is exported. *)
+ No function/module is exported. *)
diff --git a/lustrec_wp_strategies/lustrec_wp_strategies_definitions.ml b/lustrec_wp_strategies/lustrec_wp_strategies_definitions.ml
index 0ecd3ddd..18285c38 100644
--- a/lustrec_wp_strategies/lustrec_wp_strategies_definitions.ml
+++ b/lustrec_wp_strategies/lustrec_wp_strategies_definitions.ml
@@ -1,6 +1,14 @@
+(** This module contains the strategies that should be used by WP to
+ prove ACSL contracts generated by LustreC.
+
+ @author Lélio Brun
+ *)
+
+(* Globally open WP module. *)
open Wp
-(* check that a given predicate name is a transition and return its index *)
+(** Checks that a given predicate name is a transition
+ and returns its index. *)
let is_transition (f : Lang.lfun) : int option =
let open Str in
let r = regexp "_transition\\([0-9]+\\)$" in
@@ -10,7 +18,8 @@ let is_transition (f : Lang.lfun) : int option =
Some (int_of_string (matched_group 1 s))
with Not_found -> None
-(* check that a given predicate name is a transition with given index *)
+(** Checks that a given predicate name is a transition with a given
+ index. *)
let is_transition_n (n : int) (f : Lang.lfun) : bool =
let open Str in
let r = regexp ("_transition" ^ string_of_int n ^ "$") in
@@ -19,7 +28,7 @@ let is_transition_n (n : int) (f : Lang.lfun) : bool =
true
with Not_found -> false
-(* check that a given predicate name is a memory pack simulation *)
+(** Checks that a given predicate name is a memory pack simulation. *)
let is_pack (f : Lang.lfun) : bool =
let open Str in
let r = regexp "_pack\\(\\|[0-9]+\\|_base\\)$" in
@@ -29,17 +38,17 @@ let is_pack (f : Lang.lfun) : bool =
true
with Not_found -> false
-(* tactical selection of the goal *)
+(** Tactical selection of the goal. *)
let select_g (g : Lang.F.pred) : Tactical.selection =
let open Tactical in
Clause (Goal g)
-(* tactical selection of an hypothesis *)
+(** Tactical selection of an hypothesis. *)
let select_h (h : Conditions.step) : Tactical.selection =
let open Tactical in
Clause (Step h)
-(* get variables and predicate under existential binder *)
+(** Gets variables and predicate under existential binder. *)
let existential_vars_g (g : Lang.F.pred) : Lang.F.var list * Lang.F.term =
let open Lang.F in
let copy = pool () in
@@ -48,7 +57,7 @@ let existential_vars_g (g : Lang.F.pred) : Lang.F.var list * Lang.F.term =
let vars, g = e_open ~forall:false ~lambda:false ~pool (e_prop g) in
List.map snd vars, g
-(* find the index of the first element that verifies p in l *)
+(** Finds the index of the first element that verifies [p] in [l]. *)
let find_index p l =
let rec aux i = function
| [] ->
@@ -58,14 +67,15 @@ let find_index p l =
in
aux 0 l
-(* check if the term t is the variable v *)
+(** Checks if the term [t] is the variable [v]. *)
let is_var (v : Lang.F.var) (t : Lang.F.term) : bool =
match Repr.term t with Var w -> v = w | _ -> false
+(** Exception used when a witness is found. *)
exception Found of Tactical.selection list
-(* a function to search a transition call in the hypotheses *)
-(* that can be unified with a term *)
+(** Searches a transition call in the hypotheses that can
+ be unified with a term *)
let rec unify (push : Strategy.strategy -> unit) (sequent : Conditions.sequent)
(vars : Lang.F.var list) (term : Lang.F.term) : unit =
let hyps = fst sequent in
@@ -122,7 +132,7 @@ let rec unify (push : Strategy.strategy -> unit) (sequent : Conditions.sequent)
| _ ->
Lang.F.lc_iter (unify push sequent vars) term
-(* Transitions heuristic *)
+(** Class defining transitions heuristic. *)
class lustrec_transitions : Strategy.heuristic =
object
method id = "LustreC:Transitions" (* required, must be unique *)
@@ -151,7 +161,8 @@ class lustrec_transitions : Strategy.heuristic =
()
end
-(* unfold f(es) in the given context (context is handled with side-effects) *)
+(** Unfolds [f] function(s) in the given context (context is
+ handled with side-effects). *)
let definition (context : WpContext.context) (f : Lang.lfun)
(es : Lang.F.term list) : Lang.F.term =
let on_ctx f = WpContext.on_context context f in
@@ -163,7 +174,7 @@ let definition (context : WpContext.context) (f : Lang.lfun)
| _ ->
assert false
-(* rewrite a sequent by unfolding a top-level memory pack relation *)
+(** Rewrites a sequent by unfolding a top-level memory pack relation. *)
let unfold_process (context : WpContext.context) (t : Lang.F.term)
(sequent : Conditions.sequent) : Conditions.sequent option =
match Repr.term t with
@@ -173,11 +184,11 @@ let unfold_process (context : WpContext.context) (t : Lang.F.term)
| _ ->
None
-(* sequent equality *)
+(** Defines an equality relation on sequents. *)
let eq_sequent s1 s2 = Lang.F.eqp (snd s1) (snd s2)
-(* rewrite a sequent by recursively unfolding memory pack relations, by *)
-(* iterating over sub-terms *)
+(** Rewrites a sequent by recursively unfolding memory pack relations
+ by iterating over sub-terms. *)
let rec rewrite_process (context : WpContext.context)
(sequent : Conditions.sequent) : Conditions.sequent =
let goal = Lang.F.e_prop (snd sequent) in
@@ -203,7 +214,7 @@ let rec rewrite_process (context : WpContext.context)
sequent
with Found sequent' -> rewrite_process context sequent')
-(* Memory Packs tactical *)
+(** Class defining Memory Packs tactical. *)
class unfold_rec =
object
inherit
@@ -219,10 +230,10 @@ class unfold_rec =
(fun sequent -> [ "", rewrite_process context sequent ])
end
-(* Memory Packs strategy *)
+(** Memory Packs strategy. *)
let unfold_rec_strategy = Strategy.make (new unfold_rec) ~arguments:[]
-(* Memory Packs heuristic *)
+(** Class defining Memory Packs heuristic. *)
class lustrec_memory_packs : Strategy.heuristic =
object
method id = "LustreC:MemoryPacks" (* required, must be unique *)
diff --git a/lustrec_wp_strategies/lustrec_wp_strategies_options.ml b/lustrec_wp_strategies/lustrec_wp_strategies_options.ml
index e09feca2..b22a11eb 100644
--- a/lustrec_wp_strategies/lustrec_wp_strategies_options.ml
+++ b/lustrec_wp_strategies/lustrec_wp_strategies_options.ml
@@ -1,6 +1,12 @@
-(* Register the plugin *)
+(** This module contains options for the LustreC WP strategies plugin.
+
+ @author Christophe Garion
+*)
+
+(** Content of the welcome message. *)
let help_msg = "WP strategies needed for proving ACSL assertions generating with LustreC"
+(** Register the plugin to Frama-C. *)
module Self = Plugin.Register
(struct
let name = "LustreC WP Strategies"
diff --git a/lustrec_wp_strategies/lustrec_wp_strategies_run.ml b/lustrec_wp_strategies/lustrec_wp_strategies_run.ml
index fab21ad8..09a13297 100644
--- a/lustrec_wp_strategies/lustrec_wp_strategies_run.ml
+++ b/lustrec_wp_strategies/lustrec_wp_strategies_run.ml
@@ -1,7 +1,15 @@
-(* Register strategies and print simple message *)
+(** This module contains the function to be run when the module is
+ loaded and also registers the strategies wrt WP plugin.
+
+ @author Christophe Garion
+ @author Lelio Brun
+*)
+
+(** Prints a message when the plugin is loaded. *)
let run () =
Lustrec_wp_strategies_options.Self.result "LustreC WP strategies available."
+(** Register strategies to WP and print simple message when used. *)
let () =
Wp.Strategy.register (new Lustrec_wp_strategies_definitions.lustrec_transitions);
Wp.Strategy.register (new Lustrec_wp_strategies_definitions.lustrec_memory_packs);
--
GitLab