From aae0b83584317ea1369cc46bc6de6bf54425ea56 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 9 Mar 2021 17:13:15 +0100
Subject: [PATCH] [eacsl] Update loop environment with variant information
---
src/plugins/e-acsl/src/code_generator/env.ml | 45 +++++++++++++++----
src/plugins/e-acsl/src/code_generator/env.mli | 7 ++-
2 files changed, 42 insertions(+), 10 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index d10a15f1587..24775347413 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -54,6 +54,11 @@ type local_env = {
rte: bool
}
+type loop_env = {
+ variant: (term * logic_info option) option;
+ invariants: toplevel_predicate list;
+}
+
type t = {
lscope: Lscope.t;
lscope_reset: bool;
@@ -67,8 +72,8 @@ type t = {
(* Stack of contracts for active functions and statements *)
var_mapping: Varinfo.t Stack.t Logic_var.Map.t;
(* records of C bindings for logic vars *)
- loop_invariants: toplevel_predicate list list;
- (* list of loop invariants for each currently visited loops *)
+ loop_envs: loop_env list;
+ (* list of loop environment for each currently visited loops *)
cpt: int;
(* counter used when generating variables *)
}
@@ -88,6 +93,9 @@ let empty_local_env =
mp_tbl = empty_mp_tbl;
rte = true }
+let empty_loop_env =
+ { variant = None;
+ invariants = [] }
let empty =
{ lscope = Lscope.empty;
lscope_reset = true;
@@ -97,7 +105,7 @@ let empty =
env_stack = [];
contract_stack = [];
var_mapping = Logic_var.Map.empty;
- loop_invariants = [];
+ loop_envs = [];
cpt = 0 }
let top env = match env.env_stack with
@@ -113,15 +121,36 @@ let has_no_new_stmt env =
(* ************************************************************************** *)
let push_loop env =
- { env with loop_invariants = [] :: env.loop_invariants }
+ { env with loop_envs = empty_loop_env :: env.loop_envs }
-let add_loop_invariant env inv = match env.loop_invariants with
+let top_loop_env env =
+ match env.loop_envs with
| [] -> assert false
- | invs :: tl -> { env with loop_invariants = (inv :: invs) :: tl }
+ | loop_env :: tl -> loop_env, tl
+
+let set_loop_variant ?measure env t =
+ let loop_env, tl = top_loop_env env in
+ let loop_env = { loop_env with variant = Some (t, measure) } in
+ { env with loop_envs = loop_env :: tl }
-let pop_loop env = match env.loop_invariants with
+let add_loop_invariant env inv =
+ match env.loop_envs with
| [] -> assert false
- | invs :: tl -> invs, { env with loop_invariants = tl }
+ | loop_env :: tl ->
+ let loop_env = { loop_env with invariants = inv :: loop_env.invariants} in
+ { env with loop_envs = loop_env :: tl }
+
+let top_loop_variant env =
+ let loop_env, _ = top_loop_env env in
+ loop_env.variant
+
+let top_loop_invariants env =
+ let loop_env, _ = top_loop_env env in
+ loop_env.invariants
+
+let pop_loop env =
+ let _, tl = top_loop_env env in
+ { env with loop_envs = tl }
(* ************************************************************************** *)
(** {2 RTEs} *)
diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli
index 8c8152b9718..3c521f8635e 100644
--- a/src/plugins/e-acsl/src/code_generator/env.mli
+++ b/src/plugins/e-acsl/src/code_generator/env.mli
@@ -153,12 +153,15 @@ val annotation_kind: t -> Smart_stmt.annotation_kind
val set_annotation_kind: t -> Smart_stmt.annotation_kind -> t
(* ************************************************************************** *)
-(** {2 Loop invariants} *)
+(** {2 Loop annotations} *)
(* ************************************************************************** *)
val push_loop: t -> t
+val set_loop_variant: ?measure:logic_info -> t -> term -> t
val add_loop_invariant: t -> toplevel_predicate -> t
-val pop_loop: t -> toplevel_predicate list * t
+val top_loop_variant: t -> (term * logic_info option) option
+val top_loop_invariants: t -> toplevel_predicate list
+val pop_loop: t -> t
(* ************************************************************************** *)
(** {2 RTEs} *)
--
GitLab