From c7e28528f5fcfae9e1f92c532e93a2948bf0f3fa Mon Sep 17 00:00:00 2001
From: Virgile Robles <virgile.robles@protonmail.ch>
Date: Fri, 6 Nov 2020 14:43:38 +0100
Subject: [PATCH] Add conditional invariant context
---
README.md | 6 ++++++
meta_annotate.ml | 34 ++++++++++++++++++++++++----------
meta_deduce.ml | 1 +
meta_dispatch.ml | 2 +-
meta_parse.ml | 5 ++++-
meta_parse.mli | 1 +
tests/meta-wp/invariant.c | 23 ++++++++++++++++++++---
7 files changed, 57 insertions(+), 15 deletions(-)
diff --git a/README.md b/README.md
index fc3bebf..f0b8fc0 100644
--- a/README.md
+++ b/README.md
@@ -76,6 +76,12 @@ function defined in `main.c`.
The context is the situation in a target function in which the property must
hold. It can be one of the following :
+- `\conditional_invariant` : the property `P` is guarantted to be verified at
+ the end of the target function *if* it is verified at the begining.
+- `\precond` : the property `P` is a precondition of the target function and is
+ must hold at each of its callsites.
+- `\postcond` : the property `P` hold at the end of the target function for
+ every initial state satisfying the preconditions of the function.
- `\weak_invariant` : the property `P` is guaranteed to be verified at the
beginning and end of the target function.
- `\strong_invariant` : the property `P` must hold at every point of the target
diff --git a/meta_annotate.ml b/meta_annotate.ml
index b619888..a982eda 100644
--- a/meta_annotate.ml
+++ b/meta_annotate.ml
@@ -186,22 +186,34 @@ class weak_inv_visitor flags full_table table (pre, post) = object (self)
let pred_name = (Emitter.get_name ump.ump_emitter) :: pred'.pred_name in
let pred'' = {pred' with pred_name} in
let only_check = not ump.ump_assert in
- let ip_requires = Logic_const.new_predicate ~only_check pred'' in
- let ip_ensures = Logic_const.refresh_predicate ip_requires in
let deps = ref [] in
if pre then (
+ let ip_requires = Logic_const.new_predicate ~only_check pred'' in
Annotations.add_requires ump.ump_emitter kf [ip_requires];
let defb = Extlib.the (Cil.find_default_behavior (Annotations.funspec kf)) in
let rips = Property.ip_of_requires kf Kglobal defb ip_requires :: !deps in
let callsites_ip = get_callsites_ips kf rips in
deps := rips @ callsites_ip @ !deps
);
- if post then (
- Annotations.add_ensures ump.ump_emitter kf [(Normal, ip_ensures)];
+ let add_post ip =
+ Annotations.add_ensures ump.ump_emitter kf [(Normal, ip)];
let defb = Extlib.the (Cil.find_default_behavior (Annotations.funspec kf)) in
- let eip = Property.ip_of_ensures kf Kglobal defb (Normal, ip_ensures) in
+ let eip = Property.ip_of_ensures kf Kglobal defb (Normal, ip) in
deps := eip :: !deps
- );
+ in
+ begin match post with
+ | `None -> ()
+ | `Strict ->
+ let ip_ensures = Logic_const.new_predicate ~only_check pred'' in
+ add_post ip_ensures
+ | `Conditional ->
+ let pred' = Logic_const.pimplies (pred, pred) in
+ let pred'' = Meta_dispatch.name_mp_pred flags pred' ump.ump_counter in
+ let pred_name = (Emitter.get_name ump.ump_emitter) :: pred''.pred_name in
+ let pred''' = {pred'' with pred_name} in
+ let ip_ensures = Logic_const.new_predicate ~only_check pred''' in
+ add_post ip_ensures
+ end;
Meta_dispatch.add_dependency ump !deps
in
(* Delay actual instanciation for correct numbering *)
@@ -506,7 +518,7 @@ let lvals_of_predicate pred =
* maintain the invariant at the end
*)
class strong_inv_visitor flags all_mp table = object (self)
- inherit weak_inv_visitor flags all_mp table (true, true)
+ inherit weak_inv_visitor flags all_mp table (true, `Strict)
val mutable lenient = false
(* Given a lval which is to be modified, check if its modification
@@ -598,7 +610,7 @@ let report all_mp tables =
let annotate flags all_mp by_context =
let get_vis table = function
| Weak_invariant ->
- (new weak_inv_visitor flags all_mp table (true, true) :> Visitor.frama_c_visitor)
+ (new weak_inv_visitor flags all_mp table (true, `Strict) :> Visitor.frama_c_visitor)
| Calling ->
(new calling_visitor flags all_mp table :> Visitor.frama_c_visitor)
| Writing ->
@@ -608,9 +620,11 @@ let annotate flags all_mp by_context =
| Strong_invariant ->
(new strong_inv_visitor flags all_mp table :> Visitor.frama_c_visitor)
| Precond ->
- (new weak_inv_visitor flags all_mp table (true, false) :> Visitor.frama_c_visitor)
+ (new weak_inv_visitor flags all_mp table (true, `None) :> Visitor.frama_c_visitor)
| Postcond ->
- (new weak_inv_visitor flags all_mp table (false, true) :> Visitor.frama_c_visitor)
+ (new weak_inv_visitor flags all_mp table (false, `Strict) :> Visitor.frama_c_visitor)
+ | Conditional_invariant ->
+ (new weak_inv_visitor flags all_mp table (false, `Conditional) :> Visitor.frama_c_visitor)
in
List.iter (fun (ctx, table) ->
let vis = get_vis table ctx in
diff --git a/meta_deduce.ml b/meta_deduce.ml
index e49b569..2fa2b5e 100644
--- a/meta_deduce.ml
+++ b/meta_deduce.ml
@@ -217,6 +217,7 @@ let generate_mp prefix preds globals fmt (mp, tset) =
(match mp.mp_context with
| Weak_invariant -> "Weak invariant"
| Strong_invariant -> "Strong invariant"
+ | Conditional_invariant -> "Conditional invariant"
| Postcond -> "Postcond"
| Precond -> "Precond"
| Writing -> "Writing"
diff --git a/meta_dispatch.ml b/meta_dispatch.ml
index 020c04a..e1135ca 100644
--- a/meta_dispatch.ml
+++ b/meta_dispatch.ml
@@ -102,7 +102,7 @@ let unpack_mp flags mp admit =
let dispatch flags mps =
let all_mp = Hashtbl.create 10 in
let ctxts = [Weak_invariant; Strong_invariant; Writing; Reading; Calling;
- Precond; Postcond] in
+ Precond; Postcond; Conditional_invariant] in
let tables = List.map (fun ctx -> ctx, Str_Hashtbl.create 5) ctxts in
List.iter (fun mp ->
let table = List.assoc mp.mp_context tables in
diff --git a/meta_parse.ml b/meta_parse.ml
index f5688bb..3ec5060 100644
--- a/meta_parse.ml
+++ b/meta_parse.ml
@@ -34,6 +34,7 @@ type context =
| Reading
| Postcond
| Precond
+ | Conditional_invariant
type target =
| TgAll
@@ -76,7 +77,8 @@ let mp_contexts = [
"\\calling";
"\\reading";
"\\postcond";
- "\\precond"
+ "\\precond";
+ "\\conditional_invariant"
]
let mp_metavariables = [
"\\written";
@@ -387,6 +389,7 @@ let process_property tc loc = function
let mp_context = match econtext.lexpr_node with
| PLvar "\\weak_invariant" -> Weak_invariant
| PLvar "\\strong_invariant" -> Strong_invariant
+ | PLvar "\\conditional_invariant" -> Conditional_invariant
| PLvar "\\writing" -> Writing
| PLvar "\\reading" -> Reading
| PLvar "\\calling" -> Calling
diff --git a/meta_parse.mli b/meta_parse.mli
index cc62307..712af94 100644
--- a/meta_parse.mli
+++ b/meta_parse.mli
@@ -30,6 +30,7 @@ type context =
| Reading
| Postcond
| Precond
+ | Conditional_invariant
type target =
| TgAll
diff --git a/tests/meta-wp/invariant.c b/tests/meta-wp/invariant.c
index e3453c5..5ddbb68 100644
--- a/tests/meta-wp/invariant.c
+++ b/tests/meta-wp/invariant.c
@@ -4,7 +4,7 @@
#include <assert.h>
-unsigned A = 2;
+unsigned A = 2, B;
//@ assigns \nothing;
void requiresInv() {
@@ -14,9 +14,11 @@ void requiresInv() {
void breaksInv() {
A += 1;
}
+
//@ assigns \nothing;
void useless() {
}
+
//@ assigns A;
void maintainsInv() {
if(A < 42)
@@ -24,8 +26,17 @@ void maintainsInv() {
else A -= 4;
useless();
}
-//@ assigns A;
+
+//@ assigns B;
+void cond() {
+ if(B != 42){
+ B *= 2;
+ }
+}
+
+//@ assigns A, B;
void main() {
+ cond();
maintainsInv();
requiresInv();
@@ -50,7 +61,13 @@ void main() {
meta \prop,
\name("invariant_2"),
- \targets(\diff(\ALL, {main, useless})),
+ \targets(\diff(\ALL, {main, useless, cond})),
\context(\weak_invariant),
A % 2 == 0;
+
+ meta \prop,
+ \name(conditional),
+ \targets(cond),
+ \context(\conditional_invariant),
+ A == 42;
*/
--
GitLab