From fc95fe10d14e372454791fc8c7d158d36c4c572b Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 25 Nov 2021 18:10:00 +0100
Subject: [PATCH] [logic] Fixes lv_type field of variables whose value is a
function
Fixes #1093
---
src/kernel_services/ast_queries/filecheck.ml | 7 ++++---
.../ast_queries/logic_const.ml | 5 +++++
.../ast_queries/logic_const.mli | 7 +++++++
.../ast_queries/logic_typing.ml | 19 ++++++-------------
tests/spec/local_lambda.i | 9 +++++++++
tests/spec/oracle/local_lambda.res.oracle | 13 +++++++++++++
6 files changed, 44 insertions(+), 16 deletions(-)
create mode 100644 tests/spec/local_lambda.i
create mode 100644 tests/spec/oracle/local_lambda.res.oracle
diff --git a/src/kernel_services/ast_queries/filecheck.ml b/src/kernel_services/ast_queries/filecheck.ml
index 397fad32079..18d9d1cab1c 100644
--- a/src/kernel_services/ast_queries/filecheck.ml
+++ b/src/kernel_services/ast_queries/filecheck.ml
@@ -815,16 +815,17 @@ module Base_checker = struct
| None ->
check_abort "Trying to use predicate %a as a term"
Printer.pp_logic_var lvi
- | Some typ ->
+ | Some rt ->
+ let ft = Logic_const.make_arrow_type li.l_profile rt in
if
not
- (Logic_utils.is_instance_of li.l_tparams t.term_type typ)
+ (Logic_utils.is_instance_of li.l_tparams t.term_type ft)
then
check_abort
"%a is declared with type %a. It cannot be used as \
a term of type %a"
Printer.pp_logic_var lvi
- Printer.pp_logic_type typ
+ Printer.pp_logic_type ft
Printer.pp_logic_type t.term_type)
with Not_found ->
check_abort
diff --git a/src/kernel_services/ast_queries/logic_const.ml b/src/kernel_services/ast_queries/logic_const.ml
index 28623b64f5e..b7b632bb888 100644
--- a/src/kernel_services/ast_queries/logic_const.ml
+++ b/src/kernel_services/ast_queries/logic_const.ml
@@ -226,6 +226,11 @@ let transform_element f t = set_conversion (plain_or_set f t) t
let is_plain_type ty = not (is_set_type ty)
+let make_arrow_type args rt =
+ match args with
+ | [] -> rt
+ | _ -> Larrow(List.map (fun x -> x.lv_type) args, rt)
+
let rec is_boolean_type = function
| Ltype ({ lt_name = s }, []) when s = Utf8_logic.boolean -> true
| Ltype (tdef,_) as ty when is_unrollable_ltdef tdef ->
diff --git a/src/kernel_services/ast_queries/logic_const.mli b/src/kernel_services/ast_queries/logic_const.mli
index db448d2e6de..a18c91e6b7e 100644
--- a/src/kernel_services/ast_queries/logic_const.mli
+++ b/src/kernel_services/ast_queries/logic_const.mli
@@ -283,6 +283,13 @@ val transform_element: (logic_type -> logic_type) -> logic_type -> logic_type
@modify 18.0-Argon expands the logic type definition if necessary. *)
val is_plain_type: logic_type -> bool
+(** [make_arrow_type args rt] returns a [rt] if [args] is empty or the
+ corresponding [Larrow] type.
+
+ @since Frama-C+dev
+*)
+val make_arrow_type: logic_var list -> logic_type -> logic_type
+
(** @return true if the argument is the boolean type.
@modify 18.0-Argon expands the logic type definition if necessary. *)
val is_boolean_type: logic_type -> bool
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index d7c956b7eb7..8950bee942e 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -2039,7 +2039,7 @@ struct
| _,typ ->
{ term with
term_node = Tlambda(quants, term);
- term_type = Larrow(List.map (fun x -> x.lv_type) quants,typ) }
+ term_type = make_arrow_type quants typ }
in
let rec aux known_vars kont term =
match term.term_node with
@@ -2948,7 +2948,7 @@ struct
| _ -> [],tdef
in
var.l_type <- Some tdef.term_type;
- var.l_var_info.lv_type <- tdef.term_type;
+ var.l_var_info.lv_type <- make_arrow_type args tdef.term_type;
var.l_profile <- args;
var.l_body <- LBterm tdef;
let env = Lenv.add_logic_info ident var env in
@@ -3455,10 +3455,8 @@ struct
in
let var = Cil_const.make_logic_info_local x in
var.l_profile <- args;
- var.l_var_info.lv_type <-
- (match typ with
- None -> Ctype (Cil.voidType)
- | Some t -> t);
+ let rt = Option.value typ ~default:(Ctype Cil.voidType) in
+ var.l_var_info.lv_type <- make_arrow_type args rt;
var.l_type <- typ;
var.l_body <- tdef;
let env = Lenv.add_logic_info x var env in
@@ -4003,13 +4001,8 @@ struct
- Polymorphism is not reflected on the lvar level.
- However, such lvar should rarely if at all be seen under a Tvar.
*)
- (match p,t with
- _,None -> ()
- | [], Some t ->
- info.l_var_info.lv_type <- t
- | _,Some t ->
- let typ = Larrow (List.map (fun x -> x.lv_type) p,t) in
- info.l_var_info.lv_type <- typ);
+ let rt = Option.value t ~default:(Ctype Cil.voidType) in
+ info.l_var_info.lv_type <- make_arrow_type p rt;
info.l_tparams <- poly;
info.l_profile <- p;
info.l_type <- t;
diff --git a/tests/spec/local_lambda.i b/tests/spec/local_lambda.i
new file mode 100644
index 00000000000..336c1721354
--- /dev/null
+++ b/tests/spec/local_lambda.i
@@ -0,0 +1,9 @@
+/*@ logic integer id(integer x) = x; */
+
+/*@ lemma test1: 55 == \sum(1,10,id); */
+
+/*@ lemma test2: 5 == \let x = (\lambda integer y; y); x(5); */
+
+/*@ lemma test3: 55 == \sum(1,10,\lambda integer y; y); */
+
+/*@ lemma test4: 55 == \let x = (\lambda integer y; y); \sum(1,10,x); */
diff --git a/tests/spec/oracle/local_lambda.res.oracle b/tests/spec/oracle/local_lambda.res.oracle
new file mode 100644
index 00000000000..d77e1eb63c2
--- /dev/null
+++ b/tests/spec/oracle/local_lambda.res.oracle
@@ -0,0 +1,13 @@
+[kernel] Parsing tests/spec/local_lambda.i (no preprocessing)
+/* Generated by Frama-C */
+/*@ logic ℤ id(ℤ x) = x;
+ */
+/*@ lemma test1: 55 ≡ \sum(1, 10, id);
+ */
+/*@ lemma test2: 5 ≡ (\let x = \lambda ℤ y; y; x(5));
+ */
+/*@ lemma test3: 55 ≡ \sum(1, 10, \lambda ℤ y; y);
+ */
+/*@ lemma test4: 55 ≡ (\let x = \lambda ℤ y; y; \sum(1, 10, x));
+ */
+
--
GitLab