[kernel] start comparing AST for filling correspondance tables

Mostly a mock-up at this point

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

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