From cb18c4834d0da5d76d03245732cba44c623109e6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 23 Apr 2024 14:50:02 +0200
Subject: [PATCH] [kernel/logic] type & logic symbol compilation
---
.../ast_queries/logic_typing.ml | 147 +++++++++---------
tests/spec/oracle/module.res.oracle | 33 +++-
tests/spec/oracle/reset_env.res.oracle | 2 +-
3 files changed, 106 insertions(+), 76 deletions(-)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index d8223092d56..466937fa3ac 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -686,46 +686,57 @@ struct
(* Imported Scope *)
- let scopes = Stack.create ()
- let imported = ref []
+ type scope = {
+ long_prefix: string; (* last '::' included *)
+ short_prefix: string; (* last '::' included *)
+ }
+
+ let pp_scope fmt s =
+ Format.fprintf fmt "{ long: %S; short: %S }"
+ s.long_prefix s.short_prefix
+ [@@ warning "-32"]
+
+ let scopes : scope list Stack.t = Stack.create ()
+ let imported : scope list ref = ref []
- let pushScope m p =
- let prefix m = m ^ "::" in
- imported := (prefix m, Option.map prefix p) :: !imported
+ let open_scope ~name ?alias () =
+ let short = match alias with Some a -> a | None ->
+ List.hd @@ List.rev @@ String.split_on_char ':' name
+ in imported := {
+ long_prefix = name ^ "::";
+ short_prefix = short ^ "::";
+ } :: !imported
let clear_imports () = Stack.clear scopes ; imported := []
let push_imports () = Stack.push !imported scopes
let pop_imports () = imported := Stack.pop scopes
- let add_import ?alias mid =
+ let add_import ?alias name =
match alias with
- | Some _ -> pushScope mid alias
+ | Some _ -> open_scope ~name ?alias ()
| None ->
begin
- match List.rev @@ String.split_on_char ':' mid with
- | m::_ -> pushScope mid (Some m)
- | [] -> ()
- end ;
- pushScope mid None
+ match List.rev @@ String.split_on_char ':' name with
+ | alias::_ -> open_scope ~name ~alias ()
+ | [] -> open_scope ~name ()
+ end
let find_import find a =
- match find a with
- | Some _ as r -> r
- | None ->
- let size = List.length @@ String.split_on_char ':' a in
- if size > 3 then None else
- let pmatch = function
- | None -> size = 1
- | Some prefix -> size = 3 && String.starts_with ~prefix a in
- let rec lookup = function
- | [] -> None
- | (m,p)::scopes ->
- if pmatch p then
- match find (m ^ a) with
- | None -> lookup scopes
- | Some _ as r -> r
- else lookup scopes
- in lookup !imported
+ let xs = String.split_on_char ':' a in
+ let n = List.length xs in
+ if n = 1 then (* unqualified name *)
+ match List.find_map (fun s -> find (s.long_prefix ^ a)) !imported with
+ | Some _ as result -> result
+ | None -> find a
+ else
+ if n = 3 then (* single module qualified name *)
+ let is_short s = String.starts_with ~prefix:s.short_prefix a in
+ match List.find_opt is_short !imported with
+ | Some s ->
+ let x = List.hd @@ List.rev xs in
+ find (s.long_prefix ^ x)
+ | None -> find a
+ else (* long qualified name *) find a
let resolve_ltype =
find_import
@@ -2546,8 +2557,9 @@ struct
let locs = List.rev_map (make_set_conversion convert_ptr) locs in
locs,typ
and lfun_app ctxt env loc f labels ttl =
- try
- let info = Logic_env.find_logic_ctor f in
+ match resolve_lapp f env with
+ | None -> C.error loc "unbound logic function %s" f
+ | Some (Ctor info) ->
if labels <> [] then begin
if ctxt.silent then raise Backtrack;
ctxt.error loc
@@ -2555,18 +2567,13 @@ struct
It cannot have logic labels" f;
end;
let params = List.map fresh info.ctor_params in
- let env, tl =
- type_arguments ~overloaded:false env loc params ttl
- in
- let t = Ltype(info.ctor_type,
- List.map fresh_type_var
- info.ctor_type.lt_params)
- in
- let t = instantiate env t in
+ let env, tl = type_arguments ~overloaded:false env loc params ttl in
+ let alphas = List.map fresh_type_var info.ctor_type.lt_params in
+ let t = instantiate env @@ Ltype(info.ctor_type,alphas) in
TDataCons(info,tl), t
- with Not_found ->
+ | Some (Lfun infos) ->
let info, label_assoc, tl, t =
- type_logic_app env loc f labels ttl
+ type_logic_app_infos env loc f infos labels ttl
in
match t with
| None ->
@@ -3252,26 +3259,26 @@ struct
| TAddrOf lv
| Tat ({term_node = TAddrOf lv}, _) ->
f lv t
- | _ -> C.error t.term_loc "not a dependency value: %a"
- Cil_printer.pp_term t
+ | _ ->
+ C.error t.term_loc "not a dependency value: %a" Cil_printer.pp_term t
in
lift_set check_from t
and type_logic_app env loc f labels ttl =
- (* support for overloading *)
- let infos =
- try [Lenv.find_logic_info f env]
- with Not_found ->
- Logic_env.find_all_logic_functions f in
+ match resolve_lapp f env with
+ | Some (Lfun infos) -> type_logic_app_infos env loc f infos labels ttl
+ | Some (Ctor info) ->
+ C.error loc "not a predicate: constructor %s" info.ctor_name
+ | None ->
+ C.error loc "unbound logic predicate %s" f
+
+ and type_logic_app_infos env loc f (infos : logic_info list) labels ttl =
match infos with
- | [] -> C.error loc "unbound logic function %s" f
| [info] ->
begin
let labels = List.map (find_logic_label loc env) labels in
let params = List.map (fun x -> fresh x.lv_type) info.l_profile in
- let env, tl =
- type_arguments ~overloaded:false env loc params ttl
- in
+ let env, tl = type_arguments ~overloaded:false env loc params ttl in
let label_assoc = labels_assoc loc f env info.l_labels labels in
match info.l_type with
| Some t ->
@@ -3289,26 +3296,19 @@ struct
try
let labels = List.map (find_logic_label loc env) labels in
let params =
- List.map (fun x -> fresh x.lv_type) info.l_profile
- in
+ List.map (fun x -> fresh x.lv_type) info.l_profile in
let env, tl =
- type_arguments ~overloaded:true env loc params ttl
- in
- let tl =
- List.combine (List.map (instantiate env) params) tl
- in
- let label_assoc = labels_assoc loc f env info.l_labels labels
- in
+ type_arguments ~overloaded:true env loc params ttl in
+ let tl = List.combine (List.map (instantiate env) params) tl in
+ let label_assoc = labels_assoc loc f env info.l_labels labels in
match info.l_type with
| Some t ->
let t = fresh t in
let t =
try instantiate env t
with _ -> raise Not_applicable
- in
- (info, label_assoc, tl, Some t)::acc
- | None ->
- (info, label_assoc, tl, None)::acc
+ in (info, label_assoc, tl, Some t)::acc
+ | None -> (info, label_assoc, tl, None)::acc
with Not_applicable -> acc)
[] infos
in
@@ -3454,7 +3454,7 @@ struct
prel ~loc (Cil_types.Req, t, Cil.lzero ~loc ())
| p -> pnot ~loc p)
| PLapp (p, labels, tl) ->
- let ttl= List.map (term env) tl in
+ let ttl = List.map (term env) tl in
let info, label_assoc, tl, t = type_logic_app env loc p labels ttl in
begin
match t with
@@ -4261,24 +4261,29 @@ struct
C.error loc
"Duplicated module %s (first occurrence at %a)"
id Cil_printer.pp_location oldloc in
+ push_imports () ;
+ open_scope ~name () ;
let l = List.filter_map (decl ~context) decls in
+ pop_imports () ;
ignore (Logic_env.Modules.memo ~change (fun _ -> loc) name);
Some (Dmodule(name,l,[],loc))
- | LDimport _ -> C.error loc "Unsupported module import"
+ | LDimport(name,alias) ->
+ open_scope ~name ?alias () ; None
- | LDtype(s,l,def) ->
+ | LDtype(name,l,def) ->
let env = init_type_variables loc l in
+ let name = fullname ~context name in
let my_info =
- { lt_name = s;
+ { lt_name = name;
lt_params = l;
lt_def = None; (* will be updated later *)
lt_attr = [];
} in
add_logic_type loc my_info;
let tdef = Option.map (typedef loc ~context env my_info) def in
- if is_cyclic_typedef s tdef then
- C.error loc "Definition of %s is cyclic" s;
+ if is_cyclic_typedef name tdef then
+ C.error loc "Definition of %s is cyclic" name;
my_info.lt_def <- tdef;
Some (Dtype (my_info,loc))
diff --git a/tests/spec/oracle/module.res.oracle b/tests/spec/oracle/module.res.oracle
index 8d4f1a4394e..a90c44df4d2 100644
--- a/tests/spec/oracle/module.res.oracle
+++ b/tests/spec/oracle/module.res.oracle
@@ -1,5 +1,30 @@
[kernel] Parsing module.i (no preprocessing)
-[kernel:annot-error] module.i:8: Warning:
- Unsupported module import. Ignoring global annotation
-[kernel] User Error: warning annot-error treated as fatal error.
-[kernel] Frama-C aborted: invalid user input.
+/* Generated by Frama-C */
+/*@
+module foo::Bar {
+ type foo::Bar::t;
+
+ logic foo::Bar::t foo::Bar::e;
+
+ logic foo::Bar::t foo::Bar::op(foo::Bar::t x, foo::Bar::t y) ;
+
+ logic foo::Bar::t foo::Bar::opN(foo::Bar::t x, ℤ n) =
+ n ≥ 0? foo::Bar::op(x, foo::Bar::opN(x, n - 1)): foo::Bar::e;
+
+ }
+ */
+/*@
+module foo::Jazz {
+ logic foo::Bar::t foo::Jazz::inv(foo::Bar::t x) ;
+
+ logic foo::Bar::t foo::Jazz::opN(foo::Bar::t x, ℤ n) =
+ n ≥ 0? foo::Bar::opN(x, n): foo::Bar::opN(foo::Jazz::inv(x), -n);
+
+ }
+ */
+/*@
+lemma AbsOp:
+ ∀ foo::Bar::t x, ℤ n;
+ foo::Jazz::opN(x, \abs(n)) ≡ foo::Bar::opN(x, \abs(n));
+ */
+
diff --git a/tests/spec/oracle/reset_env.res.oracle b/tests/spec/oracle/reset_env.res.oracle
index 3b1ae6dc368..36dafa0e430 100644
--- a/tests/spec/oracle/reset_env.res.oracle
+++ b/tests/spec/oracle/reset_env.res.oracle
@@ -2,6 +2,6 @@
[kernel:annot-error] reset_env.i:5: Warning:
unbound logic variable INEXISTENT_SYMBOL. Ignoring global annotation
[kernel:annot-error] reset_env.i:9: Warning:
- unbound logic function bla. Ignoring specification of function f
+ unbound logic predicate bla. Ignoring specification of function f
/* Generated by Frama-C */
--
GitLab