diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 75e1c2235..4d86f39bb 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -16,13 +16,6 @@ jobs: - ubuntu-latest # - windows-latest ocaml-version: - - 4.05.0 - - 4.06.1 - - 4.07.1 - - 4.08.1 - - 4.09.1 - - 4.10.1 - - 4.11.2 - 4.12.0 - 4.13.1 - 4.14.x diff --git a/dune-project b/dune-project index 926628504..6932d5aaa 100644 --- a/dune-project +++ b/dune-project @@ -22,7 +22,7 @@ This is a fork of the 'cil' package used for 'goblint'. Major changes include: * Use dune instead of make and ocamlbuild. * Many bug fixes.") (depends - (ocaml (>= 4.05.0)) + (ocaml (>= 4.12.0)) (ocamlfind :with-test) zarith (hevea :with-doc) @@ -35,6 +35,7 @@ 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 0a1020506..d66c62b82 100644 --- a/goblint-cil.opam +++ b/goblint-cil.opam @@ -29,7 +29,7 @@ license: "BSD-3-Clause" homepage: "https://github.com/goblint/cil" bug-reports: "https://github.com/goblint/cil/issues" depends: [ - "ocaml" {>= "4.05.0"} + "ocaml" {>= "4.12.0"} "ocamlfind" {with-test} "zarith" "hevea" {with-doc} @@ -42,6 +42,7 @@ depends: [ "conf-perl" "cppo" "conf-gcc" + "domain_shims" ] conflicts: ["cil"] build: [ diff --git a/src/dune b/src/dune index ef8e36031..a804b0a1b 100644 --- a/src/dune +++ b/src/dune @@ -3,7 +3,7 @@ (library (public_name goblint-cil) (name goblintCil) - (libraries zarith unix str stdlib-shims) + (libraries zarith unix str stdlib-shims domain_shims) (modules (:standard \ main mainFeature ciloptions machdepConfigure machdepArchConfigure modelConfigure)) ) diff --git a/src/ocamlutil/pretty.ml b/src/ocamlutil/pretty.ml index 18fcb75c3..0d7f0678f 100644 --- a/src/ocamlutil/pretty.ml +++ b/src/ocamlutil/pretty.ml @@ -41,6 +41,13 @@ 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 @@ -261,54 +268,55 @@ type align = } (* We use references to avoid the need to pass data around all the time *) -let aligns: align list ref = (* The current stack of active alignment marks, +let aligns: align list refDLS = (* The current stack of active alignment marks, with the top at the head. Never empty. *) - ref [{ gainBreak = 0; isTaken = ref false; + refDLS [{ gainBreak = 0; isTaken = ref false; deltaFromPrev = ref 0; deltaToNext = ref 0; }] -let topAlignAbsCol = ref 0 (* The absolute column of the top alignment *) +let topAlignAbsCol = refDLS 0 (* The absolute column of the top alignment *) let pushAlign (abscol: int) = - let topalign = List.hd !aligns in - let res = + let topalign = List.hd @@ DLS.get 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 - aligns := res :: !aligns; - res.deltaFromPrev := abscol - !topAlignAbsCol; - topAlignAbsCol := abscol + DLS.set aligns (res :: DLS.get aligns); + let newdelta = abscol - DLS.get topAlignAbsCol in + res.deltaFromPrev := newdelta; + DLS.set topAlignAbsCol abscol let popAlign () = - match !aligns with + match DLS.get aligns with top :: t when t != [] -> - aligns := t; - topAlignAbsCol := !topAlignAbsCol - !(top.deltaFromPrev) + DLS.set aligns t; + DLS.set topAlignAbsCol (DLS.get 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 ref = ref [] +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 ref = ref [] +let breaks: bool ref list refDLS = refDLS [] (* The maximum column that we should use *) -let maxCol = ref 0 +let maxCol = refDLS 0 (* Sometimes we take all the optional breaks *) -let breakAllMode = ref false +let breakAllMode = refDLS false (* We are taking a newline and moving left *) let newline () = - let topalign = List.hd !aligns in (* aligns is never empty *) + let topalign = List.hd (DLS.get 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 !breakAllMode && !topAlignAbsCol < !maxCol then - breakAllMode := false; - !topAlignAbsCol (* This is the new column *) + if (DLS.get breakAllMode) && DLS.get topAlignAbsCol < DLS.get maxCol then + DLS.set breakAllMode false; + DLS.get topAlignAbsCol (* This is the new column *) @@ -327,7 +335,7 @@ let chooseBestGain () : align option = end else loop breakingAlign resta in - loop None !aligns + loop None (DLS.get aligns) (* We have just advanced to a new column. See if we must take a line break *) @@ -335,7 +343,7 @@ let movingRight (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 <= !maxCol then abscol else + if abscol <= DLS.get maxCol then abscol else begin if debug then dbgprintf "Looking for a break to take in column %d\n" abscol; @@ -343,13 +351,13 @@ let movingRight (abscol: int) : int = match if !fastMode then None else chooseBestGain () with None -> begin (* No breaks are available. Take all breaks from now on *) - breakAllMode := true; + DLS.set breakAllMode true; if debug then dbgprintf "Can't find any breaks\n"; abscol end | Some breakingAlign -> begin - let topalign = List.hd !aligns in + let topalign = List.hd (DLS.get aligns) in let theGain = breakingAlign.gainBreak in assert (theGain > 0); if debug then dbgprintf "Taking break at %d. gain=%d\n" abscol theGain; @@ -358,7 +366,7 @@ let movingRight (abscol: int) : int = if breakingAlign != topalign then begin breakingAlign.deltaToNext := !(breakingAlign.deltaToNext) - theGain; - topAlignAbsCol := !topAlignAbsCol - theGain + DLS.set topAlignAbsCol (DLS.get topAlignAbsCol - theGain) end; tryAgain (abscol - theGain) end @@ -371,23 +379,23 @@ 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 = ref 0 +let alignDepth = refDLS 0 let useAlignDepth = true (** Start an align. Return true if we have just passed the threshhold *) let enterAlign () = - incr alignDepth; - useAlignDepth && !alignDepth = !printDepth + 1 + incrDLS alignDepth; + useAlignDepth && DLS.get alignDepth = !printDepth + 1 (** Exit an align *) let exitAlign () = - decr alignDepth + decrDLS alignDepth (** See if we are at a low-enough align level (and we should be printing normally) *) let shallowAlign () = - not useAlignDepth || !alignDepth <= !printDepth + not useAlignDepth || DLS.get alignDepth <= !printDepth (* Pass the current absolute column and compute the new column *) @@ -420,7 +428,7 @@ let rec scan (abscol: int) (d: doc) : int = | Unalign -> exitAlign (); popAlign (); abscol | Line when shallowAlign () -> (* A forced line break *) - if !activeMarkups != [] then + if DLS.get activeMarkups != [] then failwith "Line breaks inside markup sections"; newline () @@ -428,31 +436,31 @@ let rec scan (abscol: int) (d: doc) : int = | Break when shallowAlign () -> (* An optional line break. Always a space followed by an optional line break *) - if !activeMarkups != [] then + if DLS.get activeMarkups != [] then failwith "Line breaks inside markup sections"; let takenref = ref false in - breaks := takenref :: !breaks; - let topalign = List.hd !aligns in (* aligns is never empty *) - if !breakAllMode then begin + 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 takenref := true; newline () 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 - !topAlignAbsCol; + topalign.gainBreak <- 1 + abscol - DLS.get topAlignAbsCol; if debug then dbgprintf "Registering a break at %d with gain %d\n" (1 + abscol) topalign.gainBreak; movingRight (1 + abscol) end - | Mark -> activeMarkups := abscol :: !activeMarkups; + | Mark -> DLS.set activeMarkups (abscol :: DLS.get activeMarkups); abscol | Unmark -> begin - match !activeMarkups with - old :: rest -> activeMarkups := rest; + match DLS.get activeMarkups with + old :: rest -> DLS.set activeMarkups rest; old | [] -> failwith "Too many unmark" end @@ -462,7 +470,7 @@ 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 = ref 0 +let countNewLines = refDLS 0 (* The actual function that takes a document and prints it *) let emitDoc @@ -480,8 +488,8 @@ let emitDoc [] -> failwith "Ran out of aligns" | x :: _ -> emitString "\n" 1; - incr countNewLines; - wantIndent := true; + DLS.set countNewLines (DLS.get countNewLines + 1); + wantIndent := true; x in (* Print indentation if wantIndent was previously flagged ; reset this flag *) @@ -520,7 +528,7 @@ let emitDoc cont abscol') | Align -> - aligns := abscol :: !aligns; + aligns := (abscol :: !aligns); if enterAlign () then begin indentIfNeeded (); emitString "..." 1; @@ -538,10 +546,10 @@ let emitDoc | Line when shallowAlign () -> cont (newline ()) | LeftFlush when shallowAlign () -> wantIndent := false; cont (0) | Break when shallowAlign () -> begin - match !breaks with + match DLS.get breaks with [] -> failwith "Break without a takenref" | istaken :: rest -> - breaks := rest; (* Consume the break *) + DLS.set breaks rest; (* Consume the break *) if !istaken then cont (newline ()) else begin indentIfNeeded (); @@ -551,12 +559,12 @@ let emitDoc end | Mark -> - activeMarkups := abscol :: !activeMarkups; + DLS.set activeMarkups (abscol :: DLS.get activeMarkups); cont abscol | Unmark -> begin - match !activeMarkups with - old :: rest -> activeMarkups := rest; + match DLS.get activeMarkups with + old :: rest -> DLS.set activeMarkups rest; cont old | [] -> failwith "Unmark without a mark" end @@ -570,32 +578,32 @@ let emitDoc let print_with_state ~width f = (* Save some parameters, to allow for nested calls of these routines. *) - let old_maxCol = !maxCol in - maxCol := width; - let old_breaks = !breaks in - breaks := []; - let old_activeMarkups = !activeMarkups in - activeMarkups := []; - let old_alignDepth = !alignDepth in - alignDepth := 0; - let old_aligns = !aligns in - aligns := [{ gainBreak = 0; isTaken = ref false; deltaFromPrev = ref 0; deltaToNext = ref 0; }]; - let old_topAlignAbsCol = !topAlignAbsCol in - topAlignAbsCol := 0; - let old_breakAllMode = !breakAllMode in - breakAllMode := false; + 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 () = - maxCol := old_maxCol; + DLS.set maxCol old_maxCol; (* We must do this especially if we don't do emit (which consumes breaks) because otherwise we waste memory *) - breaks := old_breaks; - activeMarkups := old_activeMarkups; - alignDepth := old_alignDepth; - aligns := old_aligns; - topAlignAbsCol := old_topAlignAbsCol; - breakAllMode := old_breakAllMode + 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 @@ -612,7 +620,7 @@ 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); - breaks := List.rev !breaks; + DLS.set breaks @@ List.rev (DLS.get breaks); emitDoc (fun s nrcopies -> for _ = 1 to nrcopies do output_string chn s @@ -625,7 +633,7 @@ 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); - breaks := List.rev !breaks; + DLS.set breaks @@ List.rev (DLS.get breaks); let buf = Buffer.create 1024 in let rec add_n_strings str num = if num <= 0 then () @@ -647,17 +655,17 @@ let gprintf (finish : doc -> 'b) let format = string_of_format format in (* Record the starting align depth *) - let startAlignDepth = !alignDepth in + let startAlignDepth = DLS.get alignDepth in (* Special concatenation functions *) let dconcat (acc: doc) (another: doc) = - if !alignDepth > !printDepth then acc else acc ++ another in + if DLS.get alignDepth > !printDepth then acc else acc ++ another in let dctext1 (acc: doc) (str: string) = - if !alignDepth > !printDepth then acc else + if DLS.get alignDepth > !printDepth then acc else CText(acc, str) in (* Special finish function *) let dfinish (dc: doc) : 'b = - if !alignDepth <> startAlignDepth then + if DLS.get alignDepth <> startAlignDepth then prerr_string ("Unmatched align/unalign in " ^ format ^ "\n"); finish dc in @@ -779,20 +787,20 @@ let gprintf (finish : doc -> 'b) (* Now the special format characters *) '[' -> (* align *) let newacc = - if !alignDepth > !printDepth then + if DLS.get alignDepth > !printDepth then acc - else if !alignDepth = !printDepth then + else if DLS.get alignDepth = !printDepth then CText(acc, "...") else acc ++ align in - incr alignDepth; + incrDLS alignDepth; collect newacc (i + 2) | ']' -> (* unalign *) - decr alignDepth; + decrDLS alignDepth; let newacc = - if !alignDepth >= !printDepth then + if DLS.get alignDepth >= !printDepth then acc else acc ++ unalign diff --git a/src/ocamlutil/pretty.mli b/src/ocamlutil/pretty.mli index 2f2ebd614..7857a87a8 100644 --- a/src/ocamlutil/pretty.mli +++ b/src/ocamlutil/pretty.mli @@ -52,6 +52,9 @@ (** 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. @@ -296,15 +299,15 @@ val withPrintDepth : int -> (unit -> unit) -> unit everything is replaced with ellipsis *) val printDepth : int ref -val printIndent : bool ref (** If false then does not indent *) +val printIndent : bool ref (** If false then does not indent *) (** If set to [true] then optional breaks are taken only when the document has exceeded the given width. This means that the printout will looked more ragged but it will be faster *) -val fastMode : bool ref +val fastMode : bool ref -val flushOften : bool ref (** If true the it flushes after every print *) +val flushOften : bool ref (** If true the it flushes after every print *) (** Whether to rebalance doc before printing it to avoid stack-overflows *) val flattenBeforePrint : bool ref @@ -312,7 +315,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 ref +val countNewLines : int refDLS (** A function that when used at top-level in a module will direct diff --git a/test/Makefile b/test/Makefile index 189d391b8..3463c0f77 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 unix.$(CMXA) str.$(CMXA) zarith.$(CMXA) \ + 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 \ goblintCil.$(CMXA) \ $(EXEOUT) $(basename $<).exe $< $(basename $<).exe