diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index 24757a156e653bb93fe74b912f6883e267902512..18a27559e31038fbfaf367c95f8abc073aeda672 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -80,6 +80,7 @@ module Correspondance =
type kf_correspondance =
[ kernel_function correspondance
| `Same_spec of kernel_function (** body has changed, but spec is identical *)
+ | `Different_calls of kernel_function
]
module Kf_correspondance =
@@ -97,15 +98,25 @@ module Kf_correspondance =
| `Same_spec f1, `Same_spec f2 -> Kernel_function.compare f1 f2
| `Same_spec _, _ -> 1
| _, `Same_spec _ -> -1
+ | `Different_calls f1, `Different_calls f2 -> Kernel_function.compare f1 f2
+ | `Different_calls _, _ -> 1
+ | _, `Different_calls _ -> -1
| (#correspondance as x), (#correspondance as y) -> C.compare x y
let equal = Datatype.from_compare
let hash = function
| `Same_spec f -> 57 * (Kernel_function.hash f)
+ | `Different_calls f -> 79 * (Kernel_function.hash f)
| #correspondance as x -> C.hash x
let internal_pretty_code p fmt = function
| `Same_spec f ->
let pp fmt =
- Format.fprintf fmt "`Same %a"
+ Format.fprintf fmt "`Same_spec %a"
+ (Kernel_function.internal_pretty_code Type.Call) f
+ in
+ Type.par p Call fmt pp
+ | `Different_calls f ->
+ let pp fmt =
+ Format.fprintf fmt "`Different_calls %a"
(Kernel_function.internal_pretty_code Type.Call) f
in
Type.par p Call fmt pp
@@ -113,6 +124,8 @@ module Kf_correspondance =
let pretty fmt = function
| `Same_spec f ->
Format.fprintf fmt "-> (contract) %a" Kernel_function.pretty f
+ | `Different_calls f ->
+ Format.fprintf fmt " -> (callees differ) %a" Kernel_function.pretty f
| #correspondance as x -> C.pretty fmt x
end)
@@ -154,3 +167,121 @@ module Kernel_function =
(Info(struct let name = "Ast_diff.Kernel_function" end))
module Fundec = Build(Cil_datatype.Fundec)
+
+(** TODO: use location info to detect potential renaming.
+ Requires some information about syntactic diff. *)
+let find_candidate_type ?loc:_loc ti =
+ if Globals.Types.mem_type Logic_typing.Typedef ti.tname then begin
+ match Globals.Types.global Logic_typing.Typedef ti.tname with
+ | GType(ti,_) -> Some ti
+ | g ->
+ Kernel.fatal
+ "Expected typeinfo instead of %a" Cil_datatype.Global.pretty g
+ end else None
+
+let find_candidate_compinfo ?loc:_loc ci =
+ let su = if ci.cstruct then Logic_typing.Struct else Logic_typing.Union in
+ if Globals.Types.mem_type su ci.cname then begin
+ match Globals.Types.global su ci.cname with
+ | GCompTag (ci,_) | GCompTagDecl(ci,_) -> Some ci
+ | g ->
+ Kernel.fatal
+ "Expected aggregate definition instead of %a"
+ Cil_datatype.Global.pretty g
+ end else None
+
+let find_candidate_enuminfo ?loc:_loc ei =
+ if Globals.Types.mem_type Logic_typing.Enum ei.ename then begin
+ match Globals.Types.global Logic_typing.Enum ei.ename with
+ | GEnumTag(ei,_) | GEnumTagDecl(ei,_) -> Some ei
+ | g ->
+ Kernel.fatal
+ "Expected enumeration definition instead of %a"
+ Cil_datatype.Global.pretty g
+ end else None
+
+let is_same_opt f o o' =
+ match o, o' with
+ | None, None -> true
+ | Some v, Some v' -> f v v'
+ | _ -> false
+
+let rec is_same_type t t' =
+ match t, t' with
+ | (TVoid _ | TInt _ | TFloat _ | TBuiltin_va_list _), _ ->
+ Cil_datatype.TypByName.equal t t'
+ | TPtr(t,a), TPtr(t',a') ->
+ is_same_type t t' && Cil_datatype.Attributes.equal a a'
+ | TArray(t,s,a), TArray(t',s',a') ->
+ is_same_type t t' && is_same_opt is_same_exp s s'
+ && Cil_datatype.Attributes.equal a a'
+ | TFun(rt,l,var,a), TFun(rt', l', var', a') ->
+ is_same_type rt rt' &&
+ is_same_opt (Logic_utils.is_same_list is_same_formal) l l' &&
+ var = var' &&
+ Cil_datatype.Attributes.equal a a'
+ | TNamed(t,a), TNamed(t',a') ->
+ let correspondance = typeinfo_correspondance t in
+ (match correspondance with
+ | `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 = compinfo_correspondance c in
+ (match correspondance with
+ | `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 = enuminfo_correspondance e in
+ (match correspondance with
+ | `Not_present -> false
+ | `Same e'' -> Cil_datatype.Enuminfo.equal e' e'') &&
+ Cil_datatype.Attributes.equal a a'
+ | (TPtr _ | TArray _ | TFun _ | TNamed _ | TComp _ | TEnum _), _ -> false
+
+and is_same_compinfo _ci _ci' = false
+
+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_exp _e _e' = false
+
+and typeinfo_correspondance ?loc ti =
+ let add ti =
+ match find_candidate_type ?loc ti with
+ | None -> `Not_present
+ | Some ti' ->
+ if is_same_type ti.ttype ti'.ttype then `Same ti' else `Not_present
+ in
+ Typeinfo.memo add ti
+
+and compinfo_correspondance ?loc ci =
+ let add ci =
+ match find_candidate_compinfo ?loc ci with
+ | None -> `Not_present
+ | Some ci' ->
+ if is_same_compinfo ci ci' then `Same ci' else `Not_present
+ in
+ Compinfo.memo add ci
+
+and enuminfo_correspondance ?loc ei =
+ let add ei =
+ match find_candidate_enuminfo ?loc ei with
+ | None -> `Not_present
+ | Some ei' ->
+ if is_same_enuminfo ei ei' then `Same ei' else `Not_present
+ in
+ Enuminfo.memo add ei
+
+let global_correspondance g =
+ match g with
+ | GType (ti,loc) -> ignore (typeinfo_correspondance ~loc ti)
+ | _ -> ()
+
+let compare_ast prj =
+ Orig_project.set prj;
+ let ast = Project.on prj Ast.get () in
+ Cil.iterGlobals ast global_correspondance
diff --git a/src/kernel_services/ast_queries/ast_diff.mli b/src/kernel_services/ast_queries/ast_diff.mli
index fe83242b179ab102af7a404f8418c0e4ee57a0c2..8aa926a5d3ab036f021c8d9faaf902a30003b79e 100644
--- a/src/kernel_services/ast_queries/ast_diff.mli
+++ b/src/kernel_services/ast_queries/ast_diff.mli
@@ -40,6 +40,8 @@ type 'a correspondance =
type kf_correspondance =
[ kernel_function correspondance
| `Same_spec of kernel_function (** body has changed, but spec is identical *)
+ | `Different_calls of kernel_function
+ (** body is identical, but there are calls to functions that have changed. *)
]
(** varinfos correspondances *)
@@ -94,3 +96,6 @@ module Kernel_function:
module Fundec:
State_builder.Hashtbl
with type key = fundec and type data = fundec correspondance
+
+(** [compare_ast prj] sets [prj] as the original project and fill the tables. *)
+val compare_ast: Project.t -> unit