package goblint
Static analysis framework for C
Install
Dune Dependency
Authors
Maintainers
Sources
goblint-2.4.0.tbz
sha256=99b78e6def71534d195eef9084baa26d8334b36084e120aa6afb300c9bf8afa6
sha512=f3162bd95a03c00358a2991f6152fc6169205bfb4c55e2c483e98cc3935673df9656d025b6f1ea0fa5f1bd0aee037d4f483966b0d2907e3fa9bf11a93a3392af
doc/src/goblint.incremental/compareAST.ml.html
Source file compareAST.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374
(** Comparison of CIL ASTs. *) open GoblintCil open CilMaps module StringMap = Map.Make(String) (* Mapping with rename assumptions about functions collected during the comparison. An assumption means that the comparison result so far is only correct, if the varinfos of a key-value pair in the mapping represent the same but renamed function. It is a mapping from a varinfo in the old version to one in the new version. *) type method_rename_assumptions = varinfo VarinfoMap.t (* Similiarly to method_rename_assumptions, just that rename assumptions about global variables are collected. *) type glob_var_rename_assumptions = varinfo VarinfoMap.t (* On a successful match, these compinfo and enuminfo names have to be set to the snd element of the tuple. *) type renamesOnSuccess = (compinfo * compinfo) list * (enuminfo * enuminfo) list (* The rename_mapping is carried through the stack when comparing the AST. Holds a list of rename assumptions. The first component is a map of rename assumptions about locals, i.e., parameters and local variables and is only used when comparing functions. *) type rename_mapping = (string StringMap.t) * method_rename_assumptions * glob_var_rename_assumptions * renamesOnSuccess (* Compares two names, being aware of the rename_mapping. Returns true iff: 1. there is a rename for name1 -> name2 = rename(name1) 2. there is no rename for name1 -> name1 = name2 *) let rename_mapping_aware_name_comparison (name1: string) (name2: string) (rename_mapping: rename_mapping) = if GobConfig.get_bool "incremental.detect-renames" then ( let (local_c, method_c, _, _) = rename_mapping in let existingAssumption: string option = StringMap.find_opt name1 local_c in match existingAssumption with | Some now -> now = name2 | None -> name1 = name2 (* Var names differ, but there is no assumption, so this can't be good *) ) else name1 = name2 (* Creates the mapping of local renames. If the locals do not match in size, an empty mapping is returned. *) let create_locals_rename_mapping (originalLocalNames: string list) (updatedLocalNames: string list): string StringMap.t = if List.compare_lengths originalLocalNames updatedLocalNames = 0 then List.combine originalLocalNames updatedLocalNames |> List.filter (fun (original, now) -> not (original = now)) |> List.map (fun (original, now) -> (original, now)) |> (fun list -> List.fold_left (fun map mapping -> StringMap.add (fst mapping) (snd mapping) map) StringMap.empty list ) else StringMap.empty let is_rename_mapping_empty (rename_mapping: rename_mapping) = let local, methods, glob_vars, _= rename_mapping in StringMap.is_empty local && VarinfoMap.is_empty methods && VarinfoMap.is_empty glob_vars (* rename mapping forward propagation, takes the result from a call and propagates the rename mapping to the next call. the second call is only executed if the previous call returned true *) let (&&>>) (prev_result: bool * rename_mapping) f : bool * rename_mapping = let (prev_equal, updated_rename_mapping) = prev_result in if prev_equal then f ~rename_mapping:updated_rename_mapping else false, updated_rename_mapping (* Same as && but propagates the rename mapping *) let (&&>) (prev_result: bool * rename_mapping) (b: bool) : bool * rename_mapping = let (prev_equal, rename_mapping) = prev_result in (prev_equal && b, rename_mapping) (* Same as Goblist.eq but propagates the rename_mapping *) let forward_list_equal ?(propF = (&&>>)) f l1 l2 ~(rename_mapping: rename_mapping) : bool * rename_mapping = if ((List.compare_lengths l1 l2) = 0) then List.fold_left2 (fun (b, r) x y -> propF (b, r) (f x y)) (true, rename_mapping) l1 l2 else false, rename_mapping (* hack: CIL generates new type names for anonymous types - we want to ignore these *) let compare_name (a: string) (b: string) = let anon_struct = "__anonstruct_" in let anon_union = "__anonunion_" in if a = b then true else BatString.(starts_with a anon_struct && starts_with b anon_struct || starts_with a anon_union && starts_with b anon_union) let rec eq_constant ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) (a: constant) (b: constant) : bool * rename_mapping = match a, b with | CInt (val1, kind1, str1), CInt (val2, kind2, str2) -> Z.compare val1 val2 = 0 && kind1 = kind2, rename_mapping (* Ignore string representation, i.e. 0x2 == 2 *) | CEnum (exp1, str1, enuminfo1), CEnum (exp2, str2, enuminfo2) -> eq_exp exp1 exp2 ~rename_mapping ~acc (* Ignore name and enuminfo *) | a, b -> a = b, rename_mapping and eq_exp (a: exp) (b: exp) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) : bool * rename_mapping = match a, b with | Const c1, Const c2 -> eq_constant c1 c2 ~rename_mapping ~acc | Lval lv1, Lval lv2 -> eq_lval lv1 lv2 ~rename_mapping ~acc | SizeOf typ1, SizeOf typ2 -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc | SizeOfE exp1, SizeOfE exp2 -> eq_exp exp1 exp2 ~rename_mapping ~acc | SizeOfStr str1, SizeOfStr str2 -> str1 = str2, rename_mapping (* possibly, having the same length would suffice *) | AlignOf typ1, AlignOf typ2 -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc | AlignOfE exp1, AlignOfE exp2 -> eq_exp exp1 exp2 ~rename_mapping ~acc | UnOp (op1, exp1, typ1), UnOp (op2, exp2, typ2) -> ((op1 == op2), rename_mapping) &&>> eq_exp exp1 exp2 ~acc &&>> eq_typ_acc typ1 typ2 ~acc | BinOp (op1, left1, right1, typ1), BinOp (op2, left2, right2, typ2) -> (op1 = op2, rename_mapping) &&>> eq_exp left1 left2 ~acc &&>> eq_exp right1 right2 ~acc &&>> eq_typ_acc typ1 typ2 ~acc | CastE (typ1, exp1), CastE (typ2, exp2) -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc &&>> eq_exp exp1 exp2 ~acc | AddrOf lv1, AddrOf lv2 -> eq_lval lv1 lv2 ~rename_mapping ~acc | StartOf lv1, StartOf lv2 -> eq_lval lv1 lv2 ~rename_mapping ~acc | Real exp1, Real exp2 -> eq_exp exp1 exp2 ~rename_mapping ~acc | Imag exp1, Imag exp2 -> eq_exp exp1 exp2 ~rename_mapping ~acc | Question (b1, t1, f1, typ1), Question (b2, t2, f2, typ2) -> eq_exp b1 b2 ~rename_mapping ~acc &&>> eq_exp t1 t2 ~acc &&>> eq_exp f1 f2 ~acc &&>> eq_typ_acc typ1 typ2 ~acc | AddrOfLabel _, AddrOfLabel _ -> false, rename_mapping (* TODO: what to do? *) | _, _ -> false, rename_mapping and eq_lhost (a: lhost) (b: lhost) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) = match a, b with Var v1, Var v2 -> eq_varinfo v1 v2 ~rename_mapping ~acc | Mem exp1, Mem exp2 -> eq_exp exp1 exp2 ~rename_mapping ~acc | _, _ -> false, rename_mapping and global_typ_acc: (typ * typ) list ref = ref [] (* TODO: optimize with physical Hashtbl? *) and mem_typ_acc (a: typ) (b: typ) acc = List.exists (fun p -> match p with (x, y) -> a == x && b == y) acc (* TODO: seems slightly more efficient to not use "fun (x, y) ->" directly to avoid caml_tuplify2 *) and pretty_length () l = Pretty.num (List.length l) and eq_typ_acc ?(fun_parameter_name_comparison_enabled: bool = true) (a: typ) (b: typ) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) : bool * rename_mapping = (* Registers a compinfo rename or a enum rename*) let register_rename_on_success = fun rename_mapping compinfo_option enum_option -> let maybeAddTuple list option = BatOption.map_default (fun v -> v :: list) list option in let (a, b, c, renames_on_success) = rename_mapping in let (compinfoRenames, enumRenames) = renames_on_success in let updatedCompinfoRenames = maybeAddTuple compinfoRenames compinfo_option in let updatedEnumRenames = maybeAddTuple enumRenames enum_option in a, b, c, (updatedCompinfoRenames, updatedEnumRenames) in if Messages.tracing then Messages.tracei "compareast" "eq_typ_acc %a vs %a (%a, %a)" d_type a d_type b pretty_length acc pretty_length !global_typ_acc; (* %a makes List.length calls lazy if compareast isn't being traced *) let r, updated_rename_mapping = match a, b with | TPtr (typ1, attr1), TPtr (typ2, attr2) -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc &&>> forward_list_equal (eq_attribute ~acc) attr1 attr2 | TArray (typ1, (Some lenExp1), attr1), TArray (typ2, (Some lenExp2), attr2) -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc &&>> eq_exp lenExp1 lenExp2 ~acc &&>> forward_list_equal (eq_attribute ~acc) attr1 attr2 | TArray (typ1, None, attr1), TArray (typ2, None, attr2) -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc &&>> forward_list_equal (eq_attribute ~acc) attr1 attr2 | TFun (typ1, (Some list1), varArg1, attr1), TFun (typ2, (Some list2), varArg2, attr2) -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc &&>> forward_list_equal (eq_args ~fun_parameter_name_comparison_enabled ~acc) list1 list2 &&> (varArg1 = varArg2) &&>> forward_list_equal (eq_attribute ~acc) attr1 attr2 | TFun (typ1, None, varArg1, attr1), TFun (typ2, None, varArg2, attr2) -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc &&> (varArg1 = varArg2) &&>> forward_list_equal (eq_attribute ~acc) attr1 attr2 | TNamed (typinfo1, attr1), TNamed (typeinfo2, attr2) -> eq_typ_acc typinfo1.ttype typeinfo2.ttype ~rename_mapping ~acc &&>> forward_list_equal (eq_attribute ~acc) attr1 attr2 (* Ignore tname, treferenced *) | TNamed (tinf, attr), b -> eq_typ_acc tinf.ttype b ~rename_mapping ~acc (* Ignore tname, treferenced. TODO: dismiss attributes, or not? *) | a, TNamed (tinf, attr) -> eq_typ_acc a tinf.ttype ~rename_mapping ~acc (* Ignore tname, treferenced . TODO: dismiss attributes, or not? *) (* The following two lines are a hack to ensure that anonymous types get the same name and thus, the same typsig *) | TComp (compinfo1, attr1), TComp (compinfo2, attr2) -> if mem_typ_acc a b acc || mem_typ_acc a b !global_typ_acc then ( if Messages.tracing then Messages.trace "compareast" "in acc"; true, rename_mapping ) else ( let acc = (a, b) :: acc in let (res, rm) = eq_compinfo compinfo1 compinfo2 acc rename_mapping &&>> forward_list_equal (eq_attribute ~acc) attr1 attr2 in let updated_rm = if res then ( global_typ_acc := (a, b) :: !global_typ_acc; register_rename_on_success rm (Some((compinfo2, compinfo1))) None ) else rm in res, updated_rm ) | TEnum (enuminfo1, attr1), TEnum (enuminfo2, attr2) -> let (res, rm) = eq_enuminfo enuminfo1 enuminfo2 ~rename_mapping ~acc &&>> forward_list_equal (eq_attribute ~acc) attr1 attr2 in if res && enuminfo1.ename <> enuminfo2.ename then res, register_rename_on_success rm None (Some((enuminfo2, enuminfo1))) else res, rm | TBuiltin_va_list attr1, TBuiltin_va_list attr2 -> forward_list_equal (eq_attribute ~acc) attr1 attr2 ~rename_mapping | TVoid attr1, TVoid attr2 -> forward_list_equal (eq_attribute ~acc) attr1 attr2 ~rename_mapping | TInt (ik1, attr1), TInt (ik2, attr2) -> (ik1 = ik2, rename_mapping) &&>> forward_list_equal (eq_attribute ~acc) attr1 attr2 | TFloat (fk1, attr1), TFloat (fk2, attr2) -> (fk1 = fk2, rename_mapping) &&>> forward_list_equal (eq_attribute ~acc) attr1 attr2 | _, _ -> false, rename_mapping in if Messages.tracing then Messages.traceu "compareast" "eq_typ_acc %a vs %a" d_type a d_type b; (r, updated_rename_mapping) and eq_eitems (a: string * exp * location) (b: string * exp * location) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) = match a, b with (name1, exp1, _l1), (name2, exp2, _l2) -> (name1 = name2, rename_mapping) &&>> eq_exp exp1 exp2 ~acc (* Ignore location *) and eq_enuminfo (a: enuminfo) (b: enuminfo) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) = (compare_name a.ename b.ename, rename_mapping) &&>> forward_list_equal (eq_attribute ~acc) a.eattr b.eattr &&>> forward_list_equal (eq_eitems ~acc) a.eitems b.eitems (* Ignore ereferenced *) (*param: fun_parameter_name_comparison_enabled when set to false, skips the comparison of the names*) and eq_args ?(fun_parameter_name_comparison_enabled: bool = true) (a: string * typ * attributes) (b: string * typ * attributes) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) : bool * rename_mapping = match a, b with (name1, typ1, attr1), (name2, typ2, attr2) -> ((not fun_parameter_name_comparison_enabled) || rename_mapping_aware_name_comparison name1 name2 rename_mapping, rename_mapping) &&>> eq_typ_acc typ1 typ2 ~acc &&>> forward_list_equal (eq_attribute ~acc) attr1 attr2 and eq_attrparam (a: attrparam) (b: attrparam) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) : bool * rename_mapping = match a, b with | ACons (str1, attrparams1), ACons (str2, attrparams2) -> (str1 = str2, rename_mapping) &&>> forward_list_equal (eq_attrparam ~acc) attrparams1 attrparams2 | ASizeOf typ1, ASizeOf typ2 -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc | ASizeOfE attrparam1, ASizeOfE attrparam2 -> eq_attrparam attrparam1 attrparam2 ~rename_mapping ~acc | ASizeOfS typsig1, ASizeOfS typsig2 -> typsig1 = typsig2, rename_mapping | AAlignOf typ1, AAlignOf typ2 -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc | AAlignOfE attrparam1, AAlignOfE attrparam2 -> eq_attrparam attrparam1 attrparam2 ~rename_mapping ~acc | AAlignOfS typsig1, AAlignOfS typsig2 -> typsig1 = typsig2, rename_mapping | AUnOp (op1, attrparam1), AUnOp (op2, attrparam2) -> (op1 = op2, rename_mapping) &&>> eq_attrparam attrparam1 attrparam2 ~acc | ABinOp (op1, left1, right1), ABinOp (op2, left2, right2) -> (op1 = op2, rename_mapping) &&>> eq_attrparam left1 left2 ~acc &&>> eq_attrparam right1 right2 ~acc | ADot (attrparam1, str1), ADot (attrparam2, str2) -> (str1 = str2, rename_mapping) &&>> eq_attrparam attrparam1 attrparam2 ~acc | AStar attrparam1, AStar attrparam2 -> eq_attrparam attrparam1 attrparam2 ~rename_mapping ~acc | AAddrOf attrparam1, AAddrOf attrparam2 -> eq_attrparam attrparam1 attrparam2 ~rename_mapping ~acc | AIndex (left1, right1), AIndex (left2, right2) -> eq_attrparam left1 left2 ~rename_mapping ~acc &&>> eq_attrparam right1 right2 ~acc | AQuestion (left1, middle1, right1), AQuestion (left2, middle2, right2) -> eq_attrparam left1 left2 ~rename_mapping ~acc &&>> eq_attrparam middle1 middle2 ~acc &&>> eq_attrparam right1 right2 ~acc | AAssign (left1, right1), AAssign (left2, right2) -> eq_attrparam left1 left2 ~rename_mapping ~acc &&>> eq_attrparam right1 right2 ~acc | a, b -> a = b, rename_mapping and eq_attribute (a: attribute) (b: attribute) ~(acc: (typ * typ) list) ~(rename_mapping: rename_mapping) = match a, b with | Attr (name1, params1), Attr (name2, params2) -> (name1 = name2, rename_mapping) &&>> forward_list_equal (eq_attrparam ~acc) params1 params2 and eq_varinfo (a: varinfo) (b: varinfo) ~(acc: (typ * typ) list) ~(rename_mapping: rename_mapping) = let (locals_renames, method_rename_mappings, glob_vars, renames_on_success) = rename_mapping in let compare_local_and_global_var = if a.vglob then let present_mapping = VarinfoMap.find_opt a glob_vars in match present_mapping with | Some (knownNowVarinfo) -> b.vname = knownNowVarinfo.vname, method_rename_mappings, glob_vars | None -> ( let update_glob_vars = VarinfoMap.add a b glob_vars in true, method_rename_mappings, update_glob_vars ) else rename_mapping_aware_name_comparison a.vname b.vname rename_mapping, method_rename_mappings, glob_vars in (*When we compare function names, we can directly compare the naming from the rename_mapping if it exists.*) let isNamingOk, updated_method_rename_mappings, updatedGlobVarMapping = match a.vtype, b.vtype with | TFun(_, aParamSpec, _, _), TFun(_, bParamSpec, _, _) -> ( let specific_method_rename_mapping = VarinfoMap.find_opt a method_rename_mappings in match specific_method_rename_mapping with | Some new_varinfo -> let is_naming_ok = new_varinfo.vname = b.vname in is_naming_ok, method_rename_mappings, glob_vars | None -> if a.vname <> b.vname then true, VarinfoMap.add a b method_rename_mappings, glob_vars else true, method_rename_mappings, glob_vars ) | _, _ -> compare_local_and_global_var in (*If the following is a method call, we need to check if we have a mapping for that method call. *) let fun_parameter_name_comparison_enabled = match b.vtype with | TFun(_, _, _, _) -> false | _ -> true in (*Ignore rename mapping for type check, as it doesn't change anyway. We only need the renames_on_success*) let (typeCheck, (_, _, _, updated_renames_on_success)) = eq_typ_acc ~fun_parameter_name_comparison_enabled a.vtype b.vtype ~rename_mapping:(StringMap.empty, VarinfoMap.empty, VarinfoMap.empty, renames_on_success) ~acc in (isNamingOk && typeCheck, (locals_renames, updated_method_rename_mappings, updatedGlobVarMapping, updated_renames_on_success)) &&>> forward_list_equal (eq_attribute ~acc) a.vattr b.vattr &&> (a.vstorage = b.vstorage) &&> (a.vglob = b.vglob) &&> (a.vaddrof = b.vaddrof) (* Ignore the location, vid, vreferenced, vdescr, vdescrpure, vinline *) (* Accumulator is needed because of recursive types: we have to assume that two types we already encountered in a previous step of the recursion are equivalent *) and eq_compinfo (a: compinfo) (b: compinfo) (acc: (typ * typ) list) (rename_mapping: rename_mapping) : bool * rename_mapping = (a.cstruct = b.cstruct, rename_mapping) &&> compare_name a.cname b.cname &&>> forward_list_equal (fun a b -> eq_fieldinfo a b ~acc) a.cfields b.cfields &&>> forward_list_equal (eq_attribute ~acc ) a.cattr b.cattr &&> (a.cdefined = b.cdefined) (* Ignore ckey, and ignore creferenced *) and eq_fieldinfo (a: fieldinfo) (b: fieldinfo) ~(acc: (typ * typ) list) ~(rename_mapping: rename_mapping) = if Messages.tracing then Messages.tracei "compareast" "fieldinfo %s vs %s" a.fname b.fname; let (r, rm) = (a.fname = b.fname, rename_mapping) &&>> eq_typ_acc a.ftype b.ftype ~acc &&> (a.fbitfield = b.fbitfield) &&>> forward_list_equal (eq_attribute ~acc) a.fattr b.fattr in if Messages.tracing then Messages.traceu "compareast" "fieldinfo %s vs %s" a.fname b.fname; (r, rm) and eq_offset (a: offset) (b: offset) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) : bool * rename_mapping = match a, b with NoOffset, NoOffset -> true, rename_mapping | Field (info1, offset1), Field (info2, offset2) -> eq_fieldinfo info1 info2 ~rename_mapping ~acc &&>> eq_offset offset1 offset2 ~acc | Index (exp1, offset1), Index (exp2, offset2) -> eq_exp exp1 exp2 ~rename_mapping ~acc &&>> eq_offset offset1 offset2 ~acc | _, _ -> false, rename_mapping and eq_lval (a: lval) (b: lval) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) : bool * rename_mapping = match a, b with (host1, off1), (host2, off2) -> eq_lhost host1 host2 ~rename_mapping ~acc &&>> eq_offset off1 off2 ~acc let eq_typ = eq_typ_acc ~acc:[] let eq_exp = eq_exp ~acc:[] let eq_varinfo = eq_varinfo ~acc:[] let eq_lval = eq_lval ~acc:[] let eq_offset = eq_offset ~acc:[] let eq_instr (a: instr) (b: instr) ~(rename_mapping: rename_mapping) = match a, b with | Set (lv1, exp1, _l1, _el1), Set (lv2, exp2, _l2, _el2) -> eq_lval lv1 lv2 ~rename_mapping &&>> eq_exp exp1 exp2 | Call (Some lv1, f1, args1, _l1, _el1), Call (Some lv2, f2, args2, _l2, _el2) -> eq_lval lv1 lv2 ~rename_mapping &&>> eq_exp f1 f2 &&>> forward_list_equal eq_exp args1 args2 | Call (None, f1, args1, _l1, _el1), Call (None, f2, args2, _l2, _el2) -> eq_exp f1 f2 ~rename_mapping &&>> forward_list_equal eq_exp args1 args2 | Asm (attr1, tmp1, ci1, dj1, rk1, l1), Asm (attr2, tmp2, ci2, dj2, rk2, l2) -> (GobList.equal String.equal tmp1 tmp2, rename_mapping) &&>> forward_list_equal (fun (x1,y1,z1) (x2,y2,z2) ~rename_mapping:x-> (x1 = x2, x) &&> (y1 = y2) &&>> eq_lval z1 z2) ci1 ci2 &&>> forward_list_equal (fun (x1,y1,z1) (x2,y2,z2) ~rename_mapping:x-> (x1 = x2, x) &&> (y1 = y2) &&>> eq_exp z1 z2) dj1 dj2 &&> GobList.equal String.equal rk1 rk2(* ignore attributes and locations *) | VarDecl (v1, _l1), VarDecl (v2, _l2) -> eq_varinfo v1 v2 ~rename_mapping | _, _ -> false, rename_mapping let eq_label (a: label) (b: label) = match a, b with Label (lb1, _l1, s1), Label (lb2, _l2, s2) -> lb1 = lb2 && s1 = s2 | Case (exp1, _l1, _el1), Case (exp2, _l2, el_2) -> exp1 = exp2 | Default (_l1, _el1), Default (_l2, _el2) -> true | _, _ -> false (* This is needed for checking whether a goto does go to the same semantic location/statement*) let eq_stmt_with_location ((a, af): stmt * fundec) ((b, bf): stmt * fundec) = let offsetA = a.sid - (List.hd af.sallstmts).sid in let offsetB = b.sid - (List.hd bf.sallstmts).sid in GobList.equal eq_label a.labels b.labels && offsetA = offsetB (* cfg_comp: blocks need only be compared in the AST comparison. For cfg comparison of functions one instead walks through the cfg and only compares the currently visited node (The cil blocks inside an if statement should not be compared together with its condition to avoid a to early and not precise detection of a changed node inside). Switch, break and continue statements are removed during cfg preparation and therefore need not to be handeled *) let rec eq_stmtkind ?(cfg_comp = false) ((a, af): stmtkind * fundec) ((b, bf): stmtkind * fundec) ~(rename_mapping: rename_mapping) = let eq_block' = fun x y ~(rename_mapping:rename_mapping) -> if cfg_comp then true, rename_mapping else eq_block (x, af) (y, bf) ~rename_mapping in match a, b with | Instr is1, Instr is2 -> forward_list_equal eq_instr is1 is2 ~rename_mapping | Return (Some exp1, _l1, _el1), Return (Some exp2, _l2, _el2) -> eq_exp exp1 exp2 ~rename_mapping | Return (None, _l1, _el1), Return (None, _l2, _el2) -> true, rename_mapping | Return _, Return _ -> false, rename_mapping | Goto (st1, _l1), Goto (st2, _l2) -> eq_stmt_with_location (!st1, af) (!st2, bf), rename_mapping | Break _, Break _ -> if cfg_comp then failwith "CompareCFG: Invalid stmtkind in CFG" else true, rename_mapping | Continue _, Continue _ -> if cfg_comp then failwith "CompareCFG: Invalid stmtkind in CFG" else true, rename_mapping | If (exp1, then1, else1, _l1, _el1), If (exp2, then2, else2, _l2, _el2) -> eq_exp exp1 exp2 ~rename_mapping &&>> eq_block' then1 then2 &&>> eq_block' else1 else2 | Switch (exp1, block1, stmts1, _l1, _el1), Switch (exp2, block2, stmts2, _l2, _el2) -> if cfg_comp then failwith "CompareCFG: Invalid stmtkind in CFG" else eq_exp exp1 exp2 ~rename_mapping &&>> eq_block' block1 block2 &&>> forward_list_equal (fun a b -> eq_stmt (a,af) (b,bf)) stmts1 stmts2 | Loop (block1, _l1, _el1, _con1, _br1), Loop (block2, _l2, _el2, _con2, _br2) -> eq_block' block1 block2 ~rename_mapping | Block block1, Block block2 -> eq_block' block1 block2 ~rename_mapping | _, _ -> false, rename_mapping and eq_stmt ?cfg_comp ((a, af): stmt * fundec) ((b, bf): stmt * fundec) ~(rename_mapping: rename_mapping) = (GobList.equal eq_label a.labels b.labels, rename_mapping) &&>> eq_stmtkind ?cfg_comp (a.skind, af) (b.skind, bf) and eq_block ((a, af): Cil.block * fundec) ((b, bf): Cil.block * fundec) ~(rename_mapping: rename_mapping) : bool * rename_mapping = (a.battrs = b.battrs, rename_mapping) &&>> forward_list_equal (fun x y -> eq_stmt (x, af) (y, bf)) a.bstmts b.bstmts let rec eq_init (a: init) (b: init) ~(rename_mapping: rename_mapping) = match a, b with | SingleInit e1, SingleInit e2 -> eq_exp e1 e2 ~rename_mapping | CompoundInit (t1, l1), CompoundInit (t2, l2) -> eq_typ t1 t2 ~rename_mapping &&>> forward_list_equal (fun (o1, i1) (o2, i2) ~rename_mapping:rename_mapping -> eq_offset o1 o2 ~rename_mapping &&>> eq_init i1 i2) l1 l2 | _, _ -> false, rename_mapping let eq_initinfo (a: initinfo) (b: initinfo) ~(rename_mapping: rename_mapping) = match a.init, b.init with | (Some init_a), (Some init_b) -> eq_init init_a init_b ~rename_mapping | None, None -> true, rename_mapping | _, _ -> false, rename_mapping
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>