CompareCIL (p.goblint.2.6.0.doc.goblint.incremental.CompareCIL)

include module type of struct include CompareAST end

include module type of struct include CompareCFG end

include module type of struct include CompareAST end

Sourcemodule StringMap = CompareCFG.StringMap

Sourcetype method_rename_assumptions = GoblintCil.varinfo CilMaps.VarinfoMap.t

Sourcetype glob_var_rename_assumptions = GoblintCil.varinfo CilMaps.VarinfoMap.t

type renamesOnSuccess =
  (GoblintCil.compinfo * GoblintCil.compinfo) list
  * (GoblintCil.enuminfo * GoblintCil.enuminfo) list

Source

type rename_mapping =
  string StringMap.t
  * method_rename_assumptions
  * glob_var_rename_assumptions
  * renamesOnSuccess

Source

val rename_mapping_aware_name_comparison : 
  string ->
  string ->
  rename_mapping ->
  bool

Source

val create_locals_rename_mapping : 
  string list ->
  string list ->
  string StringMap.t

Sourceval is_rename_mapping_empty : rename_mapping -> bool

Source

val (&&>>) : 
  (bool * rename_mapping) ->
  (rename_mapping:rename_mapping -> bool * rename_mapping) ->
  bool * rename_mapping

Sourceval (&&>) : (bool * rename_mapping) -> bool -> bool * rename_mapping

Source

val forward_list_equal : 
  ?propF:
    ((bool * rename_mapping) ->
      (rename_mapping:rename_mapping -> bool * rename_mapping) ->
      bool * rename_mapping) ->
  ('a -> 'b -> rename_mapping:rename_mapping -> bool * rename_mapping) ->
  'a list ->
  'b list ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Sourceval compare_name : string -> string -> bool

Source

val eq_constant : 
  rename_mapping:rename_mapping ->
  acc:(GoblintCil.typ * GoblintCil.typ) list ->
  GoblintCil.constant ->
  GoblintCil.constant ->
  bool * rename_mapping

Source

val eq_lhost : 
  GoblintCil.lhost ->
  GoblintCil.lhost ->
  rename_mapping:rename_mapping ->
  acc:(GoblintCil.typ * GoblintCil.typ) list ->
  bool * rename_mapping

Sourceval global_typ_acc : (GoblintCil.typ * GoblintCil.typ) list ref

Source

val mem_typ_acc : 
  GoblintCil.typ ->
  GoblintCil.typ ->
  (GoblintCil.typ * GoblintCil.typ) list ->
  bool

Source

val pretty_length : 
  unit ->
  (GoblintCil.typ * GoblintCil.typ) list ->
  GoblintCil.Pretty.doc

Source

val eq_typ_acc : 
  ?fun_parameter_name_comparison_enabled:bool ->
  GoblintCil.typ ->
  GoblintCil.typ ->
  rename_mapping:rename_mapping ->
  acc:(GoblintCil.typ * GoblintCil.typ) list ->
  bool * rename_mapping

Source

val eq_eitems : 
  (string * GoblintCil.attributes * GoblintCil.exp * GoblintCil.location) ->
  (string * GoblintCil.attributes * GoblintCil.exp * GoblintCil.location) ->
  rename_mapping:rename_mapping ->
  acc:(GoblintCil.typ * GoblintCil.typ) list ->
  bool * rename_mapping

Source

val eq_enuminfo : 
  GoblintCil.enuminfo ->
  GoblintCil.enuminfo ->
  rename_mapping:rename_mapping ->
  acc:(GoblintCil.typ * GoblintCil.typ) list ->
  bool * rename_mapping

Source

val eq_args : 
  ?fun_parameter_name_comparison_enabled:bool ->
  (string * GoblintCil.typ * GoblintCil.attributes) ->
  (string * GoblintCil.typ * GoblintCil.attributes) ->
  rename_mapping:rename_mapping ->
  acc:(GoblintCil.typ * GoblintCil.typ) list ->
  bool * rename_mapping

