diff --git a/dune-project b/dune-project index 6932d5aaa..424a6c1b6 100644 --- a/dune-project +++ b/dune-project @@ -35,7 +35,6 @@ This is a fork of the 'cil' package used for 'goblint'. Major changes include: conf-perl cppo conf-gcc - domain_shims ) (conflicts cil) ; only because we both install the cilly executable ) diff --git a/goblint-cil.opam b/goblint-cil.opam index d66c62b82..0a31ec7e0 100644 --- a/goblint-cil.opam +++ b/goblint-cil.opam @@ -42,7 +42,6 @@ depends: [ "conf-perl" "cppo" "conf-gcc" - "domain_shims" ] conflicts: ["cil"] build: [ diff --git a/src/dune b/src/dune index a804b0a1b..ef8e36031 100644 --- a/src/dune +++ b/src/dune @@ -3,7 +3,7 @@ (library (public_name goblint-cil) (name goblintCil) - (libraries zarith unix str stdlib-shims domain_shims) + (libraries zarith unix str stdlib-shims) (modules (:standard \ main mainFeature ciloptions machdepConfigure machdepArchConfigure modelConfigure)) ) diff --git a/src/ocamlutil/pretty.ml b/src/ocamlutil/pretty.ml index 0d7f0678f..9e34b39c5 100644 --- a/src/ocamlutil/pretty.ml +++ b/src/ocamlutil/pretty.ml @@ -41,13 +41,6 @@ structured text. *) -module DLS = Domain.DLS - -type 'a refDLS = 'a Domain.DLS.key -let refDLS vl = DLS.new_key (fun () -> vl) -let incrDLS rf = DLS.set rf (DLS.get rf + 1) -let decrDLS rf = DLS.set rf (DLS.get rf - 1) - let debug = false let fastMode = ref false @@ -267,63 +260,72 @@ type align = deltaFromPrev of the next active align *) } -(* We use references to avoid the need to pass data around all the time *) -let aligns: align list refDLS = (* The current stack of active alignment marks, - with the top at the head. Never empty. *) - refDLS [{ gainBreak = 0; isTaken = ref false; - deltaFromPrev = ref 0; deltaToNext = ref 0; }] +type state = { + mutable aligns: align list; + (** The current stack of active alignment marks, with the top at the head. Never empty. *) + + mutable topAlignAbsCol: int; + (** The absolute column of the top alignment *) + + mutable activeMarkups: int list; + (** We keep a list of active markup sections. For each one we keep the column we are in *) + + mutable breaks: bool ref list; + (** Keep a list of ref cells for the breaks, in the same order that we see them in the document *) + + mutable maxCol: int; + (** The maximum column that we should use *) + + mutable breakAllMode: bool; + (** Sometimes we take all the optional breaks *) + + mutable alignDepth: int; +} -let topAlignAbsCol = refDLS 0 (* The absolute column of the top alignment *) +let create_state (): state = { + aligns = [{ gainBreak = 0; isTaken = ref false; deltaFromPrev = ref 0; deltaToNext = ref 0; }]; + topAlignAbsCol = 0; + activeMarkups = []; + breaks = []; + maxCol = 0; + breakAllMode = false; + alignDepth = 0; +} -let pushAlign (abscol: int) = - let topalign = List.hd @@ DLS.get aligns in +let pushAlign ~state (abscol: int) = + let topalign = List.hd @@ state.aligns in let (res : align) = { gainBreak = 0; isTaken = ref false; deltaFromPrev = topalign.deltaToNext; (* Share with the previous *) deltaToNext = ref 0; (* Allocate a new ref *)} in - DLS.set aligns (res :: DLS.get aligns); - let newdelta = abscol - DLS.get topAlignAbsCol in + state.aligns <- res :: state.aligns; + let newdelta = abscol - state.topAlignAbsCol in res.deltaFromPrev := newdelta; - DLS.set topAlignAbsCol abscol + state.topAlignAbsCol <- abscol -let popAlign () = - match DLS.get aligns with +let popAlign ~state = + match state.aligns with top :: t when t != [] -> - DLS.set aligns t; - DLS.set topAlignAbsCol (DLS.get topAlignAbsCol - !(top.deltaFromPrev)) + state.aligns <- t; + state.topAlignAbsCol <- state.topAlignAbsCol - !(top.deltaFromPrev) | _ -> failwith "Unmatched unalign\n" -(** We keep a list of active markup sections. For each one we keep the column - we are in *) -let activeMarkups: int list refDLS = refDLS [] - - -(* Keep a list of ref cells for the breaks, in the same order that we see - them in the document *) -let breaks: bool ref list refDLS = refDLS [] - -(* The maximum column that we should use *) -let maxCol = refDLS 0 - -(* Sometimes we take all the optional breaks *) -let breakAllMode = refDLS false - (* We are taking a newline and moving left *) -let newline () = - let topalign = List.hd (DLS.get aligns) in (* aligns is never empty *) +let newline ~state = + let topalign = List.hd state.aligns in (* aligns is never empty *) if debug then dbgprintf "Taking a newline: reseting gain of %d\n" topalign.gainBreak; topalign.gainBreak <- 0; (* Erase the current break info *) - if (DLS.get breakAllMode) && DLS.get topAlignAbsCol < DLS.get maxCol then - DLS.set breakAllMode false; - DLS.get topAlignAbsCol (* This is the new column *) + if state.breakAllMode && state.topAlignAbsCol < state.maxCol then + state.breakAllMode <- false; + state.topAlignAbsCol (* This is the new column *) (* Choose the align with the best gain. We ought to find a better way to keep the aligns sorted, especially since they gain never changes (when the align is the top align) *) -let chooseBestGain () : align option = +let chooseBestGain ~state : align option = let bestGain = ref 0 in let rec loop (breakingAlign: align option) = function [] -> breakingAlign @@ -335,29 +337,29 @@ let chooseBestGain () : align option = end else loop breakingAlign resta in - loop None (DLS.get aligns) + loop None state.aligns (* We have just advanced to a new column. See if we must take a line break *) -let movingRight (abscol: int) : int = +let movingRight ~state (abscol: int) : int = (* Keep taking the best break until we get back to the left of maxCol or no more are left *) let rec tryAgain abscol = - if abscol <= DLS.get maxCol then abscol else + if abscol <= state.maxCol then abscol else begin if debug then dbgprintf "Looking for a break to take in column %d\n" abscol; (* Find the best gain there is out there *) - match if !fastMode then None else chooseBestGain () with + match if !fastMode then None else chooseBestGain ~state with None -> begin (* No breaks are available. Take all breaks from now on *) - DLS.set breakAllMode true; + state.breakAllMode <- true; if debug then dbgprintf "Can't find any breaks\n"; abscol end | Some breakingAlign -> begin - let topalign = List.hd (DLS.get aligns) in + let topalign = List.hd state.aligns in let theGain = breakingAlign.gainBreak in assert (theGain > 0); if debug then dbgprintf "Taking break at %d. gain=%d\n" abscol theGain; @@ -366,7 +368,7 @@ let movingRight (abscol: int) : int = if breakingAlign != topalign then begin breakingAlign.deltaToNext := !(breakingAlign.deltaToNext) - theGain; - DLS.set topAlignAbsCol (DLS.get topAlignAbsCol - theGain) + state.topAlignAbsCol <- state.topAlignAbsCol - theGain end; tryAgain (abscol - theGain) end @@ -379,88 +381,87 @@ let movingRight (abscol: int) : int = have properly nested align/unalign pairs. When the nesting depth surpasses !printDepth then we print ... and we skip until the matching unalign *) let printDepth = ref 10000000 (* WRW: must see whole thing *) -let alignDepth = refDLS 0 let useAlignDepth = true (** Start an align. Return true if we have just passed the threshhold *) -let enterAlign () = - incrDLS alignDepth; - useAlignDepth && DLS.get alignDepth = !printDepth + 1 +let enterAlign ~state = + state.alignDepth <- state.alignDepth + 1; + useAlignDepth && state.alignDepth = !printDepth + 1 (** Exit an align *) -let exitAlign () = - decrDLS alignDepth +let exitAlign ~state = + state.alignDepth <- state.alignDepth - 1 (** See if we are at a low-enough align level (and we should be printing normally) *) -let shallowAlign () = - not useAlignDepth || DLS.get alignDepth <= !printDepth +let shallowAlign ~state = + not useAlignDepth || state.alignDepth <= !printDepth (* Pass the current absolute column and compute the new column *) -let rec scan (abscol: int) (d: doc) : int = +let rec scan ~state (abscol: int) (d: doc) : int = match d with Nil -> abscol - | Concat (d1, d2) -> scan (scan abscol d1) d2 - | Text s when shallowAlign () -> + | Concat (d1, d2) -> scan ~state (scan ~state abscol d1) d2 + | Text s when shallowAlign ~state -> let sl = String.length s in if debug then dbgprintf "Done string: %s from %d to %d\n" s abscol (abscol + sl); - movingRight (abscol + sl) + movingRight ~state (abscol + sl) | CText (d, s) -> - let abscol' = scan abscol d in - if shallowAlign () then begin + let abscol' = scan ~state abscol d in + if shallowAlign ~state then begin let sl = String.length s in if debug then dbgprintf "Done string: %s from %d to %d\n" s abscol' (abscol' + sl); - movingRight (abscol' + sl) + movingRight ~state (abscol' + sl) end else abscol' | Align -> - pushAlign abscol; - if enterAlign () then - movingRight (abscol + 3) (* "..." *) + pushAlign ~state abscol; + if enterAlign ~state then + movingRight ~state (abscol + 3) (* "..." *) else abscol - | Unalign -> exitAlign (); popAlign (); abscol + | Unalign -> exitAlign ~state; popAlign ~state; abscol - | Line when shallowAlign () -> (* A forced line break *) - if DLS.get activeMarkups != [] then + | Line when shallowAlign ~state -> (* A forced line break *) + if state.activeMarkups != [] then failwith "Line breaks inside markup sections"; - newline () + newline ~state - | LeftFlush when shallowAlign () -> (* Keep cursor left-flushed *) 0 + | LeftFlush when shallowAlign ~state -> (* Keep cursor left-flushed *) 0 - | Break when shallowAlign () -> (* An optional line break. Always a space + | Break when shallowAlign ~state -> (* An optional line break. Always a space followed by an optional line break *) - if DLS.get activeMarkups != [] then + if state.activeMarkups != [] then failwith "Line breaks inside markup sections"; let takenref = ref false in - DLS.set breaks (takenref :: DLS.get breaks); - let topalign = List.hd (DLS.get aligns) in (* aligns is never empty *) - if DLS.get breakAllMode then begin + state.breaks <- takenref :: state.breaks; + let topalign = List.hd state.aligns in (* aligns is never empty *) + if state.breakAllMode then begin takenref := true; - newline () + newline ~state end else begin (* If there was a previous break there it stays not taken, forever. So we overwrite it. *) topalign.isTaken <- takenref; - topalign.gainBreak <- 1 + abscol - DLS.get topAlignAbsCol; + topalign.gainBreak <- 1 + abscol - state.topAlignAbsCol; if debug then dbgprintf "Registering a break at %d with gain %d\n" (1 + abscol) topalign.gainBreak; - movingRight (1 + abscol) + movingRight ~state (1 + abscol) end - | Mark -> DLS.set activeMarkups (abscol :: DLS.get activeMarkups); + | Mark -> state.activeMarkups <- abscol :: state.activeMarkups; abscol | Unmark -> begin - match DLS.get activeMarkups with - old :: rest -> DLS.set activeMarkups rest; + match state.activeMarkups with + old :: rest -> state.activeMarkups <- rest; old | [] -> failwith "Too many unmark" end @@ -470,10 +471,10 @@ let rec scan (abscol: int) (d: doc) : int = (** Keep a running counter of the newlines we are taking. You can read and reset this from user code, if you want *) -let countNewLines = refDLS 0 +let countNewLines = Atomic.make 0 (* The actual function that takes a document and prints it *) -let emitDoc +let emitDoc ~state (emitString: string -> int -> unit) (* emit a number of copies of a string *) (d: doc) = @@ -488,7 +489,7 @@ let emitDoc [] -> failwith "Ran out of aligns" | x :: _ -> emitString "\n" 1; - DLS.set countNewLines (DLS.get countNewLines + 1); + Atomic.incr countNewLines; wantIndent := true; x in @@ -510,7 +511,7 @@ let emitDoc | Concat (d1, d2) -> loopCont abscol d1 (fun abscol' -> loopCont abscol' d2 cont) - | Text s when shallowAlign () -> + | Text s when shallowAlign ~state -> let sl = String.length s in indentIfNeeded (); emitString s 1; @@ -519,7 +520,7 @@ let emitDoc | CText (d, s) -> loopCont abscol d (fun abscol' -> - if shallowAlign () then + if shallowAlign ~state then let sl = String.length s in indentIfNeeded (); emitString s 1; @@ -529,7 +530,7 @@ let emitDoc | Align -> aligns := (abscol :: !aligns); - if enterAlign () then begin + if enterAlign ~state then begin indentIfNeeded (); emitString "..." 1; cont (abscol + 3) @@ -540,16 +541,16 @@ let emitDoc match !aligns with [] -> failwith "Unmatched unalign" | _ :: rest -> - exitAlign (); + exitAlign ~state; aligns := rest; cont abscol end - | Line when shallowAlign () -> cont (newline ()) - | LeftFlush when shallowAlign () -> wantIndent := false; cont (0) - | Break when shallowAlign () -> begin - match DLS.get breaks with + | Line when shallowAlign ~state -> cont (newline ()) + | LeftFlush when shallowAlign ~state -> wantIndent := false; cont (0) + | Break when shallowAlign ~state -> begin + match state.breaks with [] -> failwith "Break without a takenref" | istaken :: rest -> - DLS.set breaks rest; (* Consume the break *) + state.breaks <- rest; (* Consume the break *) if !istaken then cont (newline ()) else begin indentIfNeeded (); @@ -559,12 +560,12 @@ let emitDoc end | Mark -> - DLS.set activeMarkups (abscol :: DLS.get activeMarkups); + state.activeMarkups <- abscol :: state.activeMarkups; cont abscol | Unmark -> begin - match DLS.get activeMarkups with - old :: rest -> DLS.set activeMarkups rest; + match state.activeMarkups with + old :: rest -> state.activeMarkups <- rest; cont old | [] -> failwith "Unmark without a mark" end @@ -577,51 +578,17 @@ let emitDoc let print_with_state ~width f = - (* Save some parameters, to allow for nested calls of these routines. *) - let old_maxCol = DLS.get maxCol in - DLS.set maxCol width; - let old_breaks = DLS.get breaks in - DLS.set breaks []; - let old_activeMarkups = DLS.get activeMarkups in - DLS.set activeMarkups []; - let old_alignDepth = DLS.get alignDepth in - DLS.set alignDepth 0; - let old_aligns = DLS.get aligns in - DLS.set aligns [{ gainBreak = 0; isTaken = ref false; deltaFromPrev = ref 0; deltaToNext = ref 0; }]; - let old_topAlignAbsCol = DLS.get topAlignAbsCol in - DLS.set topAlignAbsCol 0; - let old_breakAllMode = DLS.get breakAllMode in - DLS.set breakAllMode false; - - let finally () = - DLS.set maxCol old_maxCol; - (* We must do this especially if we don't do emit - (which consumes breaks) because otherwise we waste - memory *) - DLS.set breaks old_breaks; - DLS.set activeMarkups old_activeMarkups; - DLS.set alignDepth old_alignDepth; - DLS.set aligns old_aligns; - DLS.set topAlignAbsCol old_topAlignAbsCol; - DLS.set breakAllMode old_breakAllMode - in - - match f () with - | r -> - finally (); - r - | exception e -> - let bt = Printexc.get_raw_backtrace () in - finally (); - Printexc.raise_with_backtrace e bt + let state = create_state () in + state.maxCol <- width; + f ~state (* Print a document on a channel *) let fprint (chn: out_channel) ~(width: int) doc = let doc = if !flattenBeforePrint then flatten Nil doc else doc in - print_with_state ~width (fun () -> - ignore (scan 0 doc); - DLS.set breaks @@ List.rev (DLS.get breaks); - emitDoc (fun s nrcopies -> + print_with_state ~width (fun ~state -> + ignore (scan ~state 0 doc); + state.breaks <- List.rev state.breaks; + emitDoc ~state (fun s nrcopies -> for _ = 1 to nrcopies do output_string chn s done @@ -631,15 +598,15 @@ let fprint (chn: out_channel) ~(width: int) doc = (* Print the document to a string *) let sprint ~(width : int) doc : string = let doc = if !flattenBeforePrint then flatten Nil doc else doc in - print_with_state ~width (fun () -> - ignore (scan 0 doc); - DLS.set breaks @@ List.rev (DLS.get breaks); + print_with_state ~width (fun ~state -> + ignore (scan ~state 0 doc); + state.breaks <- List.rev state.breaks; let buf = Buffer.create 1024 in let rec add_n_strings str num = if num <= 0 then () else begin Buffer.add_string buf str; add_n_strings str (num - 1) end in - emitDoc add_n_strings doc; + emitDoc ~state add_n_strings doc; Buffer.contents buf ) @@ -654,18 +621,17 @@ let gprintf (finish : doc -> 'b) (format : ('a, unit, doc, 'b) format4) : 'a = let format = string_of_format format in - (* Record the starting align depth *) - let startAlignDepth = DLS.get alignDepth in + let alignDepth = ref 0 in (* Special concatenation functions *) let dconcat (acc: doc) (another: doc) = - if DLS.get alignDepth > !printDepth then acc else acc ++ another in + if !alignDepth > !printDepth then acc else acc ++ another in let dctext1 (acc: doc) (str: string) = - if DLS.get alignDepth > !printDepth then acc else + if !alignDepth > !printDepth then acc else CText(acc, str) in (* Special finish function *) let dfinish (dc: doc) : 'b = - if DLS.get alignDepth <> startAlignDepth then + if !alignDepth <> 0 then prerr_string ("Unmatched align/unalign in " ^ format ^ "\n"); finish dc in @@ -787,20 +753,20 @@ let gprintf (finish : doc -> 'b) (* Now the special format characters *) '[' -> (* align *) let newacc = - if DLS.get alignDepth > !printDepth then + if !alignDepth > !printDepth then acc - else if DLS.get alignDepth = !printDepth then + else if !alignDepth = !printDepth then CText(acc, "...") else acc ++ align in - incrDLS alignDepth; + incr alignDepth; collect newacc (i + 2) | ']' -> (* unalign *) - decrDLS alignDepth; + decr alignDepth; let newacc = - if DLS.get alignDepth >= !printDepth then + if !alignDepth >= !printDepth then acc else acc ++ unalign diff --git a/src/ocamlutil/pretty.mli b/src/ocamlutil/pretty.mli index 7857a87a8..a88d56393 100644 --- a/src/ocamlutil/pretty.mli +++ b/src/ocamlutil/pretty.mli @@ -52,9 +52,6 @@ (** API *) -(** refDLS is an alias for Domain.DLS.key *) -type 'a refDLS = 'a Domain.DLS.key - (** The type of unformated documents. Elements of this type can be constructed in two ways. Either with a number of constructor shown below, or using the {!Pretty.dprintf} function with a [printf]-like interface. @@ -315,7 +312,7 @@ val flattenBeforePrint : bool ref (** Keep a running count of the taken newlines. You can read and write this from the client code if you want *) -val countNewLines : int refDLS +val countNewLines : int Atomic.t (** A function that when used at top-level in a module will direct diff --git a/test/Makefile b/test/Makefile index 3463c0f77..189d391b8 100644 --- a/test/Makefile +++ b/test/Makefile @@ -276,7 +276,7 @@ else endif testrun/% : $(SMALL1)/%.ml - ocamlfind $(CAMLC) -I $(OBJDIR_DUNE) -I $(OBJDIR_MAKE) -package zarith -package domain_shims unix.$(CMXA) str.$(CMXA) zarith.$(CMXA) threads.$(CMXA) domain_shims.$(CMXA) -thread \ + ocamlfind $(CAMLC) -I $(OBJDIR_DUNE) -I $(OBJDIR_MAKE) -package zarith unix.$(CMXA) str.$(CMXA) zarith.$(CMXA) \ goblintCil.$(CMXA) \ $(EXEOUT) $(basename $<).exe $< $(basename $<).exe