ast_diff.ml

(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2022                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

open Cil_types

module Orig_project =
  State_builder.Option_ref(Project.Datatype)(
  struct
    let name = "Ast_diff.OrigProject"
    let dependencies = []
  end)

type 'a correspondance =
  [ `Same of 'a (** symbol with identical definition has been found. *)
  | `Not_present (** no correspondance *)
  ]

module Correspondance_input =
struct
  type 'a t = 'a correspondance
  let name a = Type.name a ^ " correspondance"
  let module_name = "Correspondance"
  let structural_descr _ = Structural_descr.t_abstract
  let reprs x = [ `Not_present; `Same x]
  let mk_equal eq x y =
    match x,y with
    | `Same x, `Same y -> eq x y
    | `Not_present, `Not_present -> true
    | `Same _, `Not_present
    | `Not_present, `Same _ -> false
  let mk_compare cmp x y =
    match x,y with
    | `Not_present, `Not_present -> 0
    | `Not_present, `Same _ -> -1
    | `Same x, `Same y -> cmp x y
    | `Same _, `Not_present -> 1
  let mk_hash h = function
    | `Same x -> 117 * h x
    | `Not_present -> 43
  let map f = function
    | `Same x -> `Same (f x)
    | `Not_present -> `Not_present
  let mk_internal_pretty_code pp prec fmt = function
    | `Not_present -> Format.pp_print_string fmt "`Not_present"
    | `Same x ->
      let pp fmt = Format.fprintf fmt "`Same %a" (pp Type.Call) x in
      Type.par prec Call fmt pp
  let mk_pretty pp fmt = function
    | `Not_present -> Format.pp_print_string fmt "N/A"
    | `Same x -> Format.fprintf fmt " => %a" pp x
  let mk_varname v = function
    | `Not_present -> "x"
    | `Same x -> v x ^ "_c"
  let mk_mem_project mem query = function
    | `Not_present -> false
    | `Same x -> mem query x
end

module Correspondance = Datatype.Polymorphic(Correspondance_input)

(* for kernel function, we are a bit more precise than a yes/no answer.
   More precisely, we check whether a function has the same spec,
   the same body, and whether its callees have changed (provided
   the body itself is identical, otherwise, there's no point in checking
   the callees.
*)
type partial_correspondance =
  [ `Spec_changed (* body and callees haven't changed *)
  | `Body_changed (* spec hasn't changed *)
  | `Callees_changed (* spec and body haven't changed *)
  | `Callees_spec_changed (* body hasn't changed *)
  ]

type body_correspondance =
  [ `Body_changed
  | `Callees_changed
  | `Same_body
  ]

let (<=>) res (cmp,x,y) = if res <> 0 then res else cmp x y

let compare_pc pc1 pc2 =
  match pc1, pc2 with
  | `Spec_changed, `Spec_changed -> 0
  | `Spec_changed, _ -> -1
  | _, `Spec_changed -> 1
  | `Body_changed, `Body_changed -> 0
  | `Body_changed, _ -> -1
  | _, `Body_changed -> 1
  | `Callees_changed, `Callees_changed -> 0
  | `Callees_changed, _ -> -1
  | _, `Callees_changed -> 1
  | `Callees_spec_changed, `Callees_spec_changed -> 0

let string_of_pc = function
  | `Spec_changed -> "Spec_changed"
  | `Body_changed -> "Body_changed"
  | `Callees_changed -> "Callees_changed"
  | `Callees_spec_changed -> "Callees_spec_changed"

let pretty_pc fmt =
  let open Format in
  function
  | `Spec_changed -> pp_print_string fmt "(spec changed)"
  | `Body_changed -> pp_print_string fmt "(body changed)"
  | `Callees_changed -> pp_print_string fmt "(callees changed)"
  | `Callees_spec_changed -> pp_print_string fmt "(callees and spec changed)"

type 'a code_correspondance =
  [ 'a correspondance
  | `Partial of 'a * partial_correspondance
  ]

module Code_correspondance_input =
struct
  type 'a t = 'a code_correspondance
  let name a = Type.name a ^ " code_correspondance"
  let module_name = "Code_correspondance"
  let structural_descr _ = Structural_descr.t_abstract
  let reprs = Correspondance_input.reprs
  let mk_equal eq x y =
    match x,y with
    | `Partial(x,pc), `Partial(x',pc') -> eq x x' && (compare_pc pc pc' = 0)
    | `Partial _, _ | _, `Partial _ -> false
    | (#correspondance as c), (#correspondance as c') ->
      Correspondance_input.mk_equal eq c c'

  let mk_compare cmp x y =
    match x,y with
    | `Partial(x,pc), `Partial(x',pc') ->
      cmp x x' <=> (compare_pc,pc,pc')
    | `Partial _, `Same _ -> -1
    | `Same _, `Partial _ -> 1
    | `Partial _, `Not_present -> 1
    | `Not_present, `Partial _ -> -1
    | (#correspondance as c), (#correspondance as c') ->
      Correspondance_input.mk_compare cmp c c'

  let mk_hash hash = function
    | `Partial (x,_) -> 57 * hash x
    | #correspondance as x -> Correspondance_input.mk_hash hash x

  let map f = function
    | `Partial(x,pc) -> `Partial(f x,pc)
    | (#correspondance as x) -> Correspondance_input.map f x

  let mk_internal_pretty_code pp prec fmt = function
    | `Partial (x,flags) ->
      let pp fmt =
        Format.fprintf fmt "`Partial (%a,%s)"
          (pp Type.Call) x (string_of_pc flags)
      in
      Type.par prec Call fmt pp
    | #correspondance as x ->
      Correspondance_input.mk_internal_pretty_code pp prec fmt x

  let mk_pretty pp fmt = function
    | `Partial(x,flags) ->
      Format.fprintf fmt "-> %a %a" pp x pretty_pc flags
    | #correspondance as x -> Correspondance_input.mk_pretty pp fmt x

  let mk_varname f = function
    | `Partial (x,_) -> f x ^ "_pc"
    | #correspondance as x -> Correspondance_input.mk_varname f x

  let mk_mem_project f p = function
    | `Partial (x,_) -> f p x
    | #correspondance as x -> Correspondance_input.mk_mem_project f p x
end

module Code_correspondance = Datatype.Polymorphic(Code_correspondance_input)

module Info(I: sig val name: string end) =
  (struct
    let name = "Ast_diff." ^ I.name
    let dependencies = [ Ast.self; Orig_project.self ]
    let size = 43
  end)

(* Map of symbols under analysis, in case of recursion.
   Note that this can only happen with aggregate types, logic
   types, and function (both C and ACSL). Other symbols must be
   correctly ordered in a well-formed AST
*)
type is_same_env =
  {
    compinfo: compinfo Cil_datatype.Compinfo.Map.t;
    kernel_function: kernel_function Kernel_function.Map.t;
    local_vars: varinfo Cil_datatype.Varinfo.Map.t;
    logic_info: logic_info Cil_datatype.Logic_info.Map.t;
    logic_type_info: logic_type_info Cil_datatype.Logic_type_info.Map.t;
    logic_local_vars: logic_var Cil_datatype.Logic_var.Map.t;
    logic_type_vars: string Datatype.String.Map.t;
    (* goto targets pairs are checked afterwards, so that forward gotos
       do not interrupt the linear visit.
       We thus collect them in the environment.
    *)
    goto_targets: (stmt * stmt) list;
  }

module type Correspondance_table = sig
  include State_builder.Hashtbl
  val pretty_data: Format.formatter -> data -> unit
end

module Build(H:Datatype.S_with_collections)(D:Datatype.S):
  Correspondance_table with type key = H.t and type data = D.t =
struct
  include
    State_builder.Hashtbl(H.Hashtbl)(D)
      (Info(struct let name = "Ast_diff." ^ D.name end))
  let pretty_data = D.pretty
end

module Build_correspondance(H:Datatype.S_with_collections) =
  Build(H)(Correspondance.Make(H))

module Build_code_correspondance(H:Datatype.S_with_collections) =
  Build(H)(Code_correspondance.Make(H))

module Varinfo = Build_correspondance(Cil_datatype.Varinfo)

module Compinfo = Build_correspondance(Cil_datatype.Compinfo)

module Enuminfo = Build_correspondance(Cil_datatype.Enuminfo)

module Enumitem = Build_correspondance(Cil_datatype.Enumitem)

module Typeinfo = Build_correspondance(Cil_datatype.Typeinfo)

module Stmt = Build_code_correspondance(Cil_datatype.Stmt)

module Logic_info = Build_correspondance(Cil_datatype.Logic_info)

module Logic_type_info = Build_correspondance(Cil_datatype.Logic_type_info)

module Logic_ctor_info = Build_correspondance(Cil_datatype.Logic_ctor_info)

module Fieldinfo = Build_correspondance(Cil_datatype.Fieldinfo)

module Model_info = Build_correspondance(Cil_datatype.Model_info)

module Logic_var = Build_correspondance(Cil_datatype.Logic_var)

module Kf = Kernel_function

module Kernel_function = Build_code_correspondance(Kernel_function)

module Fundec = Build_correspondance(Cil_datatype.Fundec)

let make_correspondance candidate has_same_spec code_corres =
  match has_same_spec, code_corres with
  | false, `Body_changed -> `Not_present
  | false, `Callees_changed ->
    `Partial(candidate,`Callees_spec_changed)
  | false, `Same_body ->
    `Partial(candidate, `Spec_changed)
  | true, `Same_body ->
    `Same candidate
  | true, ((`Body_changed|`Callees_changed) as c) ->
    `Partial(candidate, c)

let (&&>) (res,env) f =
  match res with
  | `Body_changed -> `Body_changed, env
  | `Same_body -> f env
  | `Callees_changed ->
    let res', env = f env in
    match res' with
    | `Body_changed -> `Body_changed, env
    | `Same_body | `Callees_changed -> `Callees_changed, env

let (&&&) (res, env) f = if res then f env else false, env

let empty_env =
  { compinfo = Cil_datatype.Compinfo.Map.empty;
    kernel_function = Kf.Map.empty;
    local_vars = Cil_datatype.Varinfo.Map.empty;
    logic_info = Cil_datatype.Logic_info.Map.empty;
    logic_type_info = Cil_datatype.Logic_type_info.Map.empty;
    logic_local_vars = Cil_datatype.Logic_var.Map.empty;
    logic_type_vars = Datatype.String.Map.empty;
    goto_targets = []
  }

let add_locals f f' env =
  let add_one env v v' =
    { env with local_vars = Cil_datatype.Varinfo.Map.add v v' env.local_vars }
  in
  List.fold_left2 add_one env f f'

(* local static variables are in fact global. As soon as we have determined
   that they have a correspondance, we add them to the global bindings *)
let add_statics l l' =
  let add_one v v' = Varinfo.add v (`Same v') in
  List.iter2 add_one l l'

let add_logic_vars p p' env =
  let add_one env lv lv' =
    { env with
      logic_local_vars =
        Cil_datatype.Logic_var.Map.add lv lv' env.logic_local_vars }
  in
  List.fold_left2 add_one env p p'

let add_logic_info v v' env =
  { env with logic_info = Cil_datatype.Logic_info.Map.add v v' env.logic_info }

let logic_type_vars_env l l' env =
  if List.length l = List.length l' then begin
    let logic_type_vars =
      List.fold_left2 (fun env s s' -> Datatype.String.Map.add s s' env)
        env.logic_type_vars l l'
    in
    true, { env with logic_type_vars }
  end else false, env

let formals_correspondance f f' =
  let add_one v v' = Varinfo.add v (`Same v') in
  List.iter2 add_one f f'

let logic_prms_correspondance p p' =
  let add_one lv lv' =
    Logic_var.add lv (`Same lv') in
  List.iter2 add_one p p'

(** 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.find_type su ci.cname with
    | TComp(ci', _) -> Some ci'
    | t ->
      Kernel.fatal
        "Expected compinfo instead of %a"
        Printer.pp_typ t
  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.find_type Logic_typing.Enum ei.ename with
    | TEnum(ei,_) -> Some ei
    | t ->
      Kernel.fatal
        "Expected enuminfo instead of %a"
        Printer.pp_typ t
  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 find_candidate_func ?loc:_loc kf =
  try
    Some (Globals.Functions.find_by_name (Kf.get_name kf))
  with Not_found -> None

let find_candidate_logic_type ?loc:_loc ti =
  try
    Some (Logic_env.find_logic_type ti.lt_name)
  with Not_found -> None

let is_same_opt f o o' env =
  match o, o' with
  | None, None -> true
  | Some v, Some v' -> f v v' env
  | _ -> false

let is_same_opt_env f o o' env =
  match o, o' with
  | None, None -> true, env
  | Some v, Some v' -> f v v' env
  | _ -> false, env

let is_same_pair f1 f2 (x1,x2) (y1,y2) env = f1 x1 y1 env && f2 x2 y2 env

let rec is_same_list f l l' env =
  match l, l' with
  | [], [] -> true
  | h::t, h'::t' -> f h h' env && is_same_list f t t' env
  | _ -> false

let rec is_same_list_env f l l' env =
  match l, l' with
  | [], [] -> true, env
  | h::t, h'::t' -> f h h' env &&& is_same_list_env f t t'
  | _ -> false, env

let get_original_kf vi =
  let selection = State_selection.of_list
      [Kernel_function.self; Annotations.funspec_state; Globals.Functions.self]
  in
  Project.on ~selection (Orig_project.get()) Globals.Functions.get vi

let check_goto_targets env =
  let check_one (s,s') =
    match Stmt.find s with
    | `Not_present -> false
    | `Same s'' | `Partial (s'',_) ->
      (* From the goto point of view, what matters is that the targets
         themselves have a correspondance. If they're e.g. calls to a
         function that has itself changed, or blocks whose content has
         changed, it has already been detected when comparing the targets,
         and will be dealt with accordingly as the fundec level. *)
      Cil_datatype.Stmt.equal s' s''
    | exception Not_found -> false
  in
  if List.for_all check_one env.goto_targets then `Same_body, env
  else `Body_changed, env

let is_matching_fieldinfo fi fi' =
  match Fieldinfo.find fi with
  | `Not_present -> false
  | `Same fi'' -> Cil_datatype.Fieldinfo.equal fi' fi''
  | exception Not_found ->
    Kernel.fatal "Unbound field %a in AST diff"
      Cil_datatype.Fieldinfo.pretty fi

let is_matching_model_info mf mf' =
  match Model_info.find mf with
  | `Not_present -> false
  | `Same mf'' -> Cil_datatype.Model_info.equal mf' mf''
  | exception Not_found ->
    Kernel.fatal "Unbound model field %a in AST diff"
      Cil_datatype.Model_info.pretty  mf

let is_matching_logic_type_var a a' env =
  match Datatype.String.Map.find_opt a env.logic_type_vars with
  | None -> false
  | Some a'' -> Datatype.String.equal a' a''

module Unop = struct
  type t = [%import: Cil_types.unop] [@@deriving eq]
end

module Binop = struct
  type t = [%import: Cil_types.binop] [@@deriving eq]
end

module Ikind = struct
  type t = [%import: Cil_types.ikind] [@@deriving eq]
end

module Fkind = struct
  type t = [%import: Cil_types.fkind] [@@deriving eq]
end

module Predicate_kind = struct
  type t = [%import: Cil_types.predicate_kind] [@@deriving eq]
end

module Logic_builtin_label = struct
  type t = [%import: Cil_types.logic_builtin_label] [@@deriving eq]
end

module Relation = struct
  type t = [%import: Cil_types.relation] [@@deriving eq]
end

module Termination_kind = struct
  type t = [%import: Cil_types.termination_kind] [@@deriving eq]
end

let is_same_behavior_set l l' =
  Datatype.String.Set.(equal (of_list l) (of_list l'))

let are_same_cd_clauses l l' =
  let module StringSetSet = Set.Make(Datatype.String.Set) in
  let of_list l =
    StringSetSet.of_list (List.map Datatype.String.Set.of_list l)
  in
  StringSetSet.equal (of_list l) (of_list l')

let is_same_logic_label l l' _env =
  match l, l' with
  | StmtLabel s, StmtLabel s' ->
    (match Stmt.find !s with
     | `Not_present -> false
     | `Same s'' | `Partial(s'',_) ->
       Cil_datatype.Stmt.equal !s' s''
     | exception Not_found -> false)
  | FormalLabel s, FormalLabel s' -> Datatype.String.equal s s'
  | BuiltinLabel l, BuiltinLabel l' -> Logic_builtin_label.equal l l'
  | (StmtLabel _ | FormalLabel _ | BuiltinLabel _), _ -> false

let rec is_same_predicate p p' env =
  (* names are semantically irrelevant. *)
  is_same_predicate_node p.pred_content p'.pred_content env

and is_same_predicate_node p p' env =
  match p, p' with
  | Pfalse, Pfalse -> true
  | Ptrue, Ptrue -> true
  | Papp(p,labs,args), Papp(p',labs',args') ->
    is_matching_logic_info p p' env &&
    is_same_list is_same_logic_label labs labs' env &&
    is_same_list is_same_term args args' env
  | Pseparated t, Pseparated t' -> is_same_list is_same_term t t' env
  | Prel (r,t1,t2), Prel(r',t1',t2') ->
    Relation.equal r r' && is_same_term t1 t1' env && is_same_term t2 t2' env
  | Pand(p1,p2), Pand(p1',p2')
  | Por(p1,p2), Por(p1',p2')
  | Pxor(p1,p2), Pxor(p1',p2')
  | Pimplies(p1,p2), Pimplies(p1',p2')
  | Piff(p1,p2), Piff(p1',p2') ->
    is_same_predicate p1 p1' env && is_same_predicate p2 p2' env
  | Pnot p, Pnot p' -> is_same_predicate p p' env
  | Pif(t,p1,p2), Pif(t',p1',p2') ->
    is_same_term t t' env &&
    is_same_predicate p1 p1' env &&
    is_same_predicate p2 p2' env
  | Plet(v,p), Plet(v',p') ->
    if is_same_logic_info v v' env then begin
      let env = add_logic_info v v' env in
      let env = add_logic_vars [v.l_var_info] [v'.l_var_info] env in
      is_same_predicate p p' env
    end else false
  | Pforall(q,p), Pforall(q',p')
  | Pexists(q,p), Pexists(q',p') ->
    if is_same_list is_same_logic_var q q' env then begin
      let env = add_logic_vars q q' env in
      is_same_predicate p p' env
    end else false
  | Pat(p,l), Pat(p',l') ->
    is_same_predicate p p' env && is_same_logic_label l l' env
  | Pobject_pointer(l,t), Pobject_pointer(l',t')
  | Pvalid_read(l,t), Pvalid_read(l',t')
  | Pvalid(l,t), Pvalid(l',t')
  | Pinitialized(l,t), Pinitialized(l',t')
  | Pdangling(l,t), Pdangling(l',t')
  | Pallocable(l,t), Pallocable(l',t')
  | Pfreeable(l,t), Pfreeable(l',t') ->
    is_same_logic_label l l' env && is_same_term t t' env
  | Pfresh(l1,l2,p,s), Pfresh(l1',l2',p',s') ->
    is_same_logic_label l1 l1' env &&
    is_same_logic_label l2 l2' env &&
    is_same_term p p' env &&
    is_same_term s s' env
  | Pvalid_function(t), Pvalid_function(t') -> is_same_term t t' env
  | (Pfalse | Ptrue | Papp _ | Pseparated _ | Prel _ | Pand _ | Por _ | Pxor _
    | Pimplies _ | Piff _ | Pnot _ | Pif _ | Plet _ | Pforall _ | Pexists _
    | Pat _ | Pobject_pointer _ | Pvalid_read _ | Pvalid _ | Pinitialized _
    | Pdangling _ | Pallocable _ | Pfreeable _ | Pfresh _
    | Pvalid_function _), _ -> false

and is_same_logic_constant c c' env =
  match c,c' with
  | LEnum ei, LEnum ei' ->
    (match enumitem_correspondance ei env with
     | `Same ei'' -> Cil_datatype.Enumitem.equal ei' ei''
     | `Not_present -> false)
  | LEnum _, _ | _, LEnum _ -> false
  | (Integer _ | LStr _ | LWStr _ | LChr _ | LReal _), _ ->
    Cil_datatype.Logic_constant.equal c c'

and is_same_term t t' env =
  is_same_term_node t.term_node t'.term_node env

and is_same_term_node t t' env =
  match t,t' with
  | TConst c, TConst c' -> is_same_logic_constant c c' env
  | TLval lv, TLval lv' -> is_same_term_lval lv lv' env
  | TSizeOf t, TSizeOf t'
  | TAlignOf t, TAlignOf t' -> is_same_type t t' env
  | TSizeOfE t, TSizeOfE t'
  | TAlignOfE t, TAlignOfE t' -> is_same_term t t' env
  | TSizeOfStr s, TSizeOfStr s' -> String.length s = String.length s'
  | TUnOp(op,t), TUnOp(op',t') -> Unop.equal op op' && is_same_term t t' env
  | TBinOp(op,t1,t2), TBinOp(op',t1',t2') ->
    Binop.equal op op' && is_same_term t1 t1' env && is_same_term t2 t2' env
  | TCastE(typ,term), TCastE(typ',term') ->
    is_same_type typ typ' env && is_same_term term term' env
  | TAddrOf lv, TAddrOf lv'
  | TStartOf lv, TStartOf lv' -> is_same_term_lval lv lv' env
  | Tapp(f,labs,args), Tapp(f',labs',args') ->
    is_matching_logic_info f f' env &&
    is_same_list is_same_logic_label labs labs' env &&
    is_same_list is_same_term args args' env
  | Tlambda(q,t), Tlambda(q',t') ->
    if is_same_list is_same_logic_var q q' env then begin
      let env = add_logic_vars q q' env in
      is_same_term t t' env
    end else false
  | TDataCons(c,args), TDataCons(c',args') ->
    is_matching_logic_ctor c c' env &&
    is_same_list is_same_term args args' env
  | Tif(c,t1,t2), Tif(c',t1',t2') ->
    is_same_term c c' env &&
    is_same_term t1 t1' env &&
    is_same_term t2 t2' env
  | Tat(t,l), Tat(t',l') ->
    is_same_term t t' env && is_same_logic_label l l' env
  | Tbase_addr(l,t), Tbase_addr(l',t')
  | Toffset(l,t), Toffset(l',t')
  | Tblock_length(l,t), Tblock_length(l',t') ->
    is_same_logic_label l l' env && is_same_term t t' env
  | Tnull, Tnull -> true
  | TLogic_coerce(typ,t), TLogic_coerce(typ',t') ->
    is_same_logic_type typ typ' env && is_same_term t t' env
  | TUpdate(a,o,v), TUpdate(a',o',v') ->
    is_same_term a a' env &&
    is_same_term_offset o o' env &&
    is_same_term v v' env
  | Ttypeof t, Ttypeof t' -> is_same_term t t' env
  | Ttype t, Ttype t' -> is_same_type t t' env
  | Tempty_set, Tempty_set -> true
  | Tunion l, Tunion l'
  | Tinter l, Tinter l' -> is_same_list is_same_term l l' env
  | Tcomprehension(t,q,p), Tcomprehension(t',q',p') ->
    if is_same_list is_same_logic_var q q' env then begin
      let env = add_logic_vars q q' env in
      is_same_term t t' env && is_same_opt is_same_predicate p p' env
    end else false
  | Trange(l,u), Trange(l',u') ->
    is_same_opt is_same_term l l' env && is_same_opt is_same_term u u' env
  | Tlet(v,t), Tlet(v',t') ->
    if is_same_logic_info v v' env then begin
      let env = add_logic_info v v' env in
      let env = add_logic_vars [v.l_var_info] [v'.l_var_info] env in
      is_same_term t t' env
    end else false
  | (TConst _ | TLval _ | TSizeOf _ | TSizeOfE _ | TSizeOfStr _ | TAlignOf _
    | TAlignOfE _ |  TUnOp _ | TBinOp _ | TCastE _ | TAddrOf _ | TStartOf _
    | Tapp _ | Tlambda _ | TDataCons _ | Tif _ | Tat _ | Tbase_addr _
    | Toffset _ | Tblock_length _ | Tnull | TLogic_coerce _ | TUpdate _
    | Ttypeof _ | Ttype _ | Tempty_set | Tunion _ | Tinter _ | Tcomprehension _
    | Tlet _ | Trange _), _ -> false

and is_same_term_lval (lh,lo) (lh',lo') env =
  is_same_term_lhost lh lh' env && is_same_term_offset lo lo' env

and is_same_term_lhost lh lh' env =
  match lh, lh' with
  | TVar lv, TVar lv' -> is_matching_logic_var lv lv' env
  | TResult _, TResult _ -> true
  | TMem p, TMem p' -> is_same_term p p' env
  | (TVar _ | TResult _ | TMem _), _ -> false

and is_matching_logic_var lv lv' env =
  match lv.lv_origin, lv'.lv_origin with
  | Some vi, Some vi' -> is_matching_varinfo vi vi' env
  | None, None ->
    (match Cil_datatype.Logic_var.Map.find_opt lv env.logic_local_vars with
     | Some lv'' -> Cil_datatype.Logic_var.equal lv' lv''
     | None ->
       (match Logic_var.find lv with
        | `Not_present -> false
        | `Same lv'' -> Cil_datatype.Logic_var.equal lv' lv''
        | exception Not_found ->
          if lv.lv_name = "\\exit_status" && lv'.lv_name = "\\exit_status"
          then begin Logic_var.add lv (`Same lv'); true end
          else begin
            match logic_var_correspondance lv env with
            | None -> false
            | Some lv'' -> Cil_datatype.Logic_var.equal lv' lv''
          end))
  | _ -> false

and logic_var_correspondance lv env =
  match find_candidate_logic_var lv env with
  | None -> None
  | Some lv' -> Logic_var.add lv (`Same lv'); Some lv'

and is_same_term_offset lo lo' env =
  match lo, lo' with
  | TNoOffset, TNoOffset -> true
  | TField(f,o), TField(f',o') ->
    is_matching_fieldinfo f f' && is_same_term_offset o o' env
  | TModel(f,o), TModel(f',o') ->
    is_matching_model_info f f' && is_same_term_offset o o' env
  | TIndex(i,o), TIndex(i',o') ->
    is_same_term i i' env && is_same_term_offset o o' env
  | (TNoOffset | TField _ | TModel _ | TIndex _), _ -> false

and is_same_toplevel_predicate p p' env =
  Predicate_kind.equal p.tp_kind p'.tp_kind &&
  is_same_predicate p.tp_statement p'.tp_statement env

and is_same_identified_predicate p p' env =
  is_same_toplevel_predicate p.ip_content p'.ip_content env

and is_same_identified_term t t' env =
  is_same_term t.it_content t'.it_content env

and is_same_post_cond (k,p) (k',p') env =
  Termination_kind.equal k k' && is_same_identified_predicate p p' env

and is_same_deps d d' env =
  match d,d' with
  | FromAny, FromAny -> true
  | From l, From l' -> is_same_list is_same_identified_term l l' env
  | (FromAny | From _), _ -> false

and is_same_from (t,f) (t',f') env =
  is_same_identified_term t t' env && is_same_deps f f' env

and is_same_assigns a a' env =
  match a,a' with
  | WritesAny, WritesAny -> true
  | Writes l, Writes l' -> is_same_list is_same_from l l' env
  | (WritesAny | Writes _), _ -> false

and is_same_allocation a a' env =
  match a,a' with
  | FreeAllocAny, FreeAllocAny -> true
  | FreeAlloc(f,a), FreeAlloc(f',a') ->
    is_same_list is_same_identified_term f f' env &&
    is_same_list is_same_identified_term a a' env
  | (FreeAllocAny | FreeAlloc _),_ -> false

and is_same_behavior b b' env =
  is_same_list is_same_identified_predicate b.b_requires b'.b_requires env &&
  is_same_list is_same_identified_predicate b.b_assumes b'.b_assumes env &&
  is_same_list is_same_post_cond b.b_post_cond b'.b_post_cond env &&
  is_same_assigns b.b_assigns b'.b_assigns env &&
  is_same_allocation b.b_allocation b'.b_allocation env
(* TODO: also consider ACSL extensions, with the help of the plugins
   that handle them. *)

and is_same_variant (v,m) (v',m') env =
  is_same_term v v' env && is_same_opt is_matching_logic_info m m' env

and is_same_loop_pragma p p' env =
  match p, p' with
  | Unroll_specs l, Unroll_specs l'
  | Widen_hints l, Widen_hints l'
  | Widen_variables l, Widen_variables l' ->
    is_same_list is_same_term l l' env
  | (Unroll_specs _ | Widen_hints _ | Widen_variables _), _ -> false

and is_same_slice_pragma p p' env =
  match p, p' with
  | SPexpr t, SPexpr t' -> is_same_term t t' env
  | SPctrl, SPctrl -> true
  | SPstmt, SPstmt -> true
  | (SPexpr _ | SPctrl | SPstmt), _ -> false

and is_same_impact_pragma p p' env =
  match p, p' with
  | IPexpr t, IPexpr t' -> is_same_term t t' env
  | IPstmt, IPstmt -> true
  | (IPexpr _ | IPstmt), _ -> false

and is_same_pragma p p' env =
  match p,p' with
  | Loop_pragma p, Loop_pragma p' -> is_same_loop_pragma p p' env
  | Slice_pragma p, Slice_pragma p' -> is_same_slice_pragma p p' env
  | Impact_pragma p, Impact_pragma p' -> is_same_impact_pragma p p' env
  | (Loop_pragma _ | Slice_pragma _ | Impact_pragma _), _ -> false

and are_same_behaviors bhvs bhvs' env =
  let treat_one_behavior acc b =
    match List.partition (fun b' -> b.b_name = b'.b_name) acc with
    | [], _ -> raise Exit
    | [b'], acc ->
      if is_same_behavior b b' env then acc else raise Exit
    | _ ->
      Kernel.fatal "found several behaviors with the same name %s" b.b_name
  in
  try
    match List.fold_left treat_one_behavior bhvs' bhvs with
    | [] -> true
    | _ -> (* new behaviors appeared: spec has changed. *) false
  with Exit -> false

and is_same_funspec s s' env =
  are_same_behaviors s.spec_behavior s'.spec_behavior env &&
  is_same_opt is_same_variant s.spec_variant s'.spec_variant env &&
  is_same_opt is_same_identified_predicate
    s.spec_terminates s'.spec_terminates env &&
  are_same_cd_clauses s.spec_complete_behaviors s'.spec_complete_behaviors &&
  are_same_cd_clauses s.spec_disjoint_behaviors s'.spec_disjoint_behaviors

and is_same_code_annotation a a' env =
  match a.annot_content, a'.annot_content with
  | AAssert (bhvs, p), AAssert(bhvs',p') ->
    is_same_behavior_set bhvs bhvs' && is_same_toplevel_predicate p p' env
  | AStmtSpec (bhvs, s), AStmtSpec(bhvs', s') ->
    is_same_behavior_set bhvs bhvs' && is_same_funspec s s' env
  | AInvariant (bhvs, is_loop, p), AInvariant(bhvs', is_loop', p') ->
    is_same_behavior_set bhvs bhvs' && is_loop = is_loop' &&
    is_same_toplevel_predicate p p' env
  | AVariant v, AVariant v' -> is_same_variant v v' env
  | AAssigns(bhvs, a), AAssigns(bhvs', a') ->
    is_same_behavior_set bhvs bhvs' && is_same_assigns a a' env
  | AAllocation(bhvs, a), AAllocation(bhvs',a') ->
    is_same_behavior_set bhvs bhvs' && is_same_allocation a a' env
  | APragma p, APragma p' -> is_same_pragma p p' env
  | AExtended _, AExtended _ -> true (*TODO: checks also for extended clauses*)
  | (AAssert _ | AStmtSpec _ | AInvariant _ | AVariant _ | AAssigns _
    | AAllocation _ | APragma _ | AExtended _), _ -> false

and is_same_logic_type t t' env =
  match t,t' with
  | Ctype t, Ctype t' -> is_same_type t t' env
  | Ltype (t,prms), Ltype (t',prms') ->
    is_matching_logic_type_info t t' env &&
    is_same_list is_same_logic_type prms prms' env
  | Lvar s, Lvar s' -> is_matching_logic_type_var s s' env
  | Linteger, Linteger -> true
  | Lreal, Lreal -> true
  | Larrow(args,rt), Larrow(args', rt')  ->
    is_same_list is_same_logic_type args args' env &&
    is_same_logic_type rt rt' env
  | (Ctype _ | Ltype _ | Lvar _ | Linteger | Lreal | Larrow _),_ -> false

and is_same_inductive_case (_,labs,tprms,p) (_,labs',tprms',p') env =
  let res, env =
    (is_same_list is_same_logic_label labs labs' env, env) &&&
    logic_type_vars_env tprms tprms'
  in
  res && is_same_predicate p p' env

and is_same_logic_body b b' env =
  match b,b' with
  | LBnone, LBnone -> true
  | LBreads l, LBreads l' ->
    is_same_list is_same_identified_term l l' env
  | LBterm t, LBterm t' -> is_same_term t t' env
  | LBpred p, LBpred p' -> is_same_predicate p p' env
  | LBinductive l, LBinductive l' ->
    is_same_list is_same_inductive_case l l' env
  | (LBnone | LBreads _ | LBterm _ | LBpred _ | LBinductive _), _ -> false

and is_same_logic_ctor_info c c' env =
  (* we rely on order in the type declaration to match constructors,
     not on names. *)
  is_same_list is_same_logic_type c.ctor_params c'.ctor_params env

and is_same_logic_type_def d d' env =
  match d,d' with
  | LTsum l, LTsum l' ->
    if is_same_list is_same_logic_ctor_info l l' env then begin
      List.iter2 (fun c c' -> Logic_ctor_info.add c (`Same c')) l l';
      true
    end else begin
      List.iter (fun c -> Logic_ctor_info.add c `Not_present) l;
      false
    end
  | LTsyn t, LTsyn t' -> is_same_logic_type t t' env
  | (LTsum _ | LTsyn _), _ -> false

and is_same_logic_info li li' env =
  let res,env =
    (is_same_list is_same_logic_label li.l_labels li'.l_labels env, env) &&&
    logic_type_vars_env li.l_tparams li'.l_tparams &&&
    logic_vars_env li.l_profile li'.l_profile
  in
  res && is_same_opt is_same_logic_type li.l_type li'.l_type env &&
  is_same_logic_body li.l_body li'.l_body env

and is_same_logic_type_info ti ti' env =
  let res,env =
    (Cil_datatype.Attributes.equal ti.lt_attr ti'.lt_attr, env) &&&
    logic_type_vars_env ti.lt_params ti'.lt_params
  in
  res && is_same_opt is_same_logic_type_def ti.lt_def ti'.lt_def env

and is_same_model_info mi mi' env =
  is_same_type mi.mi_base_type mi'.mi_base_type env &&
  is_same_logic_type mi.mi_field_type mi'.mi_field_type env &&
  Cil_datatype.Attributes.equal mi.mi_attr mi'.mi_attr

and is_same_type t t' env =
  match t, t' with
  | TVoid a, TVoid a' -> Cil_datatype.Attributes.equal a a'
  | TInt (ik,a), TInt(ik',a') ->
    Ikind.equal ik ik' && Cil_datatype.Attributes.equal a a'
  | TFloat (fk,a), TFloat(fk', a') ->
    Fkind.equal fk fk' && Cil_datatype.Attributes.equal a a'
  | TBuiltin_va_list a, TBuiltin_va_list a' ->
    Cil_datatype.Attributes.equal a a'
  | TPtr(t,a), TPtr(t',a') ->
    is_same_type t t' env && Cil_datatype.Attributes.equal a a'
  | TArray(t,s,a), TArray(t',s',a') ->
    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') ->
    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 = typeinfo_correspondance t env 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 env 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 env in
    (match correspondance with
     | `Not_present -> false
     | `Same e'' -> Cil_datatype.Enuminfo.equal e' e'') &&
    Cil_datatype.Attributes.equal a a'
  | (TVoid _ | TInt _ | TFloat _ | TBuiltin_va_list _ | TPtr _ | TArray _
    | TFun _ | TNamed _ | TComp _ | TEnum _), _ -> false

and is_same_compinfo ci ci' env =
  ci.cstruct = ci'.cstruct &&
  Cil_datatype.Attributes.equal ci.cattr ci'.cattr &&
  is_same_opt (is_same_list is_same_fieldinfo) ci.cfields ci'.cfields env

and is_same_enuminfo ei ei' env =
  Cil_datatype.Attributes.equal ei.eattr ei'.eattr &&
  Ikind.equal ei.ekind ei'.ekind &&
  is_same_list is_same_enumitem ei.eitems ei'.eitems env

and is_same_fieldinfo fi fi' env =
  (* we don't compare names: it's the order in which they appear in the
     definition of the aggregate that counts. *)
  fi.forder = fi'.forder &&
  is_same_type fi.ftype fi'.ftype env &&
  is_same_opt (fun x y _ -> x = y) fi.fbitfield fi'.fbitfield env &&
  Cil_datatype.Attributes.equal fi.fattr fi'.fattr

and is_same_enumitem ei ei' env = is_same_exp ei.eival ei'.eival env

and is_same_formal (_,t,a) (_,t',a') env =
  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' 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' env
  | (SingleInit _ | CompoundInit _), _ -> false

and is_same_initinfo i i' env = is_same_opt is_same_init i.init i'.init env

and is_same_local_init i i' env =
  match i, i' with
  | AssignInit i, AssignInit i' ->
    if is_same_init i i' env then `Same_body
    else `Body_changed
  | (ConsInit(c,args,Plain_func), ConsInit(c',args',Plain_func))
  | (ConsInit(c,args,Constructor),ConsInit(c',args',Constructor))  ->
    if is_same_varinfo c c' env &&
       is_same_list is_same_exp args args' env
    then begin
      match gfun_correspondance c env with
      | `Partial _ | `Not_present -> `Callees_changed
      | `Same _ -> `Same_body
    end else `Body_changed
  | (AssignInit _| ConsInit _), _ -> `Body_changed

and is_same_constant c c' env =
  match c,c' with
  | CEnum ei, CEnum ei' ->
    (match enumitem_correspondance ei env with
     | `Same ei'' -> Cil_datatype.Enumitem.equal ei' ei''
     | `Not_present -> false)
  | CEnum _, _ | _, CEnum _ -> false
  | (CInt64 _ | CStr _ | CWStr _ | CChr _ | CReal _), _ ->
    Cil_datatype.Constant.equal c c'

and is_same_exp e e' env =
  match e.enode, e'.enode with
  | Const c, Const c' -> is_same_constant c c' env
  | Lval lv, Lval lv' -> is_same_lval lv lv' env