Source

val eq_attrparam : 
  GoblintCil.attrparam ->
  GoblintCil.attrparam ->
  rename_mapping:rename_mapping ->
  acc:(GoblintCil.typ * GoblintCil.typ) list ->
  bool * rename_mapping

Source

val eq_attribute : 
  GoblintCil.attribute ->
  GoblintCil.attribute ->
  acc:(GoblintCil.typ * GoblintCil.typ) list ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val eq_compinfo : 
  GoblintCil.compinfo ->
  GoblintCil.compinfo ->
  (GoblintCil.typ * GoblintCil.typ) list ->
  rename_mapping ->
  bool * rename_mapping

Source

val eq_fieldinfo : 
  GoblintCil.fieldinfo ->
  GoblintCil.fieldinfo ->
  acc:(GoblintCil.typ * GoblintCil.typ) list ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val eq_typ : 
  ?fun_parameter_name_comparison_enabled:bool ->
  GoblintCil.typ ->
  GoblintCil.typ ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val eq_exp : 
  GoblintCil.exp ->
  GoblintCil.exp ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val eq_varinfo : 
  GoblintCil.varinfo ->
  GoblintCil.varinfo ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val eq_lval : 
  GoblintCil.lval ->
  GoblintCil.lval ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val eq_offset : 
  GoblintCil.offset ->
  GoblintCil.offset ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val eq_instr : 
  GoblintCil.instr ->
  GoblintCil.instr ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Sourceval eq_label : GoblintCil.label -> GoblintCil.label -> bool

Source

val eq_stmt_with_location : 
  (GoblintCil.stmt * GoblintCil.fundec) ->
  (GoblintCil.stmt * GoblintCil.fundec) ->
  bool

Source

val eq_stmtkind : 
  ?cfg_comp:bool ->
  (GoblintCil.stmtkind * GoblintCil.fundec) ->
  (GoblintCil.stmtkind * GoblintCil.fundec) ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val eq_stmt : 
  ?cfg_comp:bool ->
  (GoblintCil.stmt * GoblintCil.fundec) ->
  (GoblintCil.stmt * GoblintCil.fundec) ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val eq_block : 
  (GoblintCil.Cil.block * GoblintCil.fundec) ->
  (GoblintCil.Cil.block * GoblintCil.fundec) ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val eq_init : 
  GoblintCil.init ->
  GoblintCil.init ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val eq_initinfo : 
  GoblintCil.initinfo ->
  GoblintCil.initinfo ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val (&&<>) : 
  (bool * rename_mapping) ->
  (rename_mapping:rename_mapping -> bool * rename_mapping) ->
  bool * rename_mapping

Source

val eq_node : 
  (MyCFG.node * GoblintCil.fundec) ->
  (MyCFG.node * GoblintCil.fundec) ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val eq_edge : 
  MyCFG.edge ->
  MyCFG.edge ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Source

val eq_edge_list : 
  MyCFG.edge list ->
  MyCFG.edge list ->
  rename_mapping:rename_mapping ->
  bool * rename_mapping

Sourceval to_edge_list : ('a * 'b) list -> 'b list

Sourcemodule NH = CompareCFG.NH

Sourcetype biDirectionNodeMap = CompareCFG.biDirectionNodeMap = {

node1to2 : MyCFG.node NH.t;
node2to1 : MyCFG.node NH.t;

}

Source

val compareCfgs : 
  (module MyCFG.CfgForward) ->
  (module MyCFG.CfgForward) ->
  GoblintCil.fundec ->
  GoblintCil.fundec ->
  rename_mapping ->
  biDirectionNodeMap * unit NH.t * rename_mapping

Source

val reexamine : 
  'a ->
  CilType.Fundec.t ->
  biDirectionNodeMap ->
  unit NH.t ->
  (module MyCFG.CfgForward) ->
  (module MyCFG.CfgBidir) ->
  (NH.key * MyCFG.node) Seq.t * NH.key Seq.t

