From 6fee7b885e5826b692bfeebb38e7a6c613bdb65d Mon Sep 17 00:00:00 2001
From: Kilyan Le Gallic <kilyan.legallic@cea.fr>
Date: Tue, 2 Jul 2024 17:16:05 +0200
Subject: [PATCH] [wp] Maps for CIL locations of logic type and logic info
---
src/plugins/wp/Why3Import.ml | 70 +++++++++++++++++++++---------------
1 file changed, 41 insertions(+), 29 deletions(-)
diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index a70361d4f77..d4b4eb33edc 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -121,7 +121,9 @@ type env = {
lenv : C.logic_info W.Term.Hls.t;
lils : W.Term.lsymbol Logic_info.Hashtbl.t;
ltits : W.Ty.tysymbol Logic_type_info.Hashtbl.t;
- menv : why3module Datatype.String.Hashtbl.t
+ menv : why3module Datatype.String.Hashtbl.t;
+ tloc : C.logic_type_info Location.Hashtbl.t;
+ lloc : C.logic_info Location.Hashtbl.t;
}
type menv = {
@@ -135,7 +137,9 @@ let create_empty_env wenv =
let lils = Logic_info.Hashtbl.create 0 in
let ltits = Logic_type_info.Hashtbl.create 0 in
let menv = Datatype.String.Hashtbl.create 0 in
- { wenv; tenv; lenv; lils; ltits; menv }
+ let tloc = Location.Hashtbl.create 0 in
+ let lloc = Location.Hashtbl.create 0 in
+ { wenv; tenv; lenv; lils; ltits; menv; tloc; lloc }
(* -------------------------------------------------------------------------- *)
@@ -166,34 +170,31 @@ let add_builtins env =
(* --- Location handling --- *)
(* -------------------------------------------------------------------------- *)
-let convert_location (wloc : Why3.Loc.position) : C.location =
- let (file,lstart,cstart,lend,cend) = Why3.Loc.get wloc in
- let pstart = {
- Filepath.pos_path = F.of_string file;
- pos_lnum = lstart;
- pos_bol = 0;
- pos_cnum = cstart;
- } in
- let pend = {
- Filepath.pos_path = F.of_string file;
- pos_lnum = lend;
- pos_bol = 0;
- pos_cnum = cend;
- } in (pstart, pend)
+let convert_location (wloc : Why3.Loc.position option) : C.location =
+ match wloc with
+ | Some loc ->
+ let (file,lstart,cstart,lend,cend) = Why3.Loc.get loc in
+ let pstart = {
+ Filepath.pos_path = F.of_string file;
+ pos_lnum = lstart;
+ pos_bol = 0;
+ pos_cnum = cstart;
+ } in
+ let pend = {
+ Filepath.pos_path = F.of_string file;
+ pos_lnum = lend;
+ pos_bol = 0;
+ pos_cnum = cend;
+ } in (pstart, pend)
+ | None ->
+ (Position.unknown, Position.unknown)
+
(* For debug use only *)
let pp_cil_loc fmt (id : W.Ident.ident) =
- match id.id_loc with
- | Some loc -> Cpp.pp_location fmt (convert_location loc)
- | None -> L.error "No location found"
+ Cpp.pp_location fmt @@ convert_location id.id_loc
+
-let pp_cil_loc_pos fmt (id : W.Ident.ident) =
- match id.id_loc with
- | Some loc ->
- let (ps,pe) = convert_location loc in
- Filepath.pp_pos fmt ps;
- Filepath.pp_pos fmt pe;
- | None -> L.error "No location found"
(* -------------------------------------------------------------------------- *)
(* --- Type conversion --- *)
@@ -232,6 +233,7 @@ and lti_of_ts (env : env) (menv : menv) (ts : W.Ty.tysymbol) : C.logic_type_info
}
in W.Ty.Hts.add env.tenv ts lti ;
menv.lti <- lti :: menv.lti;
+ Location.Hashtbl.add env.tloc (convert_location ts.ts_name.id_loc) lti;
Logic_type_info.Hashtbl.add env.ltits lti ts;
lti
@@ -267,7 +269,9 @@ let li_of_ls (env:env) (menv : menv) (ls : W.Term.lsymbol) : C.logic_info =
l_body = C.LBnone;
} in W.Term.Hls.add env.lenv ls li;
menv.li <- li :: menv.li;
- Logic_info.Hashtbl.add env.lils li ls; li
+ Location.Hashtbl.add env.lloc (convert_location ls.ls_name.id_loc) li;
+ Logic_info.Hashtbl.add env.lils li ls;
+ li
(* -------------------------------------------------------------------------- *)
(* --- Theory --- *)
@@ -357,15 +361,23 @@ let () =
pp_lti lti pp_tys ts;
L.result "Logic type info located at : %a" pp_id_loc ts.ts_name;
L.result "CIL Location will be %a" pp_cil_loc ts.ts_name;
- L.result "with positions %a" pp_cil_loc_pos ts.ts_name )
+ )
env.ltits;
Logic_info.Hashtbl.iter ( fun (li) (ls) ->
L.result "Logic info %a is associated to ls : %a "
pp_li li pp_ls ls;
L.result "Logic info located at : %a" pp_id_loc ls.ls_name;
L.result "CIL Location will be %a" pp_cil_loc ls.ls_name;
- L.result "with positions %a" pp_cil_loc_pos ls.ls_name )
+ )
env.lils;
+ Location.Hashtbl.iter ( fun (loc) (lti) ->
+ L.result "Logic info %a is associated to loc %a "
+ pp_lti lti Cpp.pp_location loc;
+ ) env.tloc;
+ Location.Hashtbl.iter ( fun (loc) (li) ->
+ L.result "Logic info %a is associated to loc %a "
+ pp_li li Cpp.pp_location loc;
+ ) env.lloc;
end
end
--
GitLab