From a02389a85941738d6d3cc179d8371f8780aff297 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 6 Jan 2022 15:18:24 +0100
Subject: [PATCH] [kernel] ast-diff: correspondance between global vars
modulo implementation of correspondance between expressions
---
src/kernel_services/ast_queries/ast_diff.ml | 40 +++++++++++++++++++++
1 file changed, 40 insertions(+)
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index 18a27559e31..965b33c100e 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -200,6 +200,11 @@ let find_candidate_enuminfo ?loc:_loc ei =
Cil_datatype.Global.pretty g
end else None
+let find_candidate_varinfo ?loc:_loc vi where =
+ try
+ Some (Globals.Vars.find_from_astinfo vi.vname where)
+ with Not_found -> None
+
let is_same_opt f o o' =
match o, o' with
| None, None -> true
@@ -247,8 +252,23 @@ and is_same_enuminfo _ei _ei' = false
and is_same_formal (_,t,a) (_,t',a') =
is_same_type t t' && Cil_datatype.Attributes.equal a a'
+and is_same_compound_init (o,i) (o',i') =
+ is_same_offset o o' && is_same_init i i'
+
+and is_same_init i i' =
+ match i, i' with
+ | SingleInit e, SingleInit e' -> is_same_exp e e'
+ | CompoundInit (t,l), CompoundInit (t', l') ->
+ is_same_type t t' &&
+ Logic_utils.is_same_list is_same_compound_init l l'
+ | (SingleInit _ | CompoundInit _), _ -> false
+
+and is_same_initinfo i i' = is_same_opt is_same_init i.init i'.init
+
and is_same_exp _e _e' = false
+and is_same_offset _o _o' = false
+
and typeinfo_correspondance ?loc ti =
let add ti =
match find_candidate_type ?loc ti with
@@ -276,9 +296,29 @@ and enuminfo_correspondance ?loc ei =
in
Enuminfo.memo add ei
+let gvar_correspondance ?loc vi =
+ let add vi =
+ match find_candidate_varinfo ?loc vi Cil_types.VGlobal with
+ | None -> `Not_present
+ | Some vi' ->
+ let selection = State_selection.singleton Globals.Vars.self in
+ let init =
+ Project.on ~selection (Orig_project.get()) Globals.Vars.find vi
+ in
+ let init' = Globals.Vars.find vi' in
+ if is_same_initinfo init init' then `Same vi' else `Not_present
+ in
+ Varinfo.memo add vi
+
let global_correspondance g =
match g with
| GType (ti,loc) -> ignore (typeinfo_correspondance ~loc ti)
+ | GCompTag(ci,loc) | GCompTagDecl(ci,loc) ->
+ ignore (compinfo_correspondance ~loc ci)
+ | GEnumTag(ei,loc) | GEnumTagDecl(ei,loc) ->
+ ignore (enuminfo_correspondance ~loc ei)
+ | GVar(vi,_,loc) | GVarDecl(vi,loc) ->
+ ignore (gvar_correspondance ~loc vi)
| _ -> ()
let compare_ast prj =
--
GitLab