Source

val compareFun : 
  (module MyCFG.CfgForward) ->
  (module MyCFG.CfgBidir) ->
  GoblintCil.fundec ->
  GoblintCil.fundec ->
  rename_mapping ->
  (MyCFG.node * MyCFG.node) list * MyCFG.node list * rename_mapping

include module type of struct include CilMaps end

Sourcemodule FundecForMap = CilMaps.FundecForMap

Sourcemodule FundecMap = CilMaps.FundecMap

Sourcemodule VarinfoOrdered = CilMaps.VarinfoOrdered

Sourcemodule VarinfoMap = CilMaps.VarinfoMap

Sourcemodule GlobalMap : sig ... end

Sourcetype global_def =

| Var of GoblintCil.varinfo
| Fun of GoblintCil.fundec

Sourcetype global_col = {

decls : GoblintCil.varinfo option;
def : global_def option;

}

Sourceval name_of_global_col : global_col -> string

Sourceval compare_global_col : global_col -> global_col -> int

Sourceval equal_name_global_col : global_col -> global_col -> bool

Sourceval get_varinfo : global_col -> GoblintCil.varinfo

Sourcemodule GlobalColMap : sig ... end

Sourceval name_of_global : GoblintCil.global -> string

Sourcetype nodes_diff = {

unchangedNodes : (MyCFG.node * MyCFG.node) list;
primObsoleteNodes : MyCFG.node list;
(*
primary obsolete nodes -> all obsolete nodes are reachable from these
*)

}

Sourcetype unchanged_global = {

old : global_col;
current : global_col;

}

For semantically unchanged globals, still keep old and current version of global for resetting current to old.

Sourcetype changed_global = {

old : global_col;
current : global_col;
unchangedHeader : bool;
diff : nodes_diff option;

}

Sourcemodule VarinfoSet : sig ... end

Sourcetype change_info = {

mutable changed : changed_global list;
mutable unchanged : unchanged_global list;
mutable removed : global_col list;
mutable added : global_col list;
mutable exclude_from_rel_destab : VarinfoSet.t;
(*
Set of functions that are to be force-reanalyzed. These functions are additionally included in the changed field, among the other changed globals.
*)

}

Sourceval empty_change_info : unit -> change_info

Sourcetype change_status =

| Unchanged
| Changed
| ChangedFunHeader of GoblintCil.Cil.fundec
| ForceReanalyze of GoblintCil.Cil.fundec

Sourceval unchanged_to_change_status : bool -> change_status

Given a boolean that indicates whether the code object is identical to the previous version, returns the corresponding change_status

Sourceval empty_rename_mapping : rename_mapping

Sourceval should_reanalyze : GoblintCil.Cil.fundec -> bool

Sourceval performRenames : renamesOnSuccess -> unit

Source

val preservesSameNameMatches : 
  GlobalMap.key ->
  'a GlobalMap.t ->
  GlobalMap.key ->
  'b GlobalMap.t ->
  bool

Source

val addToFinalMatchesMapping : 
  VarinfoMap.key ->
  VarinfoMap.key ->
  (VarinfoMap.key VarinfoMap.t * VarinfoMap.key VarinfoMap.t) ->
  VarinfoMap.key VarinfoMap.t * VarinfoMap.key VarinfoMap.t

Sourceval empty_rename_assms : GoblintCil.varinfo VarinfoMap.t -> bool

Source

