From 59c7ec9ae11312b4abb27bf24c9b46d31948b733 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 10 Jan 2022 15:27:38 +0100
Subject: [PATCH] [kernel] diff-ast: do not propagate rec env when not needed
---
src/kernel_services/ast_queries/ast_diff.ml | 198 +++++++++-----------
1 file changed, 90 insertions(+), 108 deletions(-)
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index fd7fad581de..75c9ca2fa4b 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -182,7 +182,6 @@ module Info(I: sig val name: string end) =
types, and function (both C and ACSL). Other symbols must be
correctly ordered in a well-formed AST
*)
-[@@@ ocaml.warning "-69"] (* WIP: currently not all fields are used *)
type is_same_env =
{
compinfo: compinfo Cil_datatype.Compinfo.Map.t;
@@ -191,16 +190,9 @@ type is_same_env =
logic_type_info: logic_type_info Cil_datatype.Logic_type_info.Map.t;
}
-module Build(H:Datatype.S_with_collections)(D:Datatype.S) = struct
- include
- State_builder.Hashtbl(H.Hashtbl)(D)
- (Info(struct let name = "Ast_diff." ^ D.name end))
-
- let memo_env mk_val key env =
- if mem key then find key, env
- else let (data, _) as res = mk_val key env in
- add key data; res
-end
+module Build(H:Datatype.S_with_collections)(D:Datatype.S) =
+ State_builder.Hashtbl(H.Hashtbl)(D)
+ (Info(struct let name = "Ast_diff." ^ D.name end))
module Build_correspondance(H:Datatype.S_with_collections) =
Build(H)(Correspondance.Make(H))
@@ -287,98 +279,91 @@ let find_candidate_logic_type ?loc:_loc ti =
Some (Logic_env.find_logic_type ti.lt_name)
with Not_found -> None
-let (&&>) (res,env) f = if res then f env else false, env
-let (&&|) env f = f env
-let (&&&) (res,env) b = res && b, env
-
let is_same_opt f o o' env =
match o, o' with
- | None, None -> true, env
+ | None, None -> true
| Some v, Some v' -> f v v' env
- | _ -> false, env
+ | _ -> false
let rec is_same_list f l l' env =
match l, l' with
- | [], [] -> true, env
+ | [], [] -> true
| h::t, h'::t' ->
- env &&| f h h' &&> is_same_list f t t'
- | _ -> false, env
+ f h h' env && is_same_list f t t' env
+ | _ -> false
let rec is_same_type t t' env =
match t, t' with
| (TVoid _ | TInt _ | TFloat _ | TBuiltin_va_list _), _ ->
- Cil_datatype.TypByName.equal t t', env
+ Cil_datatype.TypByName.equal t t'
| TPtr(t,a), TPtr(t',a') ->
- env &&| is_same_type t t' &&& Cil_datatype.Attributes.equal a a'
+ is_same_type t t' env && Cil_datatype.Attributes.equal a a'
| TArray(t,s,a), TArray(t',s',a') ->
- env &&|
- is_same_type t t' &&>
- is_same_opt is_same_exp s s' &&&
+ is_same_type t t' env &&
+ is_same_opt is_same_exp s s' env &&
Cil_datatype.Attributes.equal a a'
| TFun(rt,l,var,a), TFun(rt', l', var', a') ->
- env &&|
- is_same_type rt rt' &&>
- is_same_opt (is_same_list is_same_formal) l l' &&&
- (var = var') &&&
+ is_same_type rt rt' env &&
+ is_same_opt (is_same_list is_same_formal) l l' env &&
+ (var = var') &&
Cil_datatype.Attributes.equal a a'
| TNamed(t,a), TNamed(t',a') ->
- let correspondance, env = typeinfo_correspondance t env in
+ let correspondance = typeinfo_correspondance t env in
(match correspondance with
- | `Not_present -> false, env
- | `Same t'' -> Cil_datatype.Typeinfo.equal t' t'',env) &&&
+ | `Not_present -> false
+ | `Same t'' -> Cil_datatype.Typeinfo.equal t' t'') &&
Cil_datatype.Attributes.equal a a'
| TComp(c,a), TComp(c', a') ->
- let correspondance, env = compinfo_correspondance c env in
+ let correspondance = compinfo_correspondance c env in
(match correspondance with
- | `Not_present -> false, env
- | `Same c'' -> Cil_datatype.Compinfo.equal c' c'', env) &&&
+ | `Not_present -> false
+ | `Same c'' -> Cil_datatype.Compinfo.equal c' c'') &&
Cil_datatype.Attributes.equal a a'
| TEnum(e,a), TEnum(e',a') ->
- let correspondance, env = enuminfo_correspondance e env in
+ let correspondance = enuminfo_correspondance e env in
(match correspondance with
- | `Not_present -> false, env
- | `Same e'' -> Cil_datatype.Enuminfo.equal e' e'', env) &&&
+ | `Not_present -> false
+ | `Same e'' -> Cil_datatype.Enuminfo.equal e' e'') &&
Cil_datatype.Attributes.equal a a'
- | (TPtr _ | TArray _ | TFun _ | TNamed _ | TComp _ | TEnum _), _ -> false, env
+ | (TPtr _ | TArray _ | TFun _ | TNamed _ | TComp _ | TEnum _), _ -> false
-and is_same_compinfo _ci _ci' env = false, env
+and is_same_compinfo _ci _ci' _env = false
-and is_same_enuminfo _ei _ei' env = false, env
+and is_same_enuminfo _ei _ei' _env = false
and is_same_formal (_,t,a) (_,t',a') env =
- is_same_type t t' env &&& Cil_datatype.Attributes.equal a a'
+ is_same_type t t' env && Cil_datatype.Attributes.equal a a'
and is_same_compound_init (o,i) (o',i') env =
- is_same_offset o o' env &&> is_same_init i i'
+ is_same_offset o o' env && is_same_init i i' env
and is_same_init i i' env =
match i, i' with
| SingleInit e, SingleInit e' -> is_same_exp e e' env
| CompoundInit (t,l), CompoundInit (t', l') ->
- is_same_type t t' env &&>
- (is_same_list is_same_compound_init) l l'
- | (SingleInit _ | CompoundInit _), _ -> false, env
+ is_same_type t t' env &&
+ (is_same_list is_same_compound_init) l l' env
+ | (SingleInit _ | CompoundInit _), _ -> false
-and is_same_initinfo i i' = is_same_opt is_same_init i.init i'.init
+and is_same_initinfo i i' env = is_same_opt is_same_init i.init i'.init env
-and is_same_exp _e _e' env = false, env
+and is_same_exp _e _e' _env = false
-and is_same_offset _o _o' env = false, env
+and is_same_offset _o _o' _env = false
-and is_same_funspec _s _s' env = false, env
+and is_same_funspec _s _s' _env = false
-and is_same_fundec _f _f' env: body_correspondance*is_same_env =
- `Body_changed, env
+and is_same_fundec _f _f' _env: body_correspondance = `Body_changed
-and is_same_logic_type _t _t' env = false, env
+and is_same_logic_type _t _t' _env = false
-and is_same_logic_param _lv _lv' env = false, env
+and is_same_logic_param _lv _lv' _env = false
-and is_same_logic_info _li _li' env = false, env
+and is_same_logic_info _li _li' _env = false
-and is_same_logic_type_info _ti _ti' env = false, env
+and is_same_logic_type_info _ti _ti' _env = false
-and is_same_model_info _mi _mi' env = false, env
+and is_same_model_info _mi _mi' _env = false
(* because of overloading, we have to check for a corresponding profile,
leading to potentially recursive calls to is_same_* functions. *)
@@ -390,20 +375,18 @@ and find_candidate_logic_info ?loc:_loc li env =
let rec extract l =
match l with
| [] -> None
- | li' :: tl ->
- let (res,_) = find_one li' in
- if res then Some li' else extract tl
+ | li' :: tl -> if find_one li' then Some li' else extract tl
in
match extract candidates with
| None -> None
| Some li' ->
- let (res,_) = is_same_opt is_same_logic_type li.l_type li'.l_type env in
+ let res = is_same_opt is_same_logic_type li.l_type li'.l_type env in
if res then Some li' else None
and find_candidate_model_info ?loc:_loc mi env =
let candidates = Logic_env.find_all_model_fields mi.mi_name in
let find_one mi' =
- fst (is_same_type mi.mi_base_type mi'.mi_base_type env)
+ is_same_type mi.mi_base_type mi'.mi_base_type env
in
let rec aux = function
| [] -> None
@@ -412,39 +395,38 @@ and find_candidate_model_info ?loc:_loc mi env =
aux candidates
and typeinfo_correspondance ?loc ti env =
- let add ti env =
+ let add ti =
match find_candidate_type ?loc ti with
- | None -> `Not_present, env
+ | None -> `Not_present
| Some ti' ->
- let res, env = is_same_type ti.ttype ti'.ttype env in
- (if res then `Same ti' else `Not_present), env
+ let res = is_same_type ti.ttype ti'.ttype env in
+ if res then `Same ti' else `Not_present
in
- Typeinfo.memo_env add ti env
+ Typeinfo.memo add ti
and compinfo_correspondance ?loc ci env =
- let add ci env =
+ let add ci =
match find_candidate_compinfo ?loc ci with
- | None -> `Not_present, env
+ | None -> `Not_present
| Some ci' ->
- let env =
+ let env' =
{env with compinfo = Cil_datatype.Compinfo.Map.add ci ci' env.compinfo}
in
- let res, env = is_same_compinfo ci ci' env in
- (if res then `Same ci' else `Not_present), env
+ let res = is_same_compinfo ci ci' env' in
+ if res then `Same ci' else `Not_present
in
match Cil_datatype.Compinfo.Map.find_opt ci env.compinfo with
- | Some ci' -> `Same ci', env
- | None -> Compinfo.memo_env add ci env
+ | Some ci' -> `Same ci'
+ | None -> Compinfo.memo add ci
and enuminfo_correspondance ?loc ei env =
- let add ei env =
+ let add ei =
match find_candidate_enuminfo ?loc ei with
- | None -> `Not_present, env
+ | None -> `Not_present
| Some ei' ->
- let res, env = is_same_enuminfo ei ei' env in
- (if res then `Same ei' else `Not_present),env
+ if is_same_enuminfo ei ei' env then `Same ei' else `Not_present
in
- Enuminfo.memo_env add ei env
+ Enuminfo.memo add ei
and gfun_correspondance ?loc vi env =
let selection =
@@ -458,64 +440,64 @@ and gfun_correspondance ?loc vi env =
let kf =
Project.on ~selection (Orig_project.get()) Globals.Functions.get vi
in
- let add kf env =
+ let add kf =
match find_candidate_func ?loc kf with
- | None -> `Not_present, env
+ | None -> `Not_present
| Some kf' ->
- let env =
+ let env' =
{ env with kernel_function = Kf.Map.add kf kf' env.kernel_function }
in
- let same_spec, env = is_same_funspec kf.spec kf'.spec env in
- let same_body, env =
+ let same_spec = is_same_funspec kf.spec kf'.spec env' in
+ let same_body =
match (Kf.has_definition kf, Kf.has_definition kf') with
- | false, false -> `Same_body, env
- | false, true | true, false -> `Body_changed, env
+ | false, false -> `Same_body
+ | false, true | true, false -> `Body_changed
| true, true ->
- is_same_fundec (Kf.get_definition kf) (Kf.get_definition kf') env
+ is_same_fundec (Kf.get_definition kf) (Kf.get_definition kf') env'
in
match same_spec, same_body with
- | false, `Body_changed -> `Not_present, env
- | false, `Callees_changed -> `Partial(kf',`Callees_spec_changed), env
- | false, `Same_body -> `Partial(kf', `Spec_changed), env
- | true, `Same_body -> `Same kf', env
- | true, ((`Body_changed|`Callees_changed) as c) -> `Partial(kf', c), env
+ | false, `Body_changed -> `Not_present
+ | false, `Callees_changed -> `Partial(kf',`Callees_spec_changed)
+ | false, `Same_body -> `Partial(kf', `Spec_changed)
+ | true, `Same_body -> `Same kf'
+ | true, ((`Body_changed|`Callees_changed) as c) -> `Partial(kf', c)
in
match Kf.Map.find_opt kf env.kernel_function with
- | Some kf' -> `Same kf', env
- | None -> Kernel_function.memo_env add kf env
+ | Some kf' -> `Same kf'
+ | None -> Kernel_function.memo add kf
and logic_info_correspondance ?loc li env =
- let add li env =
+ let add li =
match find_candidate_logic_info ?loc li env with
- | None -> `Not_present, env
+ | None -> `Not_present
| Some li' ->
let env =
{ env with
logic_info = Cil_datatype.Logic_info.Map.add li li' env.logic_info }
in
- let res, env = is_same_logic_info li li' env in
- (if res then `Same li' else `Not_present), env
+ let res = is_same_logic_info li li' env in
+ if res then `Same li' else `Not_present
in
match Cil_datatype.Logic_info.Map.find_opt li env.logic_info with
- | Some li' -> `Same li', env
- | None -> Logic_info.memo_env add li env
+ | Some li' -> `Same li'
+ | None -> Logic_info.memo add li
and logic_type_correspondance ?loc ti env =
- let add ti env =
+ let add ti =
match find_candidate_logic_type ?loc ti with
- | None -> `Not_present, env
+ | None -> `Not_present
| Some ti' ->
let env =
{ env with
logic_type_info =
Cil_datatype.Logic_type_info.Map.add ti ti' env.logic_type_info }
in
- let res, env = is_same_logic_type_info ti ti' env in
- (if res then `Same ti' else `Not_present), env
+ let res = is_same_logic_type_info ti ti' env in
+ if res then `Same ti' else `Not_present
in
match Cil_datatype.Logic_type_info.Map.find_opt ti env.logic_type_info with
- | Some ti' -> `Same ti', env
- | None -> Logic_type_info.memo_env add ti env
+ | Some ti' -> `Same ti'
+ | None -> Logic_type_info.memo add ti
let gvar_correspondance ?loc vi =
let add vi =
@@ -527,7 +509,7 @@ let gvar_correspondance ?loc vi =
Project.on ~selection (Orig_project.get()) Globals.Vars.find vi
in
let init' = Globals.Vars.find vi' in
- let res,_ = is_same_initinfo init init' empty_env in
+ let res = is_same_initinfo init init' empty_env in
if res then `Same vi' else `Not_present
in
Varinfo.memo add vi
@@ -537,7 +519,7 @@ let model_info_correspondance ?loc mi =
match find_candidate_model_info ?loc mi empty_env with
| None -> `Not_present
| Some mi' ->
- let res,_ = is_same_model_info mi mi' empty_env in
+ let res = is_same_model_info mi mi' empty_env in
if res then `Same mi' else `Not_present
in
Model_info.memo add mi
--
GitLab