diff --git a/src/cil.ml b/src/cil.ml index 63da92793..d62e186f3 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -5039,44 +5039,6 @@ let dummyFile = globinit = None; globinitcalled = false;} -(***** Load and store files as unmarshalled Ocaml binary data. ****) -type savedFile = - { savedFile: file; - savedNextVID: int; - savedNextCompinfoKey: int} - -let saveBinaryFileChannel (cil_file : file) (outchan : out_channel) = - let save = {savedFile = cil_file; - savedNextVID = !nextGlobalVID; - savedNextCompinfoKey = !nextCompinfoKey} in - Marshal.to_channel outchan save [] - -let saveBinaryFile (cil_file : file) (filename : string) = - let outchan = open_out_bin filename in - saveBinaryFileChannel cil_file outchan; - close_out outchan - -(** Read a {!Cil.file} in binary form from the filesystem. The first - * argument is the name of a file previously created by - * {!Cil.saveBinaryFile}. Because this also reads some global state, - * this should be called before any other CIL code is parsed or generated. *) -let loadBinaryFile (filename : string) : file = - let inchan = open_in_bin filename in - let loaded : savedFile = (Marshal.from_channel inchan : savedFile) in - close_in inchan ; - (* nextGlobalVID = 11 because CIL initialises many dummy variables *) - if !nextGlobalVID != 11 || !nextCompinfoKey != 1 then begin - (* In this case, we should change all of the varinfo and compinfo - keys in loaded.savedFile to prevent conflicts. But since that hasn't - been implemented yet, just print a warning. If you do implement this, - please send it to the CIL maintainers. *) - ignore (E.warn "You are possibly loading a binary file after another file has been loaded. This isn't currently supported, so varinfo and compinfo id numbers may conflict.") - end; - nextGlobalVID := max loaded.savedNextVID !nextGlobalVID; - nextCompinfoKey := max loaded.savedNextCompinfoKey !nextCompinfoKey; - loaded.savedFile - - (* Take the name of a file and make a valid symbol name out of it. There are * a few characters that are not valid in symbols *) let makeValidSymbolName (s: string) = @@ -5824,6 +5786,206 @@ let mapGlobals (fl: file) | _ -> E.s (E.bug "mapGlobals: globinit is not a function") end) +(***** Load and store files as unmarshalled Ocaml binary data. ****) +type savedFile = + { savedFile: file; + savedNextVID: int; + savedNextCompinfoKey: int} +(* Note: savedNextVID and savedNextCompinfoKey are not needed + anymore because of the way saved files are loaded now (vid and ckey + are remapped at loading time) but they are kept for backward + compatibility *) + + +let saveBinaryFileChannel (cil_file : file) (outchan : out_channel) = + let save = {savedFile = cil_file; + savedNextVID = !nextGlobalVID; + savedNextCompinfoKey = !nextCompinfoKey} in + Marshal.to_channel outchan save [] + +let saveBinaryFile (cil_file : file) (filename : string) = + let outchan = open_out_bin filename in + saveBinaryFileChannel cil_file outchan; + close_out outchan + + +(* The re-mapping of varinfo vid fields and compinfo ckey fields is + simple: +- A first visit get all the vid and ckey from the file +- A new mapping is built from the current values of the nextGlobalVID + and nextCompinfoKey references. These references are increased. The + new mapping tries not to overlap the old values (because we do not + know in what order the second visit happends) +- A second visit uses the mapping built previously to give the vid and ckey + fields their new values + *) + +(* This class visits a file and adds the vid and ckey found to the +maps (implemented as int hashes) in argument *) +class harvestUidsClass vid_imap ckey_imap = +object(self) + inherit nopCilVisitor + + method vvrbl vi = if not(IH.mem vid_imap vi.vid) then IH.add vid_imap vi.vid 0; SkipChildren + method vvdec vi = if not(IH.mem vid_imap vi.vid) then IH.add vid_imap vi.vid 0; DoChildren + + method vglob g = + match g with + | GCompTag(ci,_) + | GCompTagDecl(ci,_) -> (if not(IH.mem ckey_imap ci.ckey) then IH.add ckey_imap ci.ckey 0; DoChildren) + | _ -> DoChildren + + method vtype typ = + match typ with + | TComp(ci,_) -> (if not(IH.mem ckey_imap ci.ckey) then IH.add ckey_imap ci.ckey 0; DoChildren) + | _ -> DoChildren + +end + +(* Given a list of uids and a reference counter, this function builds + a map of the old uids to the new uids, starting from the value + given by the counter. At the end of the function the counter has + been increased just above the list of uids that are to be + considered not usable anymore. + Let [x;y;z] be a map of uids and !c the counter: + [1;2;3] !4 will yield [(1,4); (2,5); (3,6)] !7 + [1;2;3] !2 will yield [(1,4); (2,5); (3,6)] !7 too + because with (1,2), "2" is already taken and if the visit + encounters "1" before "2", then "1" and "2" will be mapped to the + same value. Hence when a new potential mapping corresponds to a uid + already used, we must try with another uid. + This also depends on the order in which [1;2;3] is visited. If the mapping + had been visited as [2;3;1] !2 the result would be [(2,2);(3,3);(1,4)] + because not changing a uid is not dangerous. + In the end, this algorithm is a reasonable trade-off between simplicity and + soundness. + *) +let build_remapping imap counter = + let risks_more_mapping i = IH.mem imap i in + let rec find_suitable_uid i counter = + if i <> !counter (* Re-mapping i to i is acceptable *) + && risks_more_mapping !counter (* Re-mapping will work if the counter + is not a remappable uid *) + then (incr counter; find_suitable_uid i counter) + in + (* The inverse map is there as a debugging aid, to check that if we can + not re-map a vid/ckey, this is because it was already re-mapped. + A property of the mapping is that it is bijective. + *) + let add_inverse k v map = + if IH.mem map v + then E.s (bug "Could not build the new uids map into a bijection") + else IH.add map v k + in + let remap counter new_imap inverse i = + if IH.mem imap i + then begin + find_suitable_uid i counter; + IH.add new_imap i !counter; + add_inverse i !counter inverse; + incr counter + end + else E.s (bug "Trying to find a new uid for a uid that was not even discovered in the first visit") + in + let inverse = IH.create (IH.length imap) in +(* We have to create a new map because iterating over a hash and changing it + on-the-fly is no recommended *) + let new_imap = IH.create (IH.length imap) in + let () = IH.iter (fun k _ -> remap counter new_imap inverse k) imap in + (new_imap, inverse) + +(* This function updates the vid/ckey field (we abstracted it a bit + to use it for both fields). *) +let remap imap imap_inv entity e_update e_uid e_name e_type = + let entity_uid = e_uid entity in + try + if !E.debugFlag + then begin + ignore (E.log "Trying %s mapping for %s (%d)\n" e_type (e_name entity) entity_uid) + end; + let new_uid = IH.find imap entity_uid in + if entity_uid <> new_uid + then begin + if !E.debugFlag + then begin + ignore (E.log "Remap: %d -> %d\n" entity_uid new_uid) + end; + e_update entity new_uid + end + else + if !E.debugFlag + then begin + ignore (E.log "No change: %d -> %d\n" entity_uid new_uid) + end + with Not_found -> + if not(IH.mem imap_inv entity_uid) + then begin + E.s (E.bug "Error: could not find %s mapping for %s (%d)" e_type (e_name entity) entity_uid) + end + else + if !E.debugFlag + then ignore (E.log "Already remapped: %s (%d)\n" (e_name entity) entity_uid) + + +let remap_varinfo imap imap_inv vi = + remap imap imap_inv vi (fun v i -> v.vid <- i) (fun v -> v.vid) (fun v -> v.vname) "varinfo" + +let remap_compinfo imap imap_inv ci = + remap imap imap_inv ci (fun c i -> c.ckey <- i) (fun c -> c.ckey) (fun c -> c.cname) "compinfo" + +(* This class updates the vid/ckey fields with the new values given in + the maps in arguments *) +class remapperClass vid_imap vid_imap_inv ckey_imap ckey_imap_inv = +object(self) + inherit nopCilVisitor + + method vvrbl vi = remap_varinfo vid_imap vid_imap_inv vi; SkipChildren + method vvdec vi = remap_varinfo vid_imap vid_imap_inv vi; DoChildren + + method vglob g = + match g with + | GCompTag(ci,_) + | GCompTagDecl(ci,_) -> (remap_compinfo ckey_imap ckey_imap_inv ci; DoChildren) + | _ -> DoChildren + + method vtype typ = + match typ with + | TComp(ci,_) -> (remap_compinfo ckey_imap ckey_imap_inv ci; DoChildren) + | _ -> DoChildren + +end + +(* This function takes a CIL file, visits it for extracting all the + possible values for its varinfo vid fiels and compinfo ckey fields, + builds a mapping from these values to new values compatible with + the nextGlobalVID and nextCompinfoKey counters, and visits the file + a second time to applying this mapping. The counters at the end of + the function are updated to the next value not conflicting with + this mapping *) +let remap cil = + begin + let vid_imap = IH.create 1000 in + let ckey_imap = IH.create 10 in + let harvestUids = new harvestUidsClass vid_imap ckey_imap in + let () = visitCilFile harvestUids cil in + let (vid_imap_final, vid_imap_inv) = build_remapping vid_imap nextGlobalVID in + let (ckey_imap_final, ckey_imap_inv) = build_remapping ckey_imap nextCompinfoKey in + let remapper = new remapperClass vid_imap_final vid_imap_inv ckey_imap_final ckey_imap_inv in + let () = visitCilFile remapper cil in + cil + end + + +(** Read a {!Cil.file} in binary form from the filesystem. The first + * argument is the name of a file previously created by + * {!Cil.saveBinaryFile}. Because this also reads some global state, + * this should be called before any other CIL code is parsed or generated. *) +let loadBinaryFile (filename : string) : file = + let inchan = open_in_bin filename in + let loaded : savedFile = (Marshal.from_channel inchan : savedFile) in + close_in inchan ; + remap loaded.savedFile + let dumpFile (pp: cilPrinter) (out : out_channel) (outfile: string) file = diff --git a/src/cil.mli b/src/cil.mli index 8b8a699a9..365363966 100644 --- a/src/cil.mli +++ b/src/cil.mli @@ -1170,8 +1170,9 @@ val saveBinaryFileChannel : file -> out_channel -> unit (** Read a {!Cil.file} in binary form from the filesystem. The first * argument is the name of a file previously created by - * {!Cil.saveBinaryFile}. Because this also reads some global state, - * this should be called before any other CIL code is parsed or generated. *) + * {!Cil.saveBinaryFile}. Be aware that the varinfo vid and compinfo ckey + * fields shall be modified to avoid conflicts with the currently used + * varinfo and compinfo values. *) val loadBinaryFile : string -> file (** Get the global initializer and create one if it does not already exist.