val already_matched : 
  VarinfoMap.key ->
  GoblintCil.varinfo ->
  (GoblintCil.varinfo VarinfoMap.t * 'a) ->
  bool

Sourceval change_info_lookup : global_col -> global_col -> change_info -> bool

Source

val eq_glob_var : 
  ?finalizeOnlyExactMatch:bool ->
  VarinfoMap.key ->
  global_col ->
  'a GlobalMap.t ->
  GoblintCil.varinfo ->
  global_col ->
  'b GlobalMap.t ->
  change_info ->
  (VarinfoMap.key VarinfoMap.t * VarinfoMap.key VarinfoMap.t) ->
  bool
  * change_info
  * (VarinfoMap.key VarinfoMap.t * VarinfoMap.key VarinfoMap.t)

Source

val compare_varinfo_exact : 
  VarinfoMap.key ->
  global_col ->
  global_col GlobalMap.t ->
  GoblintCil.varinfo ->
  global_col ->
  global_col GlobalMap.t ->
  change_info ->
  (VarinfoMap.key VarinfoMap.t * VarinfoMap.key VarinfoMap.t) ->
  bool
  * change_info
  * (VarinfoMap.key VarinfoMap.t * VarinfoMap.key VarinfoMap.t)

Source

val eqF : 
  GoblintCil.Cil.fundec ->
  GoblintCil.Cil.fundec ->
  (MyCFG.cfg * (MyCFG.cfg * MyCFG.cfg)) option ->
  method_rename_assumptions ->
  glob_var_rename_assumptions ->
  change_status
  * nodes_diff option
  * method_rename_assumptions
  * glob_var_rename_assumptions
  * renamesOnSuccess

Source

val eqF_only_consider_exact_match : 
  global_col ->
  global_col ->
  change_info ->
  (VarinfoMap.key VarinfoMap.t * VarinfoMap.key VarinfoMap.t) ->
  global_col GlobalMap.t ->
  global_col GlobalMap.t ->
  bool
  * change_info
  * (VarinfoMap.key VarinfoMap.t * VarinfoMap.key VarinfoMap.t)

Source

val eqF_check_contained_renames : 
  renameDetection:bool ->
  GoblintCil.Cil.fundec ->
  GoblintCil.Cil.fundec ->
  global_col GlobalMap.t ->
  global_col GlobalMap.t ->
  (MyCFG.cfg * (MyCFG.cfg * MyCFG.cfg)) option ->
  global_col ->
  global_col ->
  (change_info * (VarinfoMap.key VarinfoMap.t * VarinfoMap.key VarinfoMap.t)) ->
  change_info * (VarinfoMap.key VarinfoMap.t * VarinfoMap.key VarinfoMap.t)

Source

val eq_glob : 
  ?matchVars:bool ->
  ?matchFuns:bool ->
  ?renameDetection:bool ->
  global_col GlobalMap.t ->
  global_col GlobalMap.t ->
  (MyCFG.cfg * (MyCFG.cfg * MyCFG.cfg)) option ->
  global_col ->
  global_col ->
  (change_info * (VarinfoMap.key VarinfoMap.t * VarinfoMap.key VarinfoMap.t)) ->
  change_info * (VarinfoMap.key VarinfoMap.t * VarinfoMap.key VarinfoMap.t)

Source

val addNewGlobals : 
  'a ->
  global_col ->
  (change_info * ('b * 'c VarinfoMap.t)) ->
  change_info * ('b * 'c VarinfoMap.t)

Source

val addOldGlobals : 
  'a ->
  global_col ->
  (change_info * ('b VarinfoMap.t * 'c)) ->
  change_info * ('b VarinfoMap.t * 'c)

Source

val compareCilFiles : 
  ?eq:
    (?matchVars:bool ->
      ?matchFuns:bool ->
      ?renameDetection:bool ->
      global_col GlobalMap.t ->
      global_col GlobalMap.t ->
      (MyCFG.cfg * (MyCFG.cfg * MyCFG.cfg)) option ->
      global_col ->
      global_col ->
      (change_info
       * (VarinfoMap.key VarinfoMap.t * VarinfoMap.key VarinfoMap.t)) ->
      change_info * (VarinfoMap.key VarinfoMap.t * VarinfoMap.key VarinfoMap.t)) ->
  GoblintCil.file ->
  GoblintCil.file ->
  change_info

Given an (optional) equality function between Cil.globals, an old and a new Cil.file, this function computes a change_info, which describes which globals are changed, unchanged, removed and added.