From a5f03d96eee482cd84861fc8cefff9eb451c0cad Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 29 Mar 2009 09:47:11 +0000 Subject: Cleaned up configure script. Distribution of CIL as an expanded source tree with changes applied (instead of original .tar.gz + patches to be applied at config time). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1020 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cil/ocamlutil/Makefile.ocaml | 395 +++++++++++++++++ cil/ocamlutil/Makefile.ocaml.build | 50 +++ cil/ocamlutil/alpha.ml | 156 +++++++ cil/ocamlutil/alpha.mli | 50 +++ cil/ocamlutil/clist.ml | 183 ++++++++ cil/ocamlutil/clist.mli | 97 +++++ cil/ocamlutil/errormsg.ml | 337 +++++++++++++++ cil/ocamlutil/errormsg.mli | 164 +++++++ cil/ocamlutil/growArray.ml | 191 +++++++++ cil/ocamlutil/growArray.mli | 131 ++++++ cil/ocamlutil/inthash.ml | 188 ++++++++ cil/ocamlutil/inthash.mli | 27 ++ cil/ocamlutil/intmap.ml | 171 ++++++++ cil/ocamlutil/intmap.mli | 87 ++++ cil/ocamlutil/perfcount.c.in | 184 ++++++++ cil/ocamlutil/pretty.ml | 859 +++++++++++++++++++++++++++++++++++++ cil/ocamlutil/pretty.mli | 316 ++++++++++++++ cil/ocamlutil/stats.ml | 146 +++++++ cil/ocamlutil/stats.mli | 72 ++++ cil/ocamlutil/trace.ml | 169 ++++++++ cil/ocamlutil/trace.mli | 106 +++++ cil/ocamlutil/util.ml | 815 +++++++++++++++++++++++++++++++++++ cil/ocamlutil/util.mli | 311 ++++++++++++++ 23 files changed, 5205 insertions(+) create mode 100644 cil/ocamlutil/Makefile.ocaml create mode 100644 cil/ocamlutil/Makefile.ocaml.build create mode 100755 cil/ocamlutil/alpha.ml create mode 100755 cil/ocamlutil/alpha.mli create mode 100644 cil/ocamlutil/clist.ml create mode 100644 cil/ocamlutil/clist.mli create mode 100644 cil/ocamlutil/errormsg.ml create mode 100644 cil/ocamlutil/errormsg.mli create mode 100644 cil/ocamlutil/growArray.ml create mode 100644 cil/ocamlutil/growArray.mli create mode 100755 cil/ocamlutil/inthash.ml create mode 100755 cil/ocamlutil/inthash.mli create mode 100755 cil/ocamlutil/intmap.ml create mode 100755 cil/ocamlutil/intmap.mli create mode 100755 cil/ocamlutil/perfcount.c.in create mode 100644 cil/ocamlutil/pretty.ml create mode 100644 cil/ocamlutil/pretty.mli create mode 100644 cil/ocamlutil/stats.ml create mode 100644 cil/ocamlutil/stats.mli create mode 100644 cil/ocamlutil/trace.ml create mode 100644 cil/ocamlutil/trace.mli create mode 100755 cil/ocamlutil/util.ml create mode 100644 cil/ocamlutil/util.mli (limited to 'cil/ocamlutil') diff --git a/cil/ocamlutil/Makefile.ocaml b/cil/ocamlutil/Makefile.ocaml new file mode 100644 index 00000000..1d0673fa --- /dev/null +++ b/cil/ocamlutil/Makefile.ocaml @@ -0,0 +1,395 @@ +# -*- Mode: makefile -*- +# Copyright (c) 2001-2002, +# George C. Necula +# Scott McPeak +# Wes Weimer +# All rights reserved. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are +# met: +# +# 1. Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# +# 2. Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# +# 3. The names of the contributors may not be used to endorse or promote +# products derived from this software without specific prior written +# permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +# IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED +# TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A +# PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER +# OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + + # Generic Makefile for Ocaml projects + # Written by necula@cs.berkeley.edu + # + # Features: + # - keeps byproducts of building in a separate directory + # - handles dependencies automatically + # - user specifies just what modules go into a project and + # everything else is done automatically + # - you can use one Makefile for several Ocaml projects + # + # You must include this file in your Makefile. Before the include point + # you must defined the following variables (which are glob al for all Ocaml + # projects specified in one Makefile): + # + # CAMLDIR - the directory where to get the ocaml executables from. + # Must be empty (defaul) or end with a / + # OBJDIR - the directory where to put all object files. This directory + # must exist (default obj) + # DEPENDDIR - the directory where to put dependency files. This directory + # must exist. (default obj/.depend) + # NATIVECAML - if set then will use the native compiler + # UNSAFE - if set then will turn off safety checks (only with NATIVECAML) + # PROFILE - if set then it will compile and link with "gprof" profiling + # support (NATIVECAML mode only) + # ASSEMBLY - if set then it will keep assembly files + # STATIC - if set then it will compile and link statically + # (NATIVECAML mode only) + # PREPROC - the preprocessor command + + # MODULES - a list of all modules for all projects defined in the + # Makefile. Give only the basenames (no directory, + # no extension). This is used to create the dependencies. + # SOURCEDIRS - a list of all directories containing sources for all + # projects defined in a Makefile. This is used to set vpath. + # MLLS - a list of all .mll (ocamllex input) files for all + # projects defined in the Makefile. + # MLYS - a list of all .mly (ocamlyacc input) files for all + # projects defined in the Makefile. + # ECHO - if specifically set to nothing then it will print + # all of the commands issued. Set this in the command line + # if you want to see what is going on. + # + # COMPILEFLAGS - if defined, then it is passed as argument to ocamlc + # and ocamlopt + # LINKFLAGS - if defined, then it is passed as argument to + # ocamlc and ocamlopt, when linking (at start of + # command line) + # + # CAML_CFLAGS - flags used only for the compilation of C files. + # e.g. '-ccopt ' + # + # + # After you set all of the above you must do the following for EACH separate + # executable that you want to build. + # + # Define the following: + # PROJECT_EXECUTABLE - the name of the executable you want to build. To take + # advantage of the naming scheme that separates the + # bytecode version and the native version, use the + # $(EXE) variable which is defined to either .byte.exe + # or .asm.exe. I typically put the executable in + # $(OBJDIR) as well. + # PROJECT_MODULES - the base names of the modules that make this + # executable in the order in which they must be + # passed to the linker. Make sure that all of + # the names mentioned here are also mentioned in + # MODULES. + # PROJECT_CMODULES - same as modules but for the C modules. These + # do not need to be mentioned in MODULES. There must be + # no name clashes with MODULES + # PROJECT_LIBS - the base names of the libraries that you + # want to link in the executable. + # + # + # Then include Makefile.ocaml.build to generate a customized + # rule for making your executable. + # + # Example: + # + # OBJDIR = obj + # DEPENDDIR = obj/.depend + # SOURCEDIRS = src src/special + # MLLS = mylex + # MLYS = myparse + # + # MODULES = mod11 mod12 mod21 modcommon + # + # # Rules for project 1 + # PROJECT_EXECUTABLE = $(OBJDIR)/proj1$(EXE) + # PROJECT_MODULES = mod11 mod12 modcommon + # PROJECT_CMODULES = + # PROJEC_LIBS = unix + # include Makefile.ocaml.build + # + # + # # Rules for project 2 + # PROJECT_EXECUTABLE = $(OBJDIR)/proj2$(EXE) + # PROJECT_MODULES = mod21 modcommon + # PROJECT_CMODULES = + # PROJEC_LIBS = unix str + # include Makefile.ocaml.build + + +CAMLLEX = ocamllex +CAMLYACC= ocamlyacc -v +CAMLDEP = ocamldep + +COMPILEFLAGS += -I $(OBJDIR) + +# sm: two styles for echoing compilation progress: +# style 1, by George: +# - print English descriptions of what's happening +# - set ECHO to "" to see *everything* +# style 2, by Scott: +# - do not print English descriptions +# - print every shell command that is executed which has a side effect, +# so that they could be pasted into a shell to reproduce manually +# - omit some of the details of dependency generation +# +# to be able to choose which style, several variables are used: +# @$(NARRATIVE) - put this before English descriptions for style 1 +# @$(COMMAND) - put this before shell commands which are to be +# printed for style 2; the command is *not* executed +# $(AT) - put this before shell commands which are to be executed, +# and also printed in style 2 +# $(ECHO) - use in place of '@' for things not printed in either style +ifdef ECHOSTYLE_SCOTT + # 'true' silently consumes its arguments, whereas 'echo' prints them + NARRATIVE := true + COMMAND := echo + AT := + ECHO := @ +else + NARRATIVE := echo + COMMAND := true + # change these next two definitions to to echo everything, + # or leave as @ to suppress echoing + AT := @ + ECHO := @ +endif + +ifdef PREPROC + COMPILEFLAGS += -pp "$(PREPROC)$" + DEPFLAGS += -pp "$(PREPROC)" +endif + +COMPILEMSG= +LINKMSG= + +ifdef WIN32 +OBJ = obj +else +OBJ = o +endif +EXE = $(EXEEXT).exe + + +export EXE + +ifdef NATIVECAML + ifdef PROFILE + COMPILEFLAGS += -p + LINKFLAGS += -p + COMPILEMSG += (profile) + LINKMSG += (profile) + endif + ifdef ASSEMBLY + COMPILEFLAGS += -S + endif + ifdef STATIC + COMPILEFLAGS += -ccopt -static + LINKFLAGS += -ccopt -static + endif + #foo := $(shell echo "I am in NATIVECAML mode" >&2; echo whatever) + ifdef WIN32 + COMPILEFLAGS += -ccopt /Ox + else + COMPILEFLAGS += -ccopt -O3 + endif + CAMLC = $(CAMLDIR)ocamlopt $(COMPILEFLAGS) + CAMLLINK = $(CAMLDIR)ocamlopt $(LINKFLAGS) + CMO = cmx + CMC = opt.$(OBJ) # compiled (and optimized) C + CMXA = cmxa + EXEEXT = .asm + MOVEAFTERCAMLC = cmi cmx $(OBJ) + COMPILETOWHAT = native code + # sm: by adding -native in native mode, we prevent spurious + # dependencies on .cmo files which were causing lots of + # extra recompilation + CAMLDEP = $(CAMLDIR)ocamldep -native +else + CMO = cmo + CMXA = cma + CMC = $(OBJ) + EXEEXT = .byte + MOVEAFTERCAMLC = cmi cmo + COMPILETOWHAT = bytecode + ifdef WIN32 + COMPILEFLAGS += -ccopt /Zi -ccopt /Od + LINKFLAGS += -ccopt /Zi -ccopt /Od + else + COMPILEFLAGS += -g -ccopt -g + LINKFLAGS += -g -ccopt -g + endif + CAMLC = $(CAMLDIR)ocamlc -g $(COMPILEFLAGS) + CAMLLINK = $(CAMLDIR)ocamlc -custom $(LINKFLAGS) +endif + + +ifdef UNSAFE + CAMLC := $(CAMLC) -unsafe -noassert +endif + + + + + # Allow searching for .ml and .mli +vpath %.mll $(SOURCEDIRS) +vpath %.mly $(SOURCEDIRS) +vpath %.ml $(SOURCEDIRS) $(OBJDIR) +vpath %.mli $(SOURCEDIRS) $(OBJDIR) +vpath %.c $(SOURCEDIRS) + + +# Secondaries are intermediates that we don't want make to delete +# By giving the right names to secondary files we tell make where to make +# them if they are not already made. VERY USEFUL!! +.SECONDARY : $(MLLS:%.mll=$(OBJDIR)/%.ml) $(MLYS:%.mly=$(OBJDIR)/%.ml) \ + $(MLYS:%.mly=$(OBJDIR)/%.mli) + + # Run the lexer generator + # Move the result to the OBJDIR directory + # If there is a .mli file in the same directory with .mll then + # copy it to OBJDIR (where the .ml) file will live. +$(OBJDIR)/%.ml: %.mll + $(CAMLLEX) $< + $(AT)mv -f $(basename $<).ml $(OBJDIR)/ + $(ECHO)if test -f $(basename $<).mli ;then \ + $(COMMAND) cp -f $(basename $<).mli $(OBJDIR)/; \ + cp -f $(basename $<).mli $(OBJDIR)/ \ + ;fi + + # Run the parser generator + # Move the result to the $(OBJDIR) directory. +$(OBJDIR)/%.ml $(OBJDIR)/%.mli: %.mly + $(CAMLYACC) $(CAMLYACCFLAGS) $< + $(AT)mv -f $(basename $<).ml $(basename $<).mli $(OBJDIR)/ + + # Compile an MLI file. After compilation move the result to OBJDIR +$(OBJDIR)/%.cmi: %.mli + @$(NARRATIVE) Compiling interface $< + $(AT)$(CAMLC) $(COMPILEFLAGS) -c $< + $(ECHO)if test $(OBJDIR) != $() { s%[^/\\ :]*/% %g; s%[^/\\ :]+\\% %g; s%([-a-zA-Z0-9+-.:/\/_]+)%\$$(OBJDIR)/$$1%g; print $$_;}' +# FIXDEPEND:=cat + +DEPINCLUDES= -I $(OBJDIR) $(SOURCEDIRS:%=-I %) +$(DEPENDDIR)/%.d: %.ml + @$(NARRATIVE) Generating dependency information for $< + @$(COMMAND) $(CAMLDEP) $(DEPFLAGS) $(DEPINCLUDES) $< + $(ECHO)$(CAMLDEP) $(DEPFLAGS) $(DEPINCLUDES) $< | $(FIXDEPEND) > $@ + +$(DEPENDDIR)/%.di: %.mli + @$(NARRATIVE) Generating dependency information for $< + @$(COMMAND) $(CAMLDEP) $(DEPFLAGS) $(DEPINCLUDES) $< + $(ECHO)$(CAMLDEP) $(DEPFLAGS) $(DEPINCLUDES) $< | $(FIXDEPEND) > $@ + +# sm: it turns out there's a variable which lists all the goals +# specified on the command line; I'll use this to set CLEANING +# (which is not set anywhere else, currently) +ifeq ($(MAKECMDGOALS),clean) + #$(warning "Skipping dependency rules because we're cleaning") + CLEANING := 1 +endif + +ifndef CLEANING +-include $(MODULES:%=$(DEPENDDIR)/%.d) +-include $(MODULES:%=$(DEPENDDIR)/%.di) +endif + +listmodules: + @echo $(MODULES) diff --git a/cil/ocamlutil/Makefile.ocaml.build b/cil/ocamlutil/Makefile.ocaml.build new file mode 100644 index 00000000..5271e461 --- /dev/null +++ b/cil/ocamlutil/Makefile.ocaml.build @@ -0,0 +1,50 @@ +# -*- Mode: makefile -*- +# Copyright (c) 2001-2002, +# George C. Necula +# Scott McPeak +# Wes Weimer +# All rights reserved. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are +# met: +# +# 1. Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# +# 2. Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# +# 3. The names of the contributors may not be used to endorse or promote +# products derived from this software without specific prior written +# permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +# IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED +# TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A +# PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER +# OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + + # Auxiliary Makefile for building Ocaml project. See the documentation in + # the associated Makefile.ocaml for how to use this file. + # Written by necula@cs.berkeley.edu + # +$(PROJECT_EXECUTABLE) : $(PROJECT_MODULES:%=$(OBJDIR)/%.$(CMO)) \ + $(PROJECT_CMODULES:%=$(OBJDIR)/%.$(CMC)) + @$(NARRATIVE) "Linking $(COMPILETOWHAT) $@ $(LINKMSG)" + $(AT)$(CAMLLINK) -verbose -o $@ \ + $(PROJECT_LIBS:%=%.$(CMXA)) \ + $(PROJECT_LIBS:%=-cclib -l%) \ + $^ + + + + + diff --git a/cil/ocamlutil/alpha.ml b/cil/ocamlutil/alpha.ml new file mode 100755 index 00000000..6a1ea017 --- /dev/null +++ b/cil/ocamlutil/alpha.ml @@ -0,0 +1,156 @@ +module H = Hashtbl +module E = Errormsg +open Pretty + +let debugAlpha (prefix: string) = false +(*** Alpha conversion ***) +let alphaSeparator = "___" +let alphaSeparatorLen = String.length alphaSeparator + +(** For each prefix we remember the next integer suffix to use and the list + * of suffixes, each with some data assciated with the newAlphaName that + * created the suffix. *) +type 'a alphaTableData = int * (string * 'a) list + +type 'a undoAlphaElement = + AlphaChangedSuffix of 'a alphaTableData ref * 'a alphaTableData (* The + * reference that was changed and + * the old suffix *) + | AlphaAddedSuffix of string (* We added this new entry to the + * table *) + +(* Create a new name based on a given name. The new name is formed from a + * prefix (obtained from the given name by stripping a suffix consisting of + * the alphaSeparator followed by only digits), followed by alphaSeparator + * and then by a positive integer suffix. The first argument is a table + * mapping name prefixes to the largest suffix used so far for that + * prefix. The largest suffix is one when only the version without suffix has + * been used. *) +let rec newAlphaName ~(alphaTable: (string, 'a alphaTableData ref) H.t) + ~(undolist: 'a undoAlphaElement list ref option) + ~(lookupname: string) + ~(data: 'a) : string * 'a = + alphaWorker ~alphaTable:alphaTable ~undolist:undolist + ~lookupname:lookupname ~data:data true + + +(** Just register the name so that we will not use in the future *) +and registerAlphaName ~(alphaTable: (string, 'a alphaTableData ref) H.t) + ~(undolist: 'a undoAlphaElement list ref option) + ~(lookupname: string) + ~(data: 'a) : unit = + ignore (alphaWorker ~alphaTable:alphaTable ~undolist:undolist + ~lookupname:lookupname ~data:data false) + + +and alphaWorker ~(alphaTable: (string, 'a alphaTableData ref) H.t) + ~(undolist: 'a undoAlphaElement list ref option) + ~(lookupname: string) ~(data:'a) + (make_new: bool) : string * 'a = + let prefix, suffix, (numsuffix: int) = splitNameForAlpha ~lookupname in + if debugAlpha prefix then + ignore (E.log "Alpha worker: prefix=%s suffix=%s (%d) create=%b. " + prefix suffix numsuffix make_new); + let newname, (olddata: 'a) = + try + let rc = H.find alphaTable prefix in + let max, suffixes = !rc in + (* We have seen this prefix *) + if debugAlpha prefix then + ignore (E.log " Old max %d. Old suffixes: @[%a@]" max + (docList + (fun (s, l) -> dprintf "%s" (* d_loc l *) s)) suffixes); + (* Save the undo info *) + (match undolist with + Some l -> l := AlphaChangedSuffix (rc, !rc) :: !l + | _ -> ()); + + let newmax, newsuffix, (olddata: 'a), newsuffixes = + if numsuffix > max then begin + (* Clearly we have not seen it *) + numsuffix, suffix, data, + (suffix, data) :: suffixes + end else begin + match List.filter (fun (n, _) -> n = suffix) suffixes with + [] -> (* Not found *) + max, suffix, data, (suffix, data) :: suffixes + | [(_, l) ] -> + (* We have seen this exact suffix before *) + if make_new then + let newsuffix = alphaSeparator ^ (string_of_int (max + 1)) in + max + 1, newsuffix, l, (newsuffix, data) :: suffixes + else + max, suffix, data, suffixes + | _ -> E.s (E.bug "Cil.alphaWorker") + end + in + rc := (newmax, newsuffixes); + prefix ^ newsuffix, olddata + with Not_found -> begin (* First variable with this prefix *) + (match undolist with + Some l -> l := AlphaAddedSuffix prefix :: !l + | _ -> ()); + H.add alphaTable prefix (ref (numsuffix, [ (suffix, data) ])); + if debugAlpha prefix then ignore (E.log " First seen. "); + lookupname, data (* Return the original name *) + end + in + if debugAlpha prefix then + ignore (E.log " Res=: %s \n" newname (* d_loc oldloc *)); + newname, olddata + +(* Strip the suffix. Return the prefix, the suffix (including the separator + * and the numeric value, possibly empty), and the + * numeric value of the suffix (possibly -1 if missing) *) +and splitNameForAlpha ~(lookupname: string) : (string * string * int) = + let len = String.length lookupname in + (* Search backward for the numeric suffix. Return the first digit of the + * suffix. Returns len if no numeric suffix *) + let rec skipSuffix (i: int) = + if i = -1 then -1 else + let c = Char.code (String.get lookupname i) - Char.code '0' in + if c >= 0 && c <= 9 then + skipSuffix (i - 1) + else (i + 1) + in + let startSuffix = skipSuffix (len - 1) in + + if startSuffix >= len (* No digits at all at the end *) || + startSuffix <= alphaSeparatorLen (* Not enough room for a prefix and + * the separator before suffix *) || + (* Suffix starts with a 0 and has more characters after that *) + (startSuffix < len - 1 && String.get lookupname startSuffix = '0') || + alphaSeparator <> String.sub lookupname + (startSuffix - alphaSeparatorLen) + alphaSeparatorLen + then + (lookupname, "", -1) (* No valid suffix in the name *) + else + (String.sub lookupname 0 (startSuffix - alphaSeparatorLen), + String.sub lookupname (startSuffix - alphaSeparatorLen) + (len - startSuffix + alphaSeparatorLen), + int_of_string (String.sub lookupname startSuffix (len - startSuffix))) + + +let getAlphaPrefix ~(lookupname:string) : string = + let p, _, _ = splitNameForAlpha ~lookupname:lookupname in + p + +(* Undoes the changes as specified by the undolist *) +let undoAlphaChanges ~(alphaTable: (string, 'a alphaTableData ref) H.t) + ~(undolist: 'a undoAlphaElement list) = + List.iter + (function + AlphaChangedSuffix (where, old) -> + where := old + | AlphaAddedSuffix name -> + if debugAlpha name then + ignore (E.log "Removing %s from alpha table\n" name); + H.remove alphaTable name) + undolist + +let docAlphaTable () (alphaTable: (string, 'a alphaTableData ref) H.t) = + let acc : (string * (int * (string * 'a) list)) list ref = ref [] in + H.iter (fun k d -> acc := (k, !d) :: !acc) alphaTable; + docList ~sep:line (fun (k, (d, _)) -> dprintf " %s -> %d" k d) () !acc + diff --git a/cil/ocamlutil/alpha.mli b/cil/ocamlutil/alpha.mli new file mode 100755 index 00000000..e1e430dc --- /dev/null +++ b/cil/ocamlutil/alpha.mli @@ -0,0 +1,50 @@ +(** {b ALPHA conversion} *) + +(** This is the type of the elements that are recorded by the alpha + * conversion functions in order to be able to undo changes to the tables + * they modify. Useful for implementing + * scoping *) +type 'a undoAlphaElement + +(** This is the type of the elements of the alpha renaming table. These + * elements can carry some data associated with each occurrence of the name. *) +type 'a alphaTableData + + +(** Create a new name based on a given name. The new name is formed from a + * prefix (obtained from the given name by stripping a suffix consisting of _ + * followed by only digits), followed by a special separator and then by a + * positive integer suffix. The first argument is a table mapping name + * prefixes to some data that specifies what suffixes have been used and how + * to create the new one. This function updates the table with the new + * largest suffix generated. The "undolist" argument, when present, will be + * used by the function to record information that can be used by + * {!Alpha.undoAlphaChanges} to undo those changes. Note that the undo + * information will be in reverse order in which the action occurred. Returns + * the new name and, if different from the lookupname, the location of the + * previous occurrence. This function knows about the location implicitly + * from the {!Cil.currentLoc}. *) +val newAlphaName: alphaTable:(string, 'a alphaTableData ref) Hashtbl.t -> + undolist: 'a undoAlphaElement list ref option -> + lookupname:string -> data:'a -> string * 'a + + +(** Register a name with an alpha conversion table to ensure that when later + * we call newAlphaName we do not end up generating this one *) +val registerAlphaName: alphaTable:(string, 'a alphaTableData ref) Hashtbl.t -> + undolist: 'a undoAlphaElement list ref option -> + lookupname:string -> data:'a -> unit + +(** Split the name in preparation for newAlphaName. The prefix returned is + used to index into the hashtable. The next result value is a separator + (either empty or the separator chosen to separate the original name from + the index) *) +val docAlphaTable: unit -> + (string, 'a alphaTableData ref) Hashtbl.t -> Pretty.doc + + +val getAlphaPrefix: lookupname:string -> string + +(** Undo the changes to a table *) +val undoAlphaChanges: alphaTable:(string, 'a alphaTableData ref) Hashtbl.t -> + undolist:'a undoAlphaElement list -> unit diff --git a/cil/ocamlutil/clist.ml b/cil/ocamlutil/clist.ml new file mode 100644 index 00000000..80f0fd64 --- /dev/null +++ b/cil/ocamlutil/clist.ml @@ -0,0 +1,183 @@ +(* + * + * Copyright (c) 2001-2002, + * George C. Necula + * Scott McPeak + * Wes Weimer + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * + * 3. The names of the contributors may not be used to endorse or promote + * products derived from this software without specific prior written + * permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS + * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED + * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A + * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER + * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + *) + +open Pretty + + +(* We often need to concatenate sequences and using lists for this purpose is + * expensive. So we define a kind of "concatenable lists" that are easier to + * concatenate *) +type 'a clist = + | CList of 'a list (* This is the only representation for empty + * *) + | CConsL of 'a * 'a clist + | CConsR of 'a clist * 'a + | CSeq of 'a clist * 'a clist (* We concatenate only two of them at this + * time. Neither is CEmpty. To be sure + * always use append to make these *) + +let rec listifyOnto (tail: 'a list) = function + CList l -> l @ tail + | CConsL (x, l) -> x :: listifyOnto tail l + | CConsR (l, x) -> listifyOnto (x :: tail) l + | CSeq (l1, l2) -> listifyOnto (listifyOnto tail l2) l1 + +let toList l = listifyOnto [] l +let fromList l = CList l + + +let single x = CList [x] +let empty = CList [] + +let checkBeforeAppend (l1: 'a clist) (l2: 'a clist) : bool = + l1 != l2 || l1 = (CList []) + +let append l1 l2 = + if l1 = CList [] then l2 else + if l2 = CList [] then l1 else + begin + if l1 == l2 then + raise (Failure "You should not use Clist.append to double a list"); + CSeq (l1, l2) + end + +let rec length (acc: int) = function + CList l -> acc + (List.length l) + | CConsL (x, l) -> length (acc + 1) l + | CConsR (l, _) -> length (acc + 1) l + | CSeq (l1, l2) -> length (length acc l1) l2 +let length l = length 0 l (* The external version *) + +let map (f: 'a -> 'b) (l: 'a clist) : 'b clist = + let rec loop = function + CList l -> CList (List.map f l) + | CConsL (x, l) -> let x' = f x in CConsL (x', loop l) + | CConsR (l, x) -> let l' = loop l in CConsR (l', f x) + | CSeq (l1, l2) -> let l1' = loop l1 in CSeq (l1', loop l2) + in + loop l + + +let fold_left (f: 'acc -> 'a -> 'acc) (start: 'acc) (l: 'a clist) = + let rec loop (start: 'acc) = function + CList l -> List.fold_left f start l + | CConsL (x, l) -> loop (f start x) l + | CConsR (l, x) -> let res = loop start l in f res x + | CSeq (l1, l2) -> + let res1 = loop start l1 in + loop res1 l2 + in + loop start l + +let iter (f: 'a -> unit) (l: 'a clist) : unit = + let rec loop = function + CList l -> List.iter f l + | CConsL (x, l) -> f x; loop l + | CConsR (l, x) -> loop l; f x + | CSeq (l1, l2) -> loop l1; loop l2 + in + loop l + + +let rec rev (revelem: 'a -> 'a) = function + CList l -> + let rec revonto (tail: 'a list) = function + [] -> tail + | x :: rest -> revonto (revelem x :: tail) rest + in + CList (revonto [] l) + + | CConsL (x, l) -> CConsR (rev revelem l, x) + | CConsR (l, x) -> CConsL (x, rev revelem l) + | CSeq (l1, l2) -> CSeq (rev revelem l2, rev revelem l1) + + +let docCList (sep: doc) (doone: 'a -> doc) () (dl: 'a clist) = + fold_left + (fun (acc: doc) (elem: 'a) -> + let elemd = doone elem in + if acc == nil then elemd else acc ++ sep ++ elemd) + nil + dl + + +(* let debugCheck (lst: 'a clist) : unit =*) +(* (* use a hashtable to store values encountered *)*) +(* let tbl : 'a bool H.t = (H.create 13) in*) + +(* letrec recurse (node: 'a clist) =*) +(* (* have we seen*)*) + +(* match node with*) +(* | CList*) + + +(* --------------- testing ----------------- *) +type boxedInt = + | BI of int + | SomethingElse + +let d_boxedInt () b = + match b with + | BI(i) -> (dprintf "%d" i) + | SomethingElse -> (text "somethingElse") + + +(* sm: some simple tests of CLists +let testCList () : unit = +begin + (trace "sm" (dprintf "in testCList\n")); + + let clist1 = (fromList [BI(1); BI(2); BI(3)]) in + (trace "sm" (dprintf "length of clist1 is %d\n" + (length clist1) )); + + let flattened = (toList clist1) in + (trace "sm" (dprintf "flattened: %a\n" + (docList ~sep:(chr ',' ++ break) (d_boxedInt ())) + flattened)); + + +end +1) in + (trace "sm" (dprintf "flattened: %a\n" + (docList ~sep:(chr ',' ++ break) (d_boxedInt ())) + flattened)); + + +end +*) diff --git a/cil/ocamlutil/clist.mli b/cil/ocamlutil/clist.mli new file mode 100644 index 00000000..c0378a60 --- /dev/null +++ b/cil/ocamlutil/clist.mli @@ -0,0 +1,97 @@ +(* + * + * Copyright (c) 2001-2002, + * George C. Necula + * Scott McPeak + * Wes Weimer + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * + * 3. The names of the contributors may not be used to endorse or promote + * products derived from this software without specific prior written + * permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS + * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED + * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A + * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER + * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + *) + +(** Utilities for managing "concatenable lists" (clists). We often need to + concatenate sequences, and using lists for this purpose is expensive. This + module provides routines to manage such lists more efficiently. In this + model, we never do cons or append explicitly. Instead we maintain + the elements of the list in a special data structure. Routines are provided + to convert to/from ordinary lists, and carry out common list operations.*) + +(** The clist datatype. A clist can be an ordinary list, or a clist preceded + or followed by an element, or two clists implicitly appended together*) +type 'a clist = + | CList of 'a list (** The only representation for the empty + list. Try to use sparingly. *) + | CConsL of 'a * 'a clist (** Do not use this a lot because scanning + * it is not tail recursive *) + | CConsR of 'a clist * 'a + | CSeq of 'a clist * 'a clist (** We concatenate only two of them at this + time. Neither is the empty clist. To be + sure always use append to make these *) + + +(** Convert a clist to an ordinary list *) +val toList: 'a clist -> 'a list + +(** Convert an ordinary list to a clist *) +val fromList: 'a list -> 'a clist + +(** Create a clist containing one element *) +val single: 'a -> 'a clist + +(** The empty clist *) +val empty: 'a clist + + +(** Append two clists *) +val append: 'a clist -> 'a clist -> 'a clist + +(** A useful check to assert before an append. It checks that the two lists + * are not identically the same (Except if they are both empty) *) +val checkBeforeAppend: 'a clist -> 'a clist -> bool + +(** Find the length of a clist *) +val length: 'a clist -> int + +(** Map a function over a clist. Returns another clist *) +val map: ('a -> 'b) -> 'a clist -> 'b clist + + +(** A version of fold_left that works on clists *) +val fold_left: ('acc -> 'a -> 'acc) -> 'acc -> 'a clist -> 'acc + +(** A version of iter that works on clists *) +val iter: ('a -> unit) -> 'a clist -> unit + +(** Reverse a clist. The first function reverses an element. *) +val rev: ('a -> 'a) -> 'a clist -> 'a clist + +(** A document for printing a clist (similar to [docList]) *) +val docCList: + Pretty.doc -> ('a -> Pretty.doc) -> unit -> 'a clist -> Pretty.doc + diff --git a/cil/ocamlutil/errormsg.ml b/cil/ocamlutil/errormsg.ml new file mode 100644 index 00000000..07e935d4 --- /dev/null +++ b/cil/ocamlutil/errormsg.ml @@ -0,0 +1,337 @@ +(* + * + * Copyright (c) 2001-2002, + * George C. Necula + * Scott McPeak + * Wes Weimer + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * + * 3. The names of the contributors may not be used to endorse or promote + * products derived from this software without specific prior written + * permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS + * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED + * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A + * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER + * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + *) + +open Pretty + + + +let debugFlag = ref false (* If set then print debugging info *) +let verboseFlag = ref false + +(**** Error reporting ****) +exception Error +let s (d : 'a) = raise Error + +let hadErrors = ref false + +let errorContext = ref [] +let pushContext f = errorContext := f :: (!errorContext) +let popContext () = + match !errorContext with + _ :: t -> errorContext := t + | [] -> s (eprintf "Bug: cannot pop error context") + + +let withContext ctx f x = + pushContext ctx; + try + let res = f x in + popContext (); + res + with e -> begin + popContext (); + raise e + end + + (* Make sure that showContext calls + * each f with its appropriate + * errorContext as it was when it was + * pushed *) +let showContext () = + let rec loop = function + [] -> () + | f :: rest -> (errorContext := rest; (* Just in case f raises an error *) + ignore (eprintf " Context : %t@!" f); + loop rest) + in + let old = !errorContext in + try + loop old; + errorContext := old + with e -> begin + errorContext := old; + raise e + end + +let contextMessage (name: string) (d: doc) = + ignore (eprintf "@!%s: %a@!" name insert d); + showContext () + +let warnFlag = ref false + +let logChannel : out_channel ref = ref stderr + + +let bug (fmt : ('a,unit,doc,unit) format4) : 'a = + let f d = + hadErrors := true; contextMessage "Bug" d; + flush !logChannel + in + Pretty.gprintf f fmt + +let error (fmt : ('a,unit,doc,unit) format4) : 'a = + let f d = hadErrors := true; contextMessage "Error" d; + flush !logChannel + in + Pretty.gprintf f fmt + +let unimp (fmt : ('a,unit,doc,unit) format4) : 'a = + let f d = hadErrors := true; contextMessage "Unimplemented" d; + flush !logChannel + in + Pretty.gprintf f fmt + +let warn (fmt : ('a,unit,doc,unit) format4) : 'a = + let f d = contextMessage "Warning" d; flush !logChannel in + Pretty.gprintf f fmt + +let warnOpt (fmt : ('a,unit,doc,unit) format4) : 'a = + let f d = + if !warnFlag then contextMessage "Warning" d; + flush !logChannel in + Pretty.gprintf f fmt + + +let log (fmt : ('a,unit,doc,unit) format4) : 'a = + let f d = fprint !logChannel 80 d; flush !logChannel in + Pretty.gprintf f fmt + +let logg (fmt : ('a,unit,doc,unit) format4) : 'a = + let f d = fprint !logChannel 10000000 d; flush !logChannel in + Pretty.gprintf f fmt + +let null (fmt : ('a,unit,doc,unit) format4) : 'a = + let f d = () in + Pretty.gprintf f fmt + + +let theLexbuf = ref (Lexing.from_string "") + +let fail format = Pretty.gprintf (fun x -> Pretty.fprint stderr 80 x; + raise (Failure "")) format + + + +(***** Handling parsing errors ********) +type parseinfo = + { mutable linenum: int ; (* Current line *) + mutable linestart: int ; (* The position in the buffer where the + * current line starts *) + mutable fileName : string ; (* Current file *) + mutable hfile : string ; (* High-level file *) + mutable hline : int; (* High-level line *) + lexbuf : Lexing.lexbuf; + inchan : in_channel option; (* None, if from a string *) + mutable num_errors : int; (* Errors so far *) + } + +let dummyinfo = + { linenum = 1; + linestart = 0; + fileName = "" ; + lexbuf = Lexing.from_string ""; + inchan = None; + hfile = ""; + hline = 0; + num_errors = 0; + } + +let current = ref dummyinfo + +let setHLine (l: int) : unit = + !current.hline <- l +let setHFile (f: string) : unit = + !current.hfile <- f + +let rem_quotes str = String.sub str 1 ((String.length str) - 2) + +(* Change \ into / in file names. To avoid complications with escapes *) +let cleanFileName str = + let str1 = + if str <> "" && String.get str 0 = '"' (* '"' ( *) + then rem_quotes str else str in + let l = String.length str1 in + let rec loop (copyto: int) (i: int) = + if i >= l then + String.sub str1 0 copyto + else + let c = String.get str1 i in + if c <> '\\' then begin + String.set str1 copyto c; loop (copyto + 1) (i + 1) + end else begin + String.set str1 copyto '/'; + if i < l - 2 && String.get str1 (i + 1) = '\\' then + loop (copyto + 1) (i + 2) + else + loop (copyto + 1) (i + 1) + end + in + loop 0 0 + +let readingFromStdin = ref false + +let startParsing ?(useBasename=true) (fname: string) = + (* We only support one open file at a time *) + if !current != dummyinfo then begin + s (error "Errormsg.startParsing supports only one open file: You want to open %s and %s is still open\n" fname !current.fileName); + end; + let inchan = + try if fname = "-" then begin + readingFromStdin := true; + stdin + end else begin + readingFromStdin := false; + open_in fname + end + with e -> s (error "Cannot find input file %s (exception %s" + fname (Printexc.to_string e)) in + let lexbuf = Lexing.from_channel inchan in + let i = + { linenum = 1; linestart = 0; + fileName = + cleanFileName (if useBasename then Filename.basename fname else fname); + lexbuf = lexbuf; inchan = Some inchan; + hfile = ""; hline = 0; + num_errors = 0 } in + + current := i; + lexbuf + +let startParsingFromString ?(file="") ?(line=1) (str: string) = + let lexbuf = Lexing.from_string str in + let i = + { linenum = line; linestart = line - 1; + fileName = file; + hfile = ""; hline = 0; + lexbuf = lexbuf; + inchan = None; + num_errors = 0 } + in + current := i; + lexbuf + +let finishParsing () = + let i = !current in + (match i.inchan with Some c -> close_in c | _ -> ()); + current := dummyinfo + + +(* Call this function to announce a new line *) +let newline () = + let i = !current in + i.linenum <- 1 + i.linenum; + i.linestart <- Lexing.lexeme_start i.lexbuf + +let newHline () = + let i = !current in + i.hline <- 1 + i.hline + +let setCurrentLine (i: int) = + !current.linenum <- i + +let setCurrentFile (n: string) = + !current.fileName <- cleanFileName n + + +let max_errors = 20 (* Stop after 20 errors *) + +let parse_error (msg: string) : 'a = + (* Sometimes the Ocaml parser raises errors in symbol_start and symbol_end *) + let token_start, token_end = + try Parsing.symbol_start (), Parsing.symbol_end () + with e -> begin + ignore (warn "Parsing raised %s\n" (Printexc.to_string e)); + 0, 0 + end + in + let i = !current in + let adjStart = + if token_start < i.linestart then 0 else token_start - i.linestart in + let adjEnd = + if token_end < i.linestart then 0 else token_end - i.linestart in + output_string + stderr + (i.fileName ^ "[" ^ (string_of_int i.linenum) ^ ":" + ^ (string_of_int adjStart) ^ "-" + ^ (string_of_int adjEnd) + ^ "]" + ^ " : " ^ msg); + output_string stderr "\n"; + flush stderr ; + i.num_errors <- i.num_errors + 1; + if i.num_errors > max_errors then begin + output_string stderr "Too many errors. Aborting.\n" ; + exit 1 + end; + hadErrors := true; + raise Parsing.Parse_error + + + + +(* More parsing support functions: line, file, char count *) +let getPosition () : int * string * int = + let i = !current in + i.linenum, i.fileName, Lexing.lexeme_start i.lexbuf + + +let getHPosition () = + !current.hline, !current.hfile + +(** Type for source-file locations *) +type location = + { file: string; (** The file name *) + line: int; (** The line number *) + hfile: string; (** The high-level file name, or "" if not present *) + hline: int; (** The high-level line number, or 0 if not present *) + } + +let d_loc () l = + text (l.file ^ ":" ^ string_of_int l.line) + +let d_hloc () (l: location) = + dprintf "%s:%d%a" l.file l.line + insert (if l.hline > 0 then dprintf " (%s:%d)" l.hfile l.hline else nil) + +let locUnknown = { file = ""; hfile = ""; line = -1; hline = -1 } + +let getLocation () = + let hl, hf = getHPosition () in + let l, f, c = getPosition () in + { hfile = hf; hline = hl; + file = f; line = l } + diff --git a/cil/ocamlutil/errormsg.mli b/cil/ocamlutil/errormsg.mli new file mode 100644 index 00000000..8d9c6979 --- /dev/null +++ b/cil/ocamlutil/errormsg.mli @@ -0,0 +1,164 @@ +(* + * + * Copyright (c) 2001-2002, + * George C. Necula + * Scott McPeak + * Wes Weimer + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * + * 3. The names of the contributors may not be used to endorse or promote + * products derived from this software without specific prior written + * permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS + * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED + * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A + * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER + * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + *) +(** Utility functions for error-reporting *) + +(** A channel for printing log messages *) +val logChannel : out_channel ref + +(** If set then print debugging info *) +val debugFlag : bool ref + +val verboseFlag : bool ref + + +(** Set to true if you want to see all warnings. *) +val warnFlag: bool ref + +(** Error reporting functions raise this exception *) +exception Error + + + (* Error reporting. All of these functions take same arguments as a + * Pretty.eprintf. They set the hadErrors flag, but do not raise an + * exception. Their return type is unit. + *) + +(** Prints an error message of the form [Error: ...]. + Use in conjunction with s, for example: [E.s (E.error ... )]. *) +val error: ('a,unit,Pretty.doc,unit) format4 -> 'a + +(** Similar to [error] except that its output has the form [Bug: ...] *) +val bug: ('a,unit,Pretty.doc,unit) format4 -> 'a + +(** Similar to [error] except that its output has the form [Unimplemented: ...] *) +val unimp: ('a,unit,Pretty.doc,unit) format4 -> 'a + +(** Stop the execution by raising an Error. *) +val s: 'a -> 'b + +(** This is set whenever one of the above error functions are called. It must + be cleared manually *) +val hadErrors: bool ref + +(** Like {!Errormsg.error} but does not raise the {!Errormsg.Error} + * exception. Return type is unit. *) +val warn: ('a,unit,Pretty.doc,unit) format4 -> 'a + +(** Like {!Errormsg.warn} but optional. Printed only if the + * {!Errormsg.warnFlag} is set *) +val warnOpt: ('a,unit,Pretty.doc,unit) format4 -> 'a + +(** Print something to [logChannel] *) +val log: ('a,unit,Pretty.doc,unit) format4 -> 'a + +(** same as {!Errormsg.log} but do not wrap lines *) +val logg: ('a,unit,Pretty.doc,unit) format4 -> 'a + + (* All of the error and warning reporting functions can also print a + * context. To register a context printing function use "pushContext". To + * remove the last registered one use "popContext". If one of the error + * reporting functions is called it will invoke all currently registered + * context reporting functions in the reverse order they were registered. *) + +(** Do not actually print (i.e. print to /dev/null) *) +val null : ('a,unit,Pretty.doc,unit) format4 -> 'a + +(** Registers a context printing function *) +val pushContext : (unit -> Pretty.doc) -> unit + +(** Removes the last registered context printing function *) +val popContext : unit -> unit + +(** Show the context stack to stderr *) +val showContext : unit -> unit + +(** To ensure that the context is registered and removed properly, use the + function below *) +val withContext : (unit -> Pretty.doc) -> ('a -> 'b) -> 'a -> 'b + + + +val newline: unit -> unit (* Call this function to announce a new line *) +val newHline: unit -> unit + +val getPosition: unit -> int * string * int (* Line number, file name, + current byte count in file *) +val getHPosition: unit -> int * string (** high-level position *) + +val setHLine: int -> unit +val setHFile: string -> unit + +val setCurrentLine: int -> unit +val setCurrentFile: string -> unit + +(** Type for source-file locations *) +type location = + { file: string; (** The file name *) + line: int; (** The line number *) + hfile: string; (** The high-level file name, or "" if not present *) + hline: int; (** The high-level line number, or 0 if not present *) + } + +val d_loc: unit -> location -> Pretty.doc +val d_hloc: unit -> location -> Pretty.doc + +val getLocation: unit -> location + +val parse_error: string -> (* A message *) + 'a + +(** An unknown location for use when you need one but you don't have one *) +val locUnknown: location + + +(** Records whether the stdin is open for reading the goal **) +val readingFromStdin: bool ref + + +(* Call this function to start parsing. useBasename is by default "true", + * meaning that the error information maintains only the basename. If the + * file name is - then it reads from stdin. *) +val startParsing: ?useBasename:bool -> string -> + Lexing.lexbuf + +val startParsingFromString: ?file:string -> ?line:int -> string + -> Lexing.lexbuf + +val finishParsing: unit -> unit (* Call this function to finish parsing and + * close the input channel *) + + diff --git a/cil/ocamlutil/growArray.ml b/cil/ocamlutil/growArray.ml new file mode 100644 index 00000000..ccadc762 --- /dev/null +++ b/cil/ocamlutil/growArray.ml @@ -0,0 +1,191 @@ +(** Growable Arrays *) + +type 'a fill = + Elem of 'a + | Susp of (int -> 'a) + +type 'a t = { + gaFill: 'a fill; + (** Stuff to use to fill in the array as it grows *) + + mutable gaMaxInitIndex: int; + (** Maximum index that was written to. -1 if no writes have + * been made. *) + + mutable gaData: 'a array; + } + +let growTheArray (ga: 'a t) (len: int) + (toidx: int) (why: string) : unit = + if toidx >= len then begin + (* Grow the array by 50% *) + let newlen = toidx + 1 + len / 2 in +(* + ignore (E.log "growing an array to idx=%d (%s)\n" toidx why); +*) + let data' = begin match ga.gaFill with + Elem x -> + let data'' = Array.create newlen x in + Array.blit ga.gaData 0 data'' 0 len; + data'' + | Susp f -> Array.init newlen + (fun i -> if i < len then ga.gaData.(i) else f i) + end + in + ga.gaData <- data' + end + +let max_init_index (ga: 'a t) : int = + ga.gaMaxInitIndex + +let num_alloc_index (ga: 'a t) : int = + Array.length ga.gaData + +let reset_max_init_index (ga: 'a t) : unit = + ga.gaMaxInitIndex <- -1 + +let getg (ga: 'a t) (r: int) : 'a = + let len = Array.length ga.gaData in + if r >= len then + growTheArray ga len r "getg"; + + ga.gaData.(r) + +let setg (ga: 'a t) (r: int) (what: 'a) : unit = + let len = Array.length ga.gaData in + if r >= len then + growTheArray ga len r "setg"; + if r > max_init_index ga then ga.gaMaxInitIndex <- r; + ga.gaData.(r) <- what + +let get (ga: 'a t) (r: int) : 'a = Array.get ga.gaData r + +let set (ga: 'a t) (r: int) (what: 'a) : unit = + if r > max_init_index ga then ga.gaMaxInitIndex <- r; + Array.set ga.gaData r what + +let make (initsz: int) (fill: 'a fill) : 'a t = + { gaFill = fill; + gaMaxInitIndex = -1; + gaData = begin match fill with + Elem x -> Array.create initsz x + | Susp f -> Array.init initsz f + end; } + +let clear (ga: 'a t) : unit = + (* This assumes the user hasn't used the raw "set" on any value past + max_init_index. Maybe we shouldn't trust max_init_index here?? *) + if ga.gaMaxInitIndex >= 0 then begin + begin match ga.gaFill with + Elem x -> Array.fill ga.gaData 0 (ga.gaMaxInitIndex+1) x + | Susp f -> + for i = 0 to ga.gaMaxInitIndex do + Array.set ga.gaData i (f i) + done + end; + ga.gaMaxInitIndex <- -1 + end + +let copy (ga: 'a t) : 'a t = + { ga with gaData = Array.copy ga.gaData } + +let deep_copy (ga: 'a t) (copy: 'a -> 'a): 'a t = + { ga with gaData = Array.map copy ga.gaData } + +(* An accumulating for loop. Used internally. *) +let fold_for ~(init: 'a) ~(lo: int) ~(hi: int) (f: int -> 'a -> 'a) = + let rec forloop i acc = + if i > hi then acc + else forloop (i+1) (f i acc) + in + forloop lo init + +(** Iterate over the initialized elements of the array *) +let iter (f: 'a -> unit) (ga: 'a t) = + for i = 0 to max_init_index ga do + f ga.gaData.(i) + done + +(** Iterate over the initialized elements of the array *) +let iteri (f: int -> 'a -> unit) (ga: 'a t) = + for i = 0 to max_init_index ga do + f i ga.gaData.(i) + done + +(** Iterate over the elements of 2 arrays *) +let iter2 (f: int -> 'a -> 'b -> unit) (ga1: 'a t) (ga2: 'b t) = + let len1 = max_init_index ga1 in + let len2 = max_init_index ga2 in + if len1 > -1 || len2 > -1 then begin + let max = if len1 > len2 then begin + ignore(getg ga2 len1); (*grow ga2 to match ga1*) + len1 + end else begin + ignore(getg ga1 len2); (*grow ga1 to match ga2*) + len2 + end in + for i = 0 to max do + f i ga1.gaData.(i) ga2.gaData.(i) + done + end + +(** Fold left over the initialized elements of the array *) +let fold_left (f: 'acc -> 'a -> 'acc) (acc: 'acc) (ga: 'a t) : 'acc = + let rec loop (acc: 'acc) (idx: int) : 'acc = + if idx > max_init_index ga then + acc + else + loop (f acc ga.gaData.(idx)) (idx + 1) + in + loop acc 0 + + +(** Fold left over the initialized elements of the array *) +let fold_lefti (f: 'acc -> int -> 'a -> 'acc) (acc: 'acc) (ga: 'a t) : 'acc = + let rec loop (acc: 'acc) (idx: int) : 'acc = + if idx > max_init_index ga then + acc + else + loop (f acc idx ga.gaData.(idx)) (idx + 1) + in + loop acc 0 + +(** Fold right over the initialized elements of the array *) +let fold_right (f: 'a -> 'acc -> 'acc) (ga: 'a t) (acc: 'acc) : 'acc = + let rec loop (acc: 'acc) (idx: int) : 'acc = + if idx < 0 then + acc + else + loop (f ga.gaData.(idx) acc) (idx - 1) + in + loop acc (max_init_index ga) + +(** Document generator *) +let d_growarray (sep: Pretty.doc) + (doit:int -> 'a -> Pretty.doc) + () + (elements: 'a t) = + Pretty.docArray ~sep:sep doit () elements.gaData + +let restoreGA ?deepCopy (ga: 'a t) : (unit -> unit) = + let old = + (match deepCopy with + None -> copy ga + | Some f -> deep_copy ga f) + in + (fun () -> + if ga.gaFill != old.gaFill then + Errormsg.s + (Errormsg.bug "restoreGA to an array with a different fill."); + ga.gaMaxInitIndex <- old.gaMaxInitIndex; + for i = 0 to max_init_index ga do + set ga i (getg old i) + done) + +let find (ga: 'a t) (fn: 'a -> bool) : int option = + let rec loop (i:int) : int option = + if i > ga.gaMaxInitIndex then None + else if fn (get ga i) then Some i + else loop (i + 1) + in + loop 0 diff --git a/cil/ocamlutil/growArray.mli b/cil/ocamlutil/growArray.mli new file mode 100644 index 00000000..4cb5f48f --- /dev/null +++ b/cil/ocamlutil/growArray.mli @@ -0,0 +1,131 @@ +(***********************************************************************) +(* Growable Arrays *) +(* *) +(* This a wrapper around the standard OCaml array, but will grow *) +(* automatically on get or set outside the current size of the *) +(* array. *) +(* *) +(* The interface is the same as the standard OCaml array where *) +(* applicable (and implemented). *) +(***********************************************************************) + +(* $Id: growArray.mli,v 1.8 2005-01-06 15:37:36 necula Exp $ *) + +(** Array operations. *) + +(** The type of growable arrays *) +type 'a t + +(** The default value to a new element of the growable array *) +type 'a fill = + Elem of 'a + (* A default value *) + | Susp of (int -> 'a) + (* A function given an index to generate a default value *) + +val make : int -> 'a fill -> 'a t +(** [GrowArray.make n x] returns a fresh growable array of size + at least [n] with default value specified by [x]. + + Raise [Invalid_argument] if [n < 0] or [n > Sys.max_array_length]. *) + +val num_alloc_index: 'a t -> int +(** [GrowArray.num_alloc_index a] returns the number of allocated entries in + * the array **) + +val max_init_index : 'a t -> int +(** [GrowArray.max_init_index a] returns the maximum index to + which has been written. + + Returns -1 if no writes have been made. *) + +val reset_max_init_index : 'a t -> unit +(** [GrowArray.reset_init a] resets the max_init_index. You should probably + use [GrowArray.clear a] instead if you also want to delete the contents. *) + +val getg : 'a t -> int -> 'a +(** [GrowArray.getg a n] returns the element number [n] of array [a]. + The first element has number 0. + The last element has number [GrowArray.length a - 1]. + + If [n] is outside the range 0 to [(GrowArray.max_init_index a)], + then the array grows to at least [n] and yields the default value. *) + +val setg : 'a t -> int -> 'a -> unit +(** [GrowArray.setg a n x] modifies array [a] in place, replacing + element number [n] with [x]. + + If [n] is outside the range 0 to [(GrowArray.max_init_index a)], + then the array grows to at least [n] and yields the default value. *) + +val get : 'a t -> int -> 'a +(** [GrowArray.get a n] returns the element number [n] of grow array [a]. + + Raise [Invalid_argument "Array.get"] if [n] is outside the range + of the underlying array. *) + +val set : 'a t -> int -> 'a -> unit +(** [GrowArray.set a n x] modifies grow array [a] in place, replacing + element number [n] with [x]. + + Raise [Invalid_argument "Array.set"] if [n] is outside the range + of the underlying array. *) + +val clear: 'a t -> unit +(** [GrowArray.clear a] clears the contents of the array and sets + max_init_index to -1. Suspension thunks will be rerun to regenerate the + initial values of the array. *) + +val copy : 'a t -> 'a t +(** [GrowArray.copy a] returns a copy of [a], that is, a fresh array + containing the same elements as [a]. *) + +val deep_copy : 'a t -> ('a -> 'a) -> 'a t +(** [GrowArray.copy a f] returns a deep copy of [a] using f to + copy elements of [a]. *) + +val iter : ('a -> unit) -> 'a t -> unit +(** [GrowArray.iter f a] applies function [f] in turn to all + the elements of [a]. It is equivalent to + [f a.(0); f a.(1); ...; f a.(GrowArray.length a - 1); ()]. *) + +val iteri : (int -> 'a -> unit) -> 'a t -> unit +(** Same as {!GrowArray.iter}, but the + function is applied to the index of the element as first argument, + and the element itself as second argument. *) + +val iter2 : (int -> 'a -> 'b -> unit) -> 'a t -> 'b t -> unit +(** Same as {!GrowArray.iteri}, but the function is applied to two arrays. + [iter2 f a b] is equivalent to + [f 0 a.(0) b.(0); f 1 a.(1) b.(1); ...; f n a.(n) b.(n); ()] + where n is the larger of (max_init_index a) or (max_init_index b). + The shorter array will grow to match the longer.*) + +val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a +(** [GrowArray.fold_left f x a] computes + [f (... (f (f x a.(0)) a.(1)) ...) a.(n-1)], + where [n] is the length of the array [a]. *) + +val fold_lefti : ('a -> int -> 'b -> 'a) -> 'a -> 'b t -> 'a +(** [GrowArray.fold_lefti f x a] computes + [f (... (f (f x 0 a.(0)) 1 a.(1)) ...) (n-1) a.(n-1)], + where [n] is the length of the array [a]. *) + +val fold_right : ('b -> 'a -> 'a) -> 'b t -> 'a -> 'a +(** [GrowArray.fold_right f a x] computes + [f a.(0) (f a.(1) ( ... (f a.(n-1) x) ...))], + where [n] is the length of the array [a]. *) + +val d_growarray : Pretty.doc -> (int -> 'a -> Pretty.doc) -> unit -> 'a t + -> Pretty.doc +(** [GrowArray.d_growarray sep f () a] creates a {!Pretty.doc} for growable + array a using separator sep and element printer f. *) + + +val restoreGA: ?deepCopy:('a -> 'a) -> 'a t -> unit -> unit +(** Given a growable array, produce a thunk that later restores it to its + current value *) + +val find: 'a t -> ('a -> bool) -> int option +(** Returns the index of the first element in the array that satisfies the + predicate, or None if there is no such element *) diff --git a/cil/ocamlutil/inthash.ml b/cil/ocamlutil/inthash.ml new file mode 100755 index 00000000..b1ad0c07 --- /dev/null +++ b/cil/ocamlutil/inthash.ml @@ -0,0 +1,188 @@ +(** A hash table specialized on integer keys *) +type 'a t = + { mutable size: int; (* number of elements *) + mutable data: 'a bucketlist array } (* the buckets *) + +and 'a bucketlist = + Empty + | Cons of int * 'a * 'a bucketlist + +let hash key = key land 0x3fffffff + +let create initial_size = + let s = min (max 1 initial_size) Sys.max_array_length in + { size = 0; data = Array.make s Empty } + +let clear h = + for i = 0 to Array.length h.data - 1 do + h.data.(i) <- Empty + done; + h.size <- 0 + +let copy h = + { size = h.size; + data = Array.copy h.data } + +let copy_into src dest = + dest.size <- src.size; + dest.data <- Array.copy src.data + +let length h = h.size + +let resize tbl = + let odata = tbl.data in + let osize = Array.length odata in + let nsize = min (2 * osize + 1) Sys.max_array_length in + if nsize <> osize then begin + let ndata = Array.create nsize Empty in + let rec insert_bucket = function + Empty -> () + | Cons(key, data, rest) -> + insert_bucket rest; (* preserve original order of elements *) + let nidx = (hash key) mod nsize in + ndata.(nidx) <- Cons(key, data, ndata.(nidx)) in + for i = 0 to osize - 1 do + insert_bucket odata.(i) + done; + tbl.data <- ndata; + end + +let add h key info = + let i = (hash key) mod (Array.length h.data) in + let bucket = Cons(key, info, h.data.(i)) in + h.data.(i) <- bucket; + h.size <- succ h.size; + if h.size > Array.length h.data lsl 1 then resize h + +let remove h key = + let rec remove_bucket = function + Empty -> + Empty + | Cons(k, i, next) -> + if k = key + then begin h.size <- pred h.size; next end + else Cons(k, i, remove_bucket next) in + let i = (hash key) mod (Array.length h.data) in + h.data.(i) <- remove_bucket h.data.(i) + +let remove_all h key = + let rec remove_bucket = function + Empty -> + Empty + | Cons(k, i, next) -> + if k = key + then begin h.size <- pred h.size; + remove_bucket next end + else Cons(k, i, remove_bucket next) in + let i = (hash key) mod (Array.length h.data) in + h.data.(i) <- remove_bucket h.data.(i) + +let rec find_rec key = function + Empty -> + raise Not_found + | Cons(k, d, rest) -> + if key = k then d else find_rec key rest + +let find h key = + match h.data.((hash key) mod (Array.length h.data)) with + Empty -> raise Not_found + | Cons(k1, d1, rest1) -> + if key = k1 then d1 else + match rest1 with + Empty -> raise Not_found + | Cons(k2, d2, rest2) -> + if key = k2 then d2 else + match rest2 with + Empty -> raise Not_found + | Cons(k3, d3, rest3) -> + if key = k3 then d3 else find_rec key rest3 + +let find_all h key = + let rec find_in_bucket = function + Empty -> + [] + | Cons(k, d, rest) -> + if k = key then d :: find_in_bucket rest else find_in_bucket rest in + find_in_bucket h.data.((hash key) mod (Array.length h.data)) + +let replace h key info = + let rec replace_bucket = function + Empty -> + raise Not_found + | Cons(k, i, next) -> + if k = key + then Cons(k, info, next) + else Cons(k, i, replace_bucket next) in + let i = (hash key) mod (Array.length h.data) in + let l = h.data.(i) in + try + h.data.(i) <- replace_bucket l + with Not_found -> + h.data.(i) <- Cons(key, info, l); + h.size <- succ h.size; + if h.size > Array.length h.data lsl 1 then resize h + +let mem h key = + let rec mem_in_bucket = function + | Empty -> + false + | Cons(k, d, rest) -> + k = key || mem_in_bucket rest in + mem_in_bucket h.data.((hash key) mod (Array.length h.data)) + +let iter (f: int -> 'a -> unit) (h: 'a t) : unit = + let rec do_bucket = function + Empty -> + () + | Cons(k, d, rest) -> + f k d; do_bucket rest in + let d = h.data in + for i = 0 to Array.length d - 1 do + do_bucket d.(i) + done + +let fold (f: int -> 'a -> 'b -> 'b) (h: 'a t) (init: 'b) = + let rec do_bucket b accu = + match b with + Empty -> + accu + | Cons(k, d, rest) -> + do_bucket rest (f k d accu) in + let d = h.data in + let accu = ref init in + for i = 0 to Array.length d - 1 do + accu := do_bucket d.(i) !accu + done; + !accu + + +let memoize (h: 'a t) (key: int) (f: int -> 'a) : 'a = + let i = (hash key) mod (Array.length h.data) in + let rec find_rec key = function + Empty -> addit () + | Cons(k, d, rest) -> + if key = k then d else find_rec key rest + and find_in_bucket key = function + Empty -> addit () + | Cons(k1, d1, rest1) -> + if key = k1 then d1 else + match rest1 with + Empty -> addit () + | Cons(k2, d2, rest2) -> + if key = k2 then d2 else + match rest2 with + Empty -> addit () + | Cons(k3, d3, rest3) -> + if key = k3 then d3 else find_rec key rest3 + and addit () = + let it = f key in + h.data.(i) <- Cons(key, it, h.data.(i)); + h.size <- succ h.size; + if h.size > Array.length h.data lsl 1 then resize h; + it + in + find_in_bucket key h.data.(i) + + +let tolist (h: 'a t) : (int * 'a) list = + fold (fun k d acc -> (k, d) :: acc) h [] diff --git a/cil/ocamlutil/inthash.mli b/cil/ocamlutil/inthash.mli new file mode 100755 index 00000000..f62fcd2b --- /dev/null +++ b/cil/ocamlutil/inthash.mli @@ -0,0 +1,27 @@ +type 'a t + +(* These functions behave the same as Hashtbl, but the key type is + always int. (Specializing on int improves the performance) *) + +val create: int -> 'a t +val clear: 'a t -> unit +val length : 'a t -> int + +val copy: 'a t -> 'a t +val copy_into: 'a t -> 'a t -> unit + +val add: 'a t -> int -> 'a -> unit +val replace: 'a t -> int -> 'a -> unit +val remove: 'a t -> int -> unit +val remove_all: 'a t -> int -> unit + +val mem: 'a t -> int -> bool +val find: 'a t -> int -> 'a +val find_all: 'a t -> int -> 'a list + +val iter: (int -> 'a -> unit) -> 'a t -> unit +val fold: (int -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b + +val memoize: 'a t -> int -> (int -> 'a) -> 'a + +val tolist: 'a t -> (int * 'a) list diff --git a/cil/ocamlutil/intmap.ml b/cil/ocamlutil/intmap.ml new file mode 100755 index 00000000..00242bc1 --- /dev/null +++ b/cil/ocamlutil/intmap.ml @@ -0,0 +1,171 @@ +(***********************************************************************) +(* *) +(* Objective Caml *) +(* *) +(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *) +(* *) +(* Copyright 1996 Institut National de Recherche en Informatique et *) +(* en Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU Library General Public License, with *) +(* the special exception on linking described in file ../LICENSE. *) +(* *) +(***********************************************************************) + +(* $Id: intmap.ml,v 1.2 2005-10-04 21:30:25 necula Exp $ *) + +(* specialized to integer keys by George Necula *) + +type 'a t = + Empty + | Node of 'a t * int * 'a * 'a t * int + +let height = function + Empty -> 0 + | Node(_,_,_,_,h) -> h + +let create l x d r = + let hl = height l and hr = height r in + Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1)) + +let bal l x d r = + let hl = match l with Empty -> 0 | Node(_,_,_,_,h) -> h in + let hr = match r with Empty -> 0 | Node(_,_,_,_,h) -> h in + if hl > hr + 2 then begin + match l with + Empty -> invalid_arg "Map.bal" + | Node(ll, lv, ld, lr, _) -> + if height ll >= height lr then + create ll lv ld (create lr x d r) + else begin + match lr with + Empty -> invalid_arg "Map.bal" + | Node(lrl, lrv, lrd, lrr, _)-> + create (create ll lv ld lrl) lrv lrd (create lrr x d r) + end + end else if hr > hl + 2 then begin + match r with + Empty -> invalid_arg "Map.bal" + | Node(rl, rv, rd, rr, _) -> + if height rr >= height rl then + create (create l x d rl) rv rd rr + else begin + match rl with + Empty -> invalid_arg "Map.bal" + | Node(rll, rlv, rld, rlr, _) -> + create (create l x d rll) rlv rld (create rlr rv rd rr) + end + end else + Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1)) + +let empty = Empty + +let is_empty = function Empty -> true | _ -> false + +let rec add x data = function + Empty -> + Node(Empty, x, data, Empty, 1) + | Node(l, v, d, r, h) as t -> + if x = v then + Node(l, x, data, r, h) + else if x < v then + bal (add x data l) v d r + else + bal l v d (add x data r) + +let rec find x = function + Empty -> + raise Not_found + | Node(l, v, d, r, _) -> + if x = v then d + else find x (if x < v then l else r) + +let rec mem x = function + Empty -> + false + | Node(l, v, d, r, _) -> + x = v || mem x (if x < v then l else r) + +let rec min_binding = function + Empty -> raise Not_found + | Node(Empty, x, d, r, _) -> (x, d) + | Node(l, x, d, r, _) -> min_binding l + +let rec remove_min_binding = function + Empty -> invalid_arg "Map.remove_min_elt" + | Node(Empty, x, d, r, _) -> r + | Node(l, x, d, r, _) -> bal (remove_min_binding l) x d r + +let merge t1 t2 = + match (t1, t2) with + (Empty, t) -> t + | (t, Empty) -> t + | (_, _) -> + let (x, d) = min_binding t2 in + bal t1 x d (remove_min_binding t2) + +let rec remove x = function + Empty -> + Empty + | Node(l, v, d, r, h) as t -> + if x = v then + merge l r + else if x < v then + bal (remove x l) v d r + else + bal l v d (remove x r) + +let rec iter f = function + Empty -> () + | Node(l, v, d, r, _) -> + iter f l; f v d; iter f r + +let rec map f = function + Empty -> Empty + | Node(l, v, d, r, h) -> Node(map f l, v, f d, map f r, h) + +let rec mapi f = function + Empty -> Empty + | Node(l, v, d, r, h) -> Node(mapi f l, v, f v d, mapi f r, h) + +let rec fold f m accu = + match m with + Empty -> accu + | Node(l, v, d, r, _) -> + fold f l (f v d (fold f r accu)) + +type 'a enumeration = End | More of int * 'a * 'a t * 'a enumeration + +let rec cons_enum m e = + match m with + Empty -> e + | Node(l, v, d, r, _) -> cons_enum l (More(v, d, r, e)) + +let compare cmp m1 m2 = + let rec compare_aux e1 e2 = + match (e1, e2) with + (End, End) -> 0 + | (End, _) -> -1 + | (_, End) -> 1 + | (More(v1, d1, r1, e1), More(v2, d2, r2, e2)) -> + if v1 <> v2 then if v1 < v2 then -1 else 1 else + let c = cmp d1 d2 in + if c <> 0 then c else + compare_aux (cons_enum r1 e1) (cons_enum r2 e2) +in compare_aux (cons_enum m1 End) (cons_enum m2 End) + +let equal cmp m1 m2 = + let rec equal_aux e1 e2 = + match (e1, e2) with + (End, End) -> true + | (End, _) -> false + | (_, End) -> false + | (More(v1, d1, r1, e1), More(v2, d2, r2, e2)) -> + v1 = v2 && cmp d1 d2 && + equal_aux (cons_enum r1 e1) (cons_enum r2 e2) +in equal_aux (cons_enum m1 End) (cons_enum m2 End) + +(** Some definitions for ML2Coq *) +let _ = ignore "coq: +(* Some definitions for ML2Coq *) + +" diff --git a/cil/ocamlutil/intmap.mli b/cil/ocamlutil/intmap.mli new file mode 100755 index 00000000..eef89b55 --- /dev/null +++ b/cil/ocamlutil/intmap.mli @@ -0,0 +1,87 @@ +(***********************************************************************) +(* *) +(* Objective Caml *) +(* *) +(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *) +(* *) +(* Copyright 1996 Institut National de Recherche en Informatique et *) +(* en Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU Library General Public License, with *) +(* the special exception on linking described in file ../LICENSE. *) +(* *) +(***********************************************************************) + +(* $Id: intmap.mli,v 1.1 2005-02-28 16:24:00 necula Exp $ *) + +(** Specialized to integer keys by George Necula *) + +(** Association tables over ordered types. + + This module implements applicative association tables, also known as + finite maps or dictionaries, given a total ordering function + over the keys. + All operations over maps are purely applicative (no side-effects). + The implementation uses balanced binary trees, and therefore searching + and insertion take time logarithmic in the size of the map. +*) + +type (+'a) t + (** The type of maps from type [key] to type ['a]. *) + +val empty: 'a t + (** The empty map. *) + +val is_empty: 'a t -> bool + (** Test whether a map is empty or not. *) + +val add: int -> 'a -> 'a t -> 'a t + (** [add x y m] returns a map containing the same bindings as + [m], plus a binding of [x] to [y]. If [x] was already bound + in [m], its previous binding disappears. *) + +val find: int -> 'a t -> 'a + (** [find x m] returns the current binding of [x] in [m], + or raises [Not_found] if no such binding exists. *) + +val remove: int -> 'a t -> 'a t + (** [remove x m] returns a map containing the same bindings as + [m], except for [x] which is unbound in the returned map. *) + +val mem: int -> 'a t -> bool + (** [mem x m] returns [true] if [m] contains a binding for [x], + and [false] otherwise. *) + +val iter: (int -> 'a -> unit) -> 'a t -> unit + (** [iter f m] applies [f] to all bindings in map [m]. + [f] receives the key as first argument, and the associated value + as second argument. The bindings are passed to [f] in increasing + order with respect to the ordering over the type of the keys. + Only current bindings are presented to [f]: + bindings hidden by more recent bindings are not passed to [f]. *) + +val map: ('a -> 'b) -> 'a t -> 'b t + (** [map f m] returns a map with same domain as [m], where the + associated value [a] of all bindings of [m] has been + replaced by the result of the application of [f] to [a]. + The bindings are passed to [f] in increasing order + with respect to the ordering over the type of the keys. *) + +val mapi: (int -> 'a -> 'b) -> 'a t -> 'b t + (** Same as {!Map.S.map}, but the function receives as arguments both the + key and the associated value for each binding of the map. *) + +val fold: (int -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b + (** [fold f m a] computes [(f kN dN ... (f k1 d1 a)...)], + where [k1 ... kN] are the keys of all bindings in [m] + (in increasing order), and [d1 ... dN] are the associated data. *) + +val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int + (** Total ordering between maps. The first argument is a total ordering + used to compare data associated with equal keys in the two maps. *) + +val equal: ('a -> 'a -> bool) -> 'a t -> 'a t -> bool + (** [equal cmp m1 m2] tests whether the maps [m1] and [m2] are + equal, that is, contain equal keys and associate them with + equal data. [cmp] is the equality predicate used to compare + the data associated with the keys. *) + diff --git a/cil/ocamlutil/perfcount.c.in b/cil/ocamlutil/perfcount.c.in new file mode 100755 index 00000000..ae532f69 --- /dev/null +++ b/cil/ocamlutil/perfcount.c.in @@ -0,0 +1,184 @@ +// -*- Mode: c -*- +// +/* + * A module that allows the reading of performance counters on Pentium. + * + * This file contains both code that uses the performance counters to + * compute the number of cycles per second (to be used during ./configure) + * and also code to read the performance counters from Ocaml. + * + * Author: George Necula (necula@cs.berkeley.edu) + */ +#include +#include +#include + +#if defined(__GNUC__) + #define longlong long long + // RDTSC puts the result in EAX and EDX. We tell gcc to use those registers + // for "low" and "high" + #if defined(__i386__) + #define GETCOUNTER(low,high) \ + __asm__ volatile ("rdtsc" : "=a" (low), "=d" (high)); + #else + #define GETCOUNTER(low,high) \ + printf ("Reading of performance counters is supported only on Intel x86\n"); \ + exit(1); + #endif +#else + // Microsoft Visual Studio + #define longlong __int64 + #define inline __inline + #define GETCOUNTER(low,high) __asm { \ + __asm rdtsc \ + __asm mov low, eax \ + __asm mov high, edx }; +#endif + +/* Store here the first value read from the performance counter */ +unsigned static longlong first_value; + + +/* This is the function that actually reads the performance counter. */ +inline unsigned longlong read_ppc(void) { + unsigned long pclow, pchigh; + unsigned longlong lowhigh; + + GETCOUNTER(pclow, pchigh); + + // printf ("Read low=0x%08lx high=0x%08lx\n", low, high); + + // Put the 64-bit value together + lowhigh = ((unsigned longlong)pclow) | ((unsigned longlong)pchigh << 32); + + if(first_value == 0) { + first_value = lowhigh; + } + return lowhigh - first_value; +} + + +/* sm: I want a version that is as fast as possible, dropping + * bits that aren't very important to achieve it. * + * + * This version drops the low 20 bits and the high 14 bits so the + * result is 30 bits (always a positive Ocaml int); this yields + * megacycles, which for GHz machines will be something like + * milliseconds. */ +static unsigned long sample_ppc_20(void) +{ + unsigned long pclow, pchigh; + + GETCOUNTER(pclow, pchigh); + + return ((pclow >> 20) | (pchigh << 12)) & 0x3FFFFFFF; +} + +/* This version drops the low 10 bits, yielding something like + * microseconds. */ +inline static unsigned long sample_ppc_10() +{ + unsigned long pclow, pchigh; + + GETCOUNTER(pclow,pchigh); + + return ((pclow >> 10) | (pchigh << 22)) & 0x3FFFFFFF; +} + + + +#ifndef CONFIGURATION_ONLY +/*** This is the OCAML stub for the read_ppc ***/ +#include +#include +#include + +#define CYCLES_PER_USEC @CYCLES_PER_USEC@ +value read_pentium_perfcount() +{ + double counter = (double)read_ppc() / (1000000.0 * CYCLES_PER_USEC); + return copy_double(counter); +} + +/* The Ocaml system can use this function to figure out if there are + * performance counters available */ +value has_performance_counters() { + // HAS_PERFCOUNT is set by the configuration code at the end of + // this file, during ./configure +#if @HAS_PERFCOUNT@ != 0 + return Val_true; +#else + return Val_false; +#endif +} + +/* sm: interface to above from Ocaml */ +value sample_pentium_perfcount_20() +{ + return Val_long(sample_ppc_20()); +} + +value sample_pentium_perfcount_10() +{ + return Val_long(sample_ppc_10()); +} + +#endif + + +/* Now we have a function that tries to compute the number of cycles per + * second (to be used during ./configure) */ +#ifdef CONFIGURATION_ONLY +#include +#include +#include + +int main() { + struct tms t; + clock_t start, finish, diff; + unsigned longlong start_pc, finish_pc, diff_pc; + long clk_per_sec = sysconf(_SC_CLK_TCK); + double cycles_per_usec; + + if(clk_per_sec <= 0) { + printf("Cannot find clk_per_sec (got %ld)\n", clk_per_sec); + exit(1); + } + + times(&t); start = t.tms_utime; + start_pc = read_ppc(); + // Do something for a while + { + int i; + double a = 5.678; + for(i=0;i<10000000;i++) { + a = (i & 1) ? (a * a) : (sqrt(a)); + } + } + times(&t); finish = t.tms_utime; + finish_pc = read_ppc(); + diff = finish - start; + diff_pc = finish_pc - start_pc; + if(diff == 0) { + printf("Cannot use Unix.times\n"); + exit(1); + } + if(diff_pc == 0) { + printf("Invalid result from the peformance counters\n"); + exit(1); + } + diff_pc /= 1000000; // We care about cycles per microsecond +// printf("diff = %ld, diff_pc = %ld, clk = %ld\n", +// (long)diff, +// (long)diff_pc, (long)clk_per_sec); + + cycles_per_usec = (((double)diff_pc / (double)diff) + * (double)clk_per_sec); + + /* Whatever value we print here will be used as the CYCLES_PER_USEC + * below */ + printf("%.3lf\n", cycles_per_usec); + exit(0); +} +#endif //defined CONFIGURATION_ONLY + diff --git a/cil/ocamlutil/pretty.ml b/cil/ocamlutil/pretty.ml new file mode 100644 index 00000000..47d07ac4 --- /dev/null +++ b/cil/ocamlutil/pretty.ml @@ -0,0 +1,859 @@ +(* + * + * Copyright (c) 2001-2002, + * George C. Necula + * Scott McPeak + * Wes Weimer + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * + * 3. The names of the contributors may not be used to endorse or promote + * products derived from this software without specific prior written + * permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS + * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED + * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A + * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER + * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + *) + +(******************************************************************************) +(* Pretty printer + This module contains several fast, but sub-optimal heuristics to pretty-print + structured text. +*) + +let debug = false + +(* Choose an algorithm *) +type algo = George | Aman | Gap +let algo = George +let fastMode = ref false + + +(** Whether to print identation or not (for faster printing and smaller + * output) *) +let printIndent = ref true + +(******************************************************************************) +(* The doc type and constructors *) + +type doc = + Nil + | Text of string + | Concat of doc * doc + | CText of doc * string + | Break + | Line + | LeftFlush + | Align + | Unalign + | Mark + | Unmark + +(* Break a string at \n *) +let rec breakString (acc: doc) (str: string) : doc = + try + (* Printf.printf "breaking string %s\n" str; *) + let r = String.index str '\n' in + (* Printf.printf "r=%d\n" r; *) + let len = String.length str in + if r > 0 then begin + (* Printf.printf "Taking %s\n" (String.sub str 0 r); *) + let acc' = Concat(CText (acc, String.sub str 0 r), Line) in + if r = len - 1 then (* The last one *) + acc' + else begin + (* Printf.printf "Continuing with %s\n" (String.sub str (r + 1) (len - r - 1)); *) + breakString acc' + (String.sub str (r + 1) (len - r - 1)) + end + end else (* The first is a newline *) + breakString (Concat(acc, Line)) + (String.sub str (r + 1) (len - r - 1)) + with Not_found -> + if acc = Nil then Text str else CText (acc, str) + +let nil = Nil +let text s = breakString nil s +let num i = text (string_of_int i) +let real f = text (string_of_float f) +let chr c = text (String.make 1 c) +let align = Align +let unalign = Unalign +let line = Line +let leftflush = LeftFlush +let break = Break +let mark = Mark +let unmark = Unmark + +let d_int32 (i: int32) = text (Int32.to_string i) +let f_int32 () i = d_int32 i + +let d_int64 (i: int64) = text (Int64.to_string i) +let f_int64 () i = d_int64 i + + +(* Note that the ++ operator in Ocaml are left-associative. This means + * that if you have a long list of ++ then the whole thing is very unbalanced + * towards the left side. This is the worst possible case since scanning the + * left side of a Concat is the non-tail recursive case. *) + +let (++) d1 d2 = Concat (d1, d2) +let concat d1 d2 = Concat (d1, d2) + +(* Ben Liblit fix *) +let indent n d = text (String.make n ' ') ++ (align ++ (d ++ unalign)) + +let markup d = mark ++ d ++ unmark + +(* Format a sequence. The first argument is a separator *) +let seq ~(sep:doc) ~(doit:'a -> doc) ~(elements: 'a list) = + let rec loop (acc: doc) = function + [] -> acc + | h :: t -> + let fh = doit h in (* Make sure this is done first *) + loop (acc ++ sep ++ fh) t + in + (match elements with + [] -> nil + | h :: t -> + let fh = doit h in loop fh t) + + +let docArray ?(sep=chr ',') (doit:int -> 'a -> doc) () (elements:'a array) = + let len = Array.length elements in + if len = 0 then + nil + else + let rec loop (acc: doc) i = + if i >= len then acc else + let fi = doit i elements.(i) in (* Make sure this is done first *) + loop (acc ++ sep ++ fi) (i + 1) + in + let f0 = doit 0 elements.(0) in + loop f0 1 + +let docOpt delem () = function + None -> text "None" + | Some e -> text "Some(" ++ (delem e) ++ chr ')' + + + +let docList ?(sep=chr ',') (doit:'a -> doc) () (elements:'a list) = + seq sep doit elements + +let insert () d = d + + +let d_list (sep:string) (doit:unit -> 'a -> doc) () (elts:'a list) : doc = + (* thunk 'doit' to match docList's interface *) + let internalDoit (elt:'a) = + (doit () elt) in + (docList ~sep:(text sep) internalDoit () elts) + +(** Format maps *) +module MakeMapPrinter = + functor (Map: sig + type key + type 'a t + val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b + end) -> +struct + let docMap ?(sep=chr ',') + (doit: Map.key -> 'a -> doc) () (maplets: 'a Map.t) : doc = + Map.fold + (fun k d acc -> + (if acc==nil then acc else acc ++ sep) + ++ (doit k d)) + maplets + nil + + let dmaplet d0 d1 = d0 ++ (text " |-> ") ++ d1 + + let d_map ?(dmaplet=dmaplet) (sep:string) dkey dval = + let doit = fun k d -> dmaplet (dkey () k) (dval () d) in + docMap ~sep:(text sep) doit +end + +(** Format sets *) +module MakeSetPrinter = + functor (Set: sig + type elt + type t + val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a + end) -> +struct + let docSet ?(sep=chr ',') (doit: Set.elt -> doc) () (set: Set.t) : doc = + Set.fold + (fun elt acc -> + (if acc==nil then acc else acc ++ sep) + ++ (doit elt)) + set + nil + + let d_set (sep:string) delt = + docSet ~sep:(text sep) (delt ()) +end + + +(******************************************************************************) +(* Some debugging stuff *) + +let dbgprintf x = Printf.fprintf stderr x + +let rec dbgPrintDoc = function + Nil -> dbgprintf "(Nil)" + | Text s -> dbgprintf "(Text %s)" s + | Concat (d1,d2) -> dbgprintf ""; dbgPrintDoc d1; dbgprintf " ++\n "; + dbgPrintDoc d2; dbgprintf "" + | CText (d,s) -> dbgPrintDoc d; dbgprintf " ++ \"%s\"" s; + | Break -> dbgprintf "(Break)" + | Line -> dbgprintf "(Line)" + | LeftFlush -> dbgprintf "(LeftFlush)" + | Align -> dbgprintf "(Align)" + | Unalign -> dbgprintf "(Unalign)" + | Mark -> dbgprintf "(Mark)" + | Unmark -> dbgprintf "(Unmark)" + +(******************************************************************************) +(* The "george" algorithm *) + +(* When we construct documents, most of the time they are heavily unbalanced + * towards the left. This is due to the left-associativity of ++ and also to + * the fact that constructors such as docList construct from the let of a + * sequence. We would prefer to shift the imbalance to the right to avoid + * consuming a lot of stack when we traverse the document *) +let rec flatten (acc: doc) = function + | Concat (d1, d2) -> flatten (flatten acc d2) d1 + | CText (d, s) -> flatten (Concat(Text s, acc)) d + | Nil -> acc (* Get rid of Nil *) + | d -> Concat(d, acc) + +(* We keep a stack of active aligns. *) +type align = + { mutable gainBreak: int; (* This is the gain that is associated with + * taking the break associated with this + * alignment mark. If this is 0, then there + * is no break associated with the mark *) + mutable isTaken: bool ref; (* If breakGain is > 0 then this is a ref + * cell that must be set to true when the + * break is taken. These ref cells are also + * int the "breaks" list *) + deltaFromPrev: int ref; (* The column of this alignment mark - + * the column of the previous mark. + * Shared with the deltaToNext of the + * previous active align *) + deltaToNext: int ref (* The column of the next alignment mark - + * the columns of this one. Shared with + * deltaFromPrev of the next active 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, + * with the top at the head. Never empty. *) + ref [{ gainBreak = 0; isTaken = ref false; + deltaFromPrev = ref 0; deltaToNext = ref 0; }] + +let topAlignAbsCol = ref 0 (* The absolute column of the top alignment *) + +let pushAlign (abscol: int) = + let topalign = List.hd !aligns in + let res = + { 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 + +let popAlign () = + match !aligns with + top :: t when t != [] -> + aligns := t; + topAlignAbsCol := !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 [] + + +(* 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 [] + +(* The maximum column that we should use *) +let maxCol = ref 0 + +(* Sometimes we take all the optional breaks *) +let breakAllMode = ref false + +(* We are taking a newline and moving left *) +let newline () = + let topalign = List.hd !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 *) + + + +(* Choose the align with the best gain. We outght 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 bestGain = ref 0 in + let rec loop (breakingAlign: align option) = function + [] -> breakingAlign + | a :: resta -> + if debug then dbgprintf "Looking at align with gain %d\n" a.gainBreak; + if a.gainBreak > !bestGain then begin + bestGain := a.gainBreak; + loop (Some a) resta + end else + loop breakingAlign resta + in + loop None !aligns + + +(* Another one that chooses the break associated with the current align only *) +let chooseLastGain () : align option = + let topalign = List.hd !aligns in + if topalign.gainBreak > 0 then Some topalign else None + +(* We have just advanced to a new column. See if we must take a line break *) +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 + 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 + None -> begin + (* No breaks are available. Take all breaks from now on *) + breakAllMode := true; + if debug then + dbgprintf "Can't find any breaks\n"; + abscol + end + | Some breakingAlign -> begin + let topalign = List.hd !aligns in + let theGain = breakingAlign.gainBreak in + assert (theGain > 0); + if debug then dbgprintf "Taking break at %d. gain=%d\n" abscol theGain; + breakingAlign.isTaken := true; + breakingAlign.gainBreak <- 0; + if breakingAlign != topalign then begin + breakingAlign.deltaToNext := + !(breakingAlign.deltaToNext) - theGain; + topAlignAbsCol := !topAlignAbsCol - theGain + end; + tryAgain (abscol - theGain) + end + end + in + tryAgain abscol + + +(* Keep track of nested align in gprintf. Each gprintf format string must + * 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 useAlignDepth = true + +(** Start an align. Return true if we ahve just passed the threshhold *) +let enterAlign () = + incr alignDepth; + useAlignDepth && !alignDepth = !printDepth + 1 + +(** Exit an align *) +let exitAlign () = + decr alignDepth + +(** See if we are at a low-enough align level (and we should be printing + * normally) *) +let shallowAlign () = + not useAlignDepth || !alignDepth <= !printDepth + + +(* Pass the current absolute column and compute the new column *) +let rec scan (abscol: int) (d: doc) : int = + match d with + Nil -> abscol + | Concat (d1, d2) -> scan (scan abscol d1) d2 + | Text s when shallowAlign () -> + 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) + | CText (d, s) -> + let abscol' = scan abscol d in + if shallowAlign () 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) + end else + abscol' + + | Align -> + pushAlign abscol; + if enterAlign () then + movingRight (abscol + 3) (* "..." *) + else + abscol + + | Unalign -> exitAlign (); popAlign (); abscol + + | Line when shallowAlign () -> (* A forced line break *) + if !activeMarkups != [] then + failwith "Line breaks inside markup sections"; + newline () + + | LeftFlush when shallowAlign () -> (* Keep cursor left-flushed *) 0 + + | Break when shallowAlign () -> (* An optional line break. Always a space + * followed by an optional line break *) + if !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 + 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; + 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; + abscol + + | Unmark -> begin + match !activeMarkups with + old :: rest -> activeMarkups := rest; + old + | [] -> failwith "Too many unmark" + end + + | _ -> (* Align level is too deep *) abscol + + +(** 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 + +(* The actual function that takes a document and prints it *) +let emitDoc + (emitString: string -> int -> unit) (* emit a number of copies of a + * string *) + (d: doc) = + let aligns: int list ref = ref [0] in (* A stack of alignment columns *) + + let wantIndent = ref false in + (* Use this function to take a newline *) + (* AB: modified it to flag wantIndent. The actual indentation is done only + if leftflush is not encountered *) + let newline () = + match !aligns with + [] -> failwith "Ran out of aligns" + | x :: _ -> + emitString "\n" 1; + incr countNewLines; + wantIndent := true; + x + in + (* Print indentation if wantIndent was previously flagged ; reset this flag *) + let indentIfNeeded () = + if !printIndent && !wantIndent then ignore ( + match !aligns with + [] -> failwith "Ran out of aligns" + | x :: _ -> + if x > 0 then emitString " " x; + x); + wantIndent := false + in + (* A continuation passing style loop *) + let rec loopCont (abscol: int) (d: doc) (cont: int -> unit) : unit + (* the new column *) = + match d with + Nil -> cont abscol + | Concat (d1, d2) -> + loopCont abscol d1 (fun abscol' -> loopCont abscol' d2 cont) + + | Text s when shallowAlign () -> + let sl = String.length s in + indentIfNeeded (); + emitString s 1; + cont (abscol + sl) + + | CText (d, s) -> + loopCont abscol d + (fun abscol' -> + if shallowAlign () then + let sl = String.length s in + indentIfNeeded (); + emitString s 1; + cont (abscol' + sl) + else + cont abscol') + + | Align -> + aligns := abscol :: !aligns; + if enterAlign () then begin + indentIfNeeded (); + emitString "..." 1; + cont (abscol + 3) + end else + cont abscol + + | Unalign -> begin + match !aligns with + [] -> failwith "Unmatched unalign" + | _ :: rest -> + exitAlign (); + aligns := rest; cont abscol + end + | Line when shallowAlign () -> cont (newline ()) + | LeftFlush when shallowAlign () -> wantIndent := false; cont (0) + | Break when shallowAlign () -> begin + match !breaks with + [] -> failwith "Break without a takenref" + | istaken :: rest -> + breaks := rest; (* Consume the break *) + if !istaken then cont (newline ()) + else begin + indentIfNeeded (); + emitString " " 1; + cont (abscol + 1) + end + end + + | Mark -> + activeMarkups := abscol :: !activeMarkups; + cont abscol + + | Unmark -> begin + match !activeMarkups with + old :: rest -> activeMarkups := rest; + cont old + | [] -> failwith "Unmark without a mark" + end + + | _ -> (* Align is too deep *) + cont abscol + in + + loopCont 0 d (fun x -> ()) + + +(* Print a document on a channel *) +let fprint (chn: out_channel) ~(width: int) doc = + (* Save some parameters, to allow for nested calls of these routines. *) + maxCol := width; + let old_breaks = !breaks in + breaks := []; + let old_alignDepth = !alignDepth in + alignDepth := 0; + let old_activeMarkups = !activeMarkups in + activeMarkups := []; + ignore (scan 0 doc); + breaks := List.rev !breaks; + ignore (emitDoc + (fun s nrcopies -> + for i = 1 to nrcopies do + output_string chn s + done) doc); + activeMarkups := old_activeMarkups; + alignDepth := old_alignDepth; + breaks := old_breaks (* We must do this especially if we don't do emit + * (which consumes breaks) because otherwise we waste + * memory *) + +(* Print the document to a string *) +let sprint ~(width : int) doc : string = + maxCol := width; + let old_breaks = !breaks in + breaks := []; + let old_activeMarkups = !activeMarkups in + activeMarkups := []; + let old_alignDepth = !alignDepth in + alignDepth := 0; + ignore (scan 0 doc); + breaks := List.rev !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; + breaks := old_breaks; + activeMarkups := old_activeMarkups; + alignDepth := old_alignDepth; + Buffer.contents buf + + + (* The rest is based on printf.ml *) +external format_int: string -> int -> string = "caml_format_int" +external format_float: string -> float -> string = "caml_format_float" + + + +let gprintf (finish : doc -> 'b) + (format : ('a, unit, doc, 'b) format4) : 'a = + let format = (Obj.magic format : string) in + + (* Record the starting align depth *) + let startAlignDepth = !alignDepth in + (* Special concatenation functions *) + let dconcat (acc: doc) (another: doc) = + if !alignDepth > !printDepth then acc else acc ++ another in + let dctext1 (acc: doc) (str: string) = + if !alignDepth > !printDepth then acc else + CText(acc, str) + in + (* Special finish function *) + let dfinish (dc: doc) : 'b = + if !alignDepth <> startAlignDepth then + prerr_string ("Unmatched align/unalign in " ^ format ^ "\n"); + finish dc + in + let flen = String.length format in + (* Reading a format character *) + let fget = String.unsafe_get format in + (* Output a literal sequence of + * characters, starting at i. The + * character at i does not need to be + * checked. *) + let rec literal acc i = + let rec skipChars j = + if j >= flen || + (match fget j with + '%' -> true + | '@' -> true + | '\n' -> true + | _ -> false) then + collect (dctext1 acc (String.sub format i (j-i))) j + else + skipChars (succ j) + in + skipChars (succ i) + (* the main collection function *) + and collect (acc: doc) (i: int) = + if i >= flen then begin + Obj.magic (dfinish acc) + end else begin + let c = fget i in + if c = '%' then begin + let j = skip_args (succ i) in + match fget j with + '%' -> literal acc j + | 's' -> + Obj.magic(fun s -> + let str = + if j <= i+1 then + s + else + let sl = String.length s in + let p = + try + int_of_string (String.sub format (i+1) (j-i-1)) + with _ -> + invalid_arg "fprintf: bad %s format" in + if p > 0 && sl < p then + (String.make (p - sl) ' ') ^ s + else if p < 0 && sl < -p then + s ^ (String.make (-p - sl) ' ') + else + s + in + collect (breakString acc str) (succ j)) + | 'c' -> + Obj.magic(fun c -> + collect (dctext1 acc (String.make 1 c)) (succ j)) + | 'd' | 'i' | 'o' | 'x' | 'X' | 'u' -> + Obj.magic(fun n -> + collect (dctext1 acc + (format_int (String.sub format i + (j-i+1)) n)) + (succ j)) + (* L, l, and n are the Int64, Int32, and Nativeint modifiers to the integer + formats d,i,o,x,X,u. For example, %Lo means print an Int64 in octal.*) + | 'L' -> + if j != i + 1 then (*Int64.format handles simple formats like %d. + * Any special flags eaten by skip_args will confuse it. *) + invalid_arg ("dprintf: unimplemented format " + ^ (String.sub format i (j-i+1))); + let j' = succ j in (* eat the d,i,x etc. *) + let format_spec = "% " in + String.set format_spec 1 (fget j'); (* format_spec = "%x", etc. *) + Obj.magic(fun n -> + collect (dctext1 acc + (Int64.format format_spec n)) + (succ j')) + | 'l' -> + if j != i + 1 then invalid_arg ("dprintf: unimplemented format " + ^ (String.sub format i (j-i+1))); + let j' = succ j in (* eat the d,i,x etc. *) + let format_spec = "% " in + String.set format_spec 1 (fget j'); (* format_spec = "%x", etc. *) + Obj.magic(fun n -> + collect (dctext1 acc + (Int32.format format_spec n)) + (succ j')) + | 'n' -> + if j != i + 1 then invalid_arg ("dprintf: unimplemented format " + ^ (String.sub format i (j-i+1))); + let j' = succ j in (* eat the d,i,x etc. *) + let format_spec = "% " in + String.set format_spec 1 (fget j'); (* format_spec = "%x", etc. *) + Obj.magic(fun n -> + collect (dctext1 acc + (Nativeint.format format_spec n)) + (succ j')) + | 'f' | 'e' | 'E' | 'g' | 'G' -> + Obj.magic(fun f -> + collect (dctext1 acc + (format_float (String.sub format i (j-i+1)) f)) + (succ j)) + | 'b' | 'B' -> + Obj.magic(fun b -> + collect (dctext1 acc (string_of_bool b)) (succ j)) + | 'a' -> + Obj.magic(fun pprinter arg -> + collect (dconcat acc (pprinter () arg)) (succ j)) + | 't' -> + Obj.magic(fun pprinter -> + collect (dconcat acc (pprinter ())) (succ j)) + | c -> + invalid_arg ("dprintf: unknown format %s" ^ String.make 1 c) + + end else if c = '@' then begin + if i + 1 < flen then begin + match fget (succ i) with + + (* Now the special format characters *) + '[' -> (* align *) + let newacc = + if !alignDepth > !printDepth then + acc + else if !alignDepth = !printDepth then + CText(acc, "...") + else + acc ++ align + in + incr alignDepth; + collect newacc (i + 2) + + | ']' -> (* unalign *) + decr alignDepth; + let newacc = + if !alignDepth >= !printDepth then + acc + else + acc ++ unalign + in + collect newacc (i + 2) + | '!' -> (* hard-line break *) + collect (dconcat acc line) (i + 2) + | '?' -> (* soft line break *) + collect (dconcat acc (break)) (i + 2) + | '<' -> + collect (dconcat acc mark) (i +1) + | '>' -> + collect (dconcat acc unmark) (i +1) + | '^' -> (* left-flushed *) + collect (dconcat acc (leftflush)) (i + 2) + | '@' -> + collect (dctext1 acc "@") (i + 2) + | c -> + invalid_arg ("dprintf: unknown format @" ^ String.make 1 c) + end else + invalid_arg "dprintf: incomplete format @" + end else if c = '\n' then begin + collect (dconcat acc line) (i + 1) + end else + literal acc i + end + + and skip_args j = + match String.unsafe_get format j with + '0' .. '9' | ' ' | '.' | '-' -> skip_args (succ j) + | c -> j + + in + collect Nil 0 + +let withPrintDepth dp thunk = + let opd = !printDepth in + printDepth := dp; + thunk (); + printDepth := opd + + + +let flushOften = ref false + +let dprintf format = gprintf (fun x -> x) format +let fprintf chn format = + let f d = fprint chn 80 d; d in + (* weimeric hack begins -- flush output to streams *) + let res = gprintf f format in + (* save the value we would have returned, flush the channel and then + * return it -- this allows us to see debug input near infinite loops + * *) + if !flushOften then flush chn; + res + (* weimeric hack ends *) + +let printf format = fprintf stdout format +let eprintf format = fprintf stderr format + + + +(******************************************************************************) +let getAlgoName = function + George -> "George" + | Aman -> "Aman" + | Gap -> "Gap" + +let getAboutString () : string = + "(Pretty: ALGO=" ^ (getAlgoName algo) ^ ")" + + +(************************************************) +let auto_printer (typ: string) = + failwith ("Pretty.auto_printer \"" ^ typ ^ "\" only works with you use -pp \"camlp4o pa_prtype.cmo\" when you compile") diff --git a/cil/ocamlutil/pretty.mli b/cil/ocamlutil/pretty.mli new file mode 100644 index 00000000..5422432d --- /dev/null +++ b/cil/ocamlutil/pretty.mli @@ -0,0 +1,316 @@ +(* + * + * Copyright (c) 2001 by + * George C. Necula necula@cs.berkeley.edu + * Scott McPeak smcpeak@cs.berkeley.edu + * Wes Weimer weimer@cs.berkeley.edu + * + * All rights reserved. Permission to use, copy, modify and distribute + * this software for research purposes only is hereby granted, + * provided that the following conditions are met: + * 1. Redistributions of source code must retain the above copyright notice, + * this list of conditions and the following disclaimer. + * 2. Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * 3. The name of the authors may not be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * DISCLAIMER: + * THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS OR + * IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES + * OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. + * IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY DIRECT, INDIRECT, + * INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, + * BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS + * OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON + * ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT + * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF + * THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + *) + +(** Utility functions for pretty-printing. The major features provided by + this module are +- An [fprintf]-style interface with support for user-defined printers +- The printout is fit to a width by selecting some of the optional newlines +- Constructs for alignment and indentation +- Print ellipsis starting at a certain nesting depth +- Constructs for printing lists and arrays + + Pretty-printing occurs in two stages: +- Construct a {!Pretty.doc} object that encodes all of the elements to be + printed + along with alignment specifiers and optional and mandatory newlines +- Format the {!Pretty.doc} to a certain width and emit it as a string, to an + output stream or pass it to a user-defined function + + The formatting algorithm is not optimal but it does a pretty good job while + still operating in linear time. The original version was based on a pretty + printer by Philip Wadler which turned out to not scale to large jobs. +*) + +(** API *) + +(** 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. + * The {!Pretty.dprintf} method is slightly slower so we do not use it for + * large jobs such as the output routines for a compiler. But we use it for + * small jobs such as logging and error messages. *) +type doc + + + +(** Constructors for the doc type. *) + + + + +(** Constructs an empty document *) +val nil : doc + + +(** Concatenates two documents. This is an infix operator that associates to + the left. *) +val (++) : doc -> doc -> doc +val concat : doc -> doc -> doc + +(** A document that prints the given string *) +val text : string -> doc + + +(** A document that prints an integer in decimal form *) +val num : int -> doc + + +(** A document that prints a real number *) +val real : float -> doc + +(** A document that prints a character. This is just like {!Pretty.text} + with a one-character string. *) +val chr : char -> doc + + +(** A document that consists of a mandatory newline. This is just like [(text + "\n")]. The new line will be indented to the current indentation level, + unless you use {!Pretty.leftflush} right after this. *) +val line : doc + +(** Use after a {!Pretty.line} to prevent the indentation. Whatever follows + * next will be flushed left. Indentation resumes on the next line. *) +val leftflush : doc + + +(** A document that consists of either a space or a line break. Also called + an optional line break. Such a break will be + taken only if necessary to fit the document in a given width. If the break + is not taken a space is printed instead. *) +val break: doc + +(** Mark the current column as the current indentation level. Does not print + anything. All taken line breaks will align to this column. The previous + alignment level is saved on a stack. *) +val align: doc + +(** Reverts to the last saved indentation level. *) +val unalign: doc + + +(** Mark the beginning of a markup section. The width of a markup section is + * considered 0 for the purpose of computing identation *) +val mark: doc + +(** The end of a markup section *) +val unmark: doc + +(************* Now some syntactic sugar *****************) +(** Syntactic sugar *) + +(** Indents the document. Same as [((text " ") ++ align ++ doc ++ unalign)], + with the specified number of spaces. *) +val indent: int -> doc -> doc + +(** Prints a document as markup. The marked document cannot contain line + * breaks or alignment constructs. *) +val markup: doc -> doc + +(** Formats a sequence. [sep] is a separator, [doit] is a function that + * converts an element to a document. *) +val seq: sep:doc -> doit:('a ->doc) -> elements:'a list -> doc + + +(** An alternative function for printing a list. The [unit] argument is there + * to make this function more easily usable with the {!Pretty.dprintf} + * interface. The first argument is a separator, by default a comma. *) +val docList: ?sep:doc -> ('a -> doc) -> unit -> 'a list -> doc + +(** sm: Yet another list printer. This one accepts the same kind of + * printing function that {!Pretty.dprintf} does, and itself works + * in the dprintf context. Also accepts + * a string as the separator since that's by far the most common. *) +val d_list: string -> (unit -> 'a -> doc) -> unit -> 'a list -> doc + +(** Formats an array. A separator and a function that prints an array + element. The default separator is a comma. *) +val docArray: ?sep:doc -> (int -> 'a -> doc) -> unit -> 'a array -> doc + +(** Prints an ['a option] with [None] or [Some] *) +val docOpt: ('a -> doc) -> unit -> 'a option -> doc + + +(** Print an int32 *) +val d_int32: int32 -> doc +val f_int32: unit -> int32 -> doc + +val d_int64: int64 -> doc +val f_int64: unit -> int64 -> doc + +(** Format maps. *) +module MakeMapPrinter : + functor (Map: sig + type key + type 'a t + val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b + end) -> +sig + (** Format a map, analogous to docList. *) + val docMap: ?sep:doc -> (Map.key -> 'a -> doc) -> unit -> 'a Map.t -> doc + + (** Format a map, analogous to d_list. *) + val d_map: ?dmaplet:(doc -> doc -> doc) + -> string + -> (unit -> Map.key -> doc) + -> (unit -> 'a -> doc) + -> unit + -> 'a Map.t + -> doc + end + +(** Format sets. *) +module MakeSetPrinter : + functor (Set: sig + type elt + type t + val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a + end) -> +sig + (** Format a set, analogous to docList. *) + val docSet: ?sep:doc -> (Set.elt -> doc) -> unit -> Set.t -> doc + + (** Format a set, analogous to d_list. *) + val d_set: string + -> (unit -> Set.elt -> doc) + -> unit + -> Set.t + -> doc +end + +(** A function that is useful with the [printf]-like interface *) +val insert: unit -> doc -> doc + +val dprintf: ('a, unit, doc, doc) format4 -> 'a +(** This function provides an alternative method for constructing + [doc] objects. The first argument for this function is a format string + argument (of type [('a, unit, doc) format]; if you insist on + understanding what that means see the module [Printf]). The format string + is like that for the [printf] function in C, except that it understands a + few more formatting controls, all starting with the @ character. + + See the gprintf function if you want to pipe the result of dprintf into + some other functions. + + The following special formatting characters are understood (these do not + correspond to arguments of the function): +- @\[ Inserts an {!Pretty.align}. Every format string must have matching + {!Pretty.align} and {!Pretty.unalign}. +- @\] Inserts an {!Pretty.unalign}. +- @! Inserts a {!Pretty.line}. Just like "\n" +- @? Inserts a {!Pretty.break}. +- @< Inserts a {!Pretty.mark}. +- @> Inserts a {!Pretty.unmark}. +- @^ Inserts a {!Pretty.leftflush} + Should be used immediately after @! or "\n". +- @@ : inserts a @ character + + In addition to the usual [printf] % formatting characters the following two + new characters are supported: +- %t Corresponds to an argument of type [unit -> doc]. This argument is + invoked to produce a document +- %a Corresponds to {b two} arguments. The first of type [unit -> 'a -> doc] + and the second of type ['a]. (The extra [unit] is do to the + peculiarities of the built-in support for format strings in Ocaml. It + turns out that it is not a major problem.) Here is an example of how + you use this: + +{v dprintf "Name=%s, SSN=%7d, Children=\@\[%a\@\]\n" + pers.name pers.ssn (docList (chr ',' ++ break) text) + pers.children v} + + The result of [dprintf] is a {!Pretty.doc}. You can format the document and + emit it using the functions {!Pretty.fprint} and {!Pretty.sprint}. + +*) + +(** Like {!Pretty.dprintf} but more general. It also takes a function that is + * invoked on the constructed document but before any formatting is done. The + * type of the format argument means that 'a is the type of the parameters of + * this function, unit is the type of the first argument to %a and %t + * formats, doc is the type of the intermediate result, and 'b is the type of + * the result of gprintf. *) +val gprintf: (doc -> 'b) -> ('a, unit, doc, 'b) format4 -> 'a + +(** Format the document to the given width and emit it to the given channel *) +val fprint: out_channel -> width:int -> doc -> unit + +(** Format the document to the given width and emit it as a string *) +val sprint: width:int -> doc -> string + +(** Like {!Pretty.dprintf} followed by {!Pretty.fprint} *) +val fprintf: out_channel -> ('a, unit, doc) format -> 'a + +(** Like {!Pretty.fprintf} applied to [stdout] *) +val printf: ('a, unit, doc) format -> 'a + +(** Like {!Pretty.fprintf} applied to [stderr] *) +val eprintf: ('a, unit, doc) format -> 'a + + +(* sm: arg! why can't I write this function?! *) +(* * Like {!Pretty.dprintf} but yielding a string with no newlines *) +(*val sprintf: (doc, unit, doc) format -> string*) + +(* sm: different tack.. *) +(* doesn't work either. well f it anyway *) +(*val failwithf: ('a, unit, doc) format -> 'a*) + + +(** Invokes a thunk, with printDepth temporarily set to the specified value *) +val withPrintDepth : int -> (unit -> unit) -> unit + +(** The following variables can be used to control the operation of the printer *) + +(** Specifies the nesting depth of the [align]/[unalign] pairs at which + everything is replaced with ellipsis *) +val printDepth : int ref + +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 flushOften : bool ref (** If true the it flushes after every print *) + + +(** 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 + + +(** A function that when used at top-level in a module will direct + * the pa_prtype module generate automatically the printing functions for a + * type *) +val auto_printer: string -> 'b diff --git a/cil/ocamlutil/stats.ml b/cil/ocamlutil/stats.ml new file mode 100644 index 00000000..8bbb7d05 --- /dev/null +++ b/cil/ocamlutil/stats.ml @@ -0,0 +1,146 @@ +(* The following functions are implemented in perfcount.c *) + +(* Returns true is we have the performance counters *) +external has_performance_counters: unit -> bool = "has_performance_counters" + +(* Returns number of seconds since the first read *) +external read_pentium_perfcount : unit -> float = "read_pentium_perfcount" + +(* Returns current cycle counter, divided by 1^20, and truncated to 30 bits *) +external sample_pentium_perfcount_20 : unit -> int = "sample_pentium_perfcount_20" + +(* Returns current cycle counter, divided by 1^10, and truncated to 30 bits *) +external sample_pentium_perfcount_10 : unit -> int = "sample_pentium_perfcount_10" + + +(* Whether to use the performance counters (on Pentium only) *) + +(* The performance counters are disabled by default. *) +let do_use_performance_counters = ref false + + (* A hierarchy of timings *) + +type t = { name : string; + mutable time : float; (* In seconds *) + mutable sub : t list} + + (* Create the top level *) +let top = { name = "TOTAL"; + time = 0.0; + sub = []; } + + (* The stack of current path through + * the hierarchy. The first is the + * leaf. *) +let current : t list ref = ref [top] + +exception NoPerfCount +let reset (perfcount: bool) = + top.sub <- []; + if perfcount then begin + if not (has_performance_counters ()) then begin + raise NoPerfCount + end + end; + do_use_performance_counters := perfcount + + + +let print chn msg = + (* Total up *) + top.time <- List.fold_left (fun sum f -> sum +. f.time) 0.0 top.sub; + let rec prTree ind node = + if !do_use_performance_counters then + (Printf.fprintf chn "%s%-20s %8.5f s\n" + (String.make ind ' ') node.name node.time) + else + (Printf.fprintf chn "%s%-20s %6.3f s\n" + (String.make ind ' ') node.name node.time); + + List.iter (prTree (ind + 2)) (List.rev node.sub) + in + Printf.fprintf chn "%s" msg; + List.iter (prTree 0) [ top ]; + Printf.fprintf chn "Timing used %s\n" + (if !do_use_performance_counters then "Pentium performance counters" + else "Unix.time"); + let gc = Gc.quick_stat () in + let printM (w: float) : string = + Printf.sprintf "%.2fMb" (w *. 4.0 /. 1000000.0) + in + Printf.fprintf chn + "Memory statistics: total=%s, max=%s, minor=%s, major=%s, promoted=%s\n minor collections=%d major collections=%d compactions=%d\n" + (printM (gc.Gc.minor_words +. gc.Gc.major_words + -. gc.Gc.promoted_words)) + (printM (float_of_int gc.Gc.top_heap_words)) + (printM gc.Gc.minor_words) + (printM gc.Gc.major_words) + (printM gc.Gc.promoted_words) + gc.Gc.minor_collections + gc.Gc.major_collections + gc.Gc.compactions; + + () + + + +(* Get the current time, in seconds *) +let get_current_time () : float = + if !do_use_performance_counters then + read_pentium_perfcount () + else + (Unix.times ()).Unix.tms_utime + +let repeattime limit str f arg = + (* Find the right stat *) + let stat : t = + let curr = match !current with h :: _ -> h | _ -> assert false in + let rec loop = function + h :: _ when h.name = str -> h + | _ :: rest -> loop rest + | [] -> + let nw = {name = str; time = 0.0; sub = []} in + curr.sub <- nw :: curr.sub; + nw + in + loop curr.sub + in + let oldcurrent = !current in + current := stat :: oldcurrent; + let start = get_current_time () in + let rec repeatf count = + let res = f arg in + let diff = get_current_time () -. start in + if diff < limit then + repeatf (count + 1) + else begin + stat.time <- stat.time +. (diff /. float(count)); + current := oldcurrent; (* Pop the current stat *) + res (* Return the function result *) + end + in + repeatf 1 + + +let time str f arg = repeattime 0.0 str f arg + + +let lastTime = ref 0.0 +let timethis (f: 'a -> 'b) (arg: 'a) : 'b = + let start = get_current_time () in + let res = f arg in + lastTime := get_current_time () -. start; + res + + + + + + + + + + + + + diff --git a/cil/ocamlutil/stats.mli b/cil/ocamlutil/stats.mli new file mode 100644 index 00000000..9ed98e56 --- /dev/null +++ b/cil/ocamlutil/stats.mli @@ -0,0 +1,72 @@ +(* + * + * Copyright (c) 2001 by + * George C. Necula necula@cs.berkeley.edu + * Scott McPeak smcpeak@cs.berkeley.edu + * Wes Weimer weimer@cs.berkeley.edu + * + * All rights reserved. Permission to use, copy, modify and distribute + * this software for research purposes only is hereby granted, + * provided that the following conditions are met: + * 1. Redistributions of source code must retain the above copyright notice, + * this list of conditions and the following disclaimer. + * 2. Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * 3. The name of the authors may not be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * DISCLAIMER: + * THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS OR + * IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES + * OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. + * IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY DIRECT, INDIRECT, + * INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, + * BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS + * OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON + * ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT + * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF + * THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + *) + +(** Utilities for maintaining timing statistics *) + +(** Resets all the timings. Invoke with "true" if you want to switch to using + * the hardware performance counters from now on. You get an exception if + * there are not performance counters available *) +val reset: bool -> unit +exception NoPerfCount + +(** Check if we have performance counters *) +val has_performance_counters: unit -> bool + +(** Sample the current cycle count, in megacycles. *) +val sample_pentium_perfcount_20: unit -> int + +(** Sample the current cycle count, in kilocycles. *) +val sample_pentium_perfcount_10: unit -> int + +(** Time a function and associate the time with the given string. If some + timing information is already associated with that string, then accumulate + the times. If this function is invoked within another timed function then + you can have a hierarchy of timings *) +val time : string -> ('a -> 'b) -> 'a -> 'b + +(** repeattime is like time but runs the function several times until the total + running time is greater or equal to the first argument. The total time is + then divided by the number of times the function was run. *) +val repeattime : float -> string -> ('a -> 'b) -> 'a -> 'b + +(** Print the current stats preceeded by a message *) +val print : out_channel -> string -> unit + + + +(** Time a function and set lastTime to the time it took *) +val lastTime: float ref +val timethis: ('a -> 'b) -> 'a -> 'b + + + + diff --git a/cil/ocamlutil/trace.ml b/cil/ocamlutil/trace.ml new file mode 100644 index 00000000..b4292865 --- /dev/null +++ b/cil/ocamlutil/trace.ml @@ -0,0 +1,169 @@ +(* + * + * Copyright (c) 2001-2002, + * George C. Necula + * Scott McPeak + * Wes Weimer + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * + * 3. The names of the contributors may not be used to endorse or promote + * products derived from this software without specific prior written + * permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS + * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED + * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A + * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER + * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + *) + +(* Trace module implementation + * see trace.mli + *) + +open Pretty;; + + +(* --------- traceSubsystems --------- *) +(* this is the list of tags (usually subsystem names) for which + * trace output will appear *) +let traceSubsystems : string list ref = ref [];; + + +let traceAddSys (subsys : string) : unit = + (* (ignore (printf "traceAddSys %s\n" subsys)); *) + traceSubsystems := subsys :: !traceSubsystems +;; + + +let traceActive (subsys : string) : bool = + (* (List.mem elt list) returns true if something in list equals ('=') elt *) + (List.mem subsys !traceSubsystems) +;; + + +let rec parseString (str : string) (delim : char) : string list = +begin + if (not (String.contains str delim)) then + if ((String.length str) = 0) then + [] + else + [str] + + else + let d = ((String.index str delim) + 1) in + if (d = 1) then + (* leading delims are eaten *) + (parseString (String.sub str d ((String.length str) - d)) delim) + else + (String.sub str 0 (d-1)) :: + (parseString (String.sub str d ((String.length str) - d)) delim) +end;; + +let traceAddMulti (systems : string) : unit = +begin + let syslist = (parseString systems ',') in + (List.iter traceAddSys syslist) +end;; + + + +(* --------- traceIndent --------- *) +let traceIndentLevel : int ref = ref 0;; + + +let traceIndent (sys : string) : unit = + if (traceActive sys) then + traceIndentLevel := !traceIndentLevel + 2 +;; + +let traceOutdent (sys : string) : unit = + if ((traceActive sys) && + (!traceIndentLevel >= 2)) then + traceIndentLevel := !traceIndentLevel - 2 +;; + + +(* --------- trace --------- *) +(* return a tag to prepend to a trace output + * e.g. " %%% mysys: " + *) +let traceTag (sys : string) : Pretty.doc = + (* return string of 'i' spaces *) + let rec ind (i : int) : string = + if (i <= 0) then + "" + else + " " ^ (ind (i-1)) + + in + (text ((ind !traceIndentLevel) ^ "%%% " ^ sys ^ ": ")) +;; + + +(* this is the trace function; its first argument is a string + * tag, and subsequent arguments are like printf formatting + * strings ("%a" and whatnot) *) +let trace + (subsys : string) (* subsystem identifier for enabling tracing *) + (d : Pretty.doc) (* something made by 'dprintf' *) + : unit = (* no return value *) + (* (ignore (printf "trace %s\n" subsys)); *) + + (* see if the subsystem's tracing is turned on *) + if (traceActive subsys) then + begin + (fprint stderr 80 (* print it *) + ((traceTag subsys) ++ d)); (* with prepended subsys tag *) + (* mb: flush after every message; useful if the program hangs in an + infinite loop... *) + (flush stderr) + end + else + () (* eat it *) +;; + + +let tracei (sys : string) (d : Pretty.doc) : unit = + (* trace before indent *) + (trace sys d); + (traceIndent sys) +;; + +let traceu (sys : string) (d : Pretty.doc) : unit = + (* trace after outdent *) + (* no -- I changed my mind -- I want trace *then* outdent *) + (trace sys d); + (traceOutdent sys) +;; + + + + +(* -------------------------- trash --------------------- *) +(* TRASH START + +(* sm: more experimenting *) +(trace "no" (dprintf "no %d\n" 5)); +(trace "yes" (dprintf "yes %d\n" 6)); +(trace "maybe" (dprintf "maybe %d\n" 7)); + +TRASH END *) diff --git a/cil/ocamlutil/trace.mli b/cil/ocamlutil/trace.mli new file mode 100644 index 00000000..46ca6523 --- /dev/null +++ b/cil/ocamlutil/trace.mli @@ -0,0 +1,106 @@ +(* + * + * Copyright (c) 2001-2002, + * George C. Necula + * Scott McPeak + * Wes Weimer + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * + * 3. The names of the contributors may not be used to endorse or promote + * products derived from this software without specific prior written + * permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS + * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED + * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A + * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER + * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + *) + +(* Trace module + * Scott McPeak, 5/4/00 + * + * The idea is to pepper the source with debugging printfs, + * and be able to select which ones to actually display at + * runtime. + * + * It is built on top of the Pretty module for printing data + * structures. + * + * To a first approximation, this is needed to compensate for + * the lack of a debugger that does what I want... + *) + + +(* this is the list of tags (usually subsystem names) for which + * trace output will appear *) +val traceSubsystems : string list ref + +(* interface to add a new subsystem to trace (slightly more + * convenient than direclty changing 'tracingSubsystems') *) +val traceAddSys : string -> unit + +(* query whether a particular subsystem is being traced *) +val traceActive : string -> bool + +(* add several systems, separated by commas *) +val traceAddMulti : string -> unit + + +(* current indentation level for tracing *) +val traceIndentLevel : int ref + +(* bump up or down the indentation level, if the given subsys + * is being traced *) +val traceIndent : string -> unit +val traceOutdent : string -> unit + + +(* this is the trace function; its first argument is a string + * tag, and second argument is a 'doc' (which is what 'dprintf' + * returns). + * + * so a sample usage might be + * (trace "mysubsys" (dprintf "something neat happened %d times\n" counter)) + *) +val trace : string -> Pretty.doc -> unit + + +(* special flavors that indent/outdent as well. the indent version + * indents *after* printing, while the outdent version outdents + * *before* printing. thus, a sequence like + * + * (tracei "foo" (dprintf "beginning razzle-dazzle\n")) + * ..razzle.. + * ..dazzle.. + * (traceu "foo" (dprintf "done with razzle-dazzle\n")) + * + * will do the right thing + * + * update -- I changed my mind! I decided I prefer it like this + * %%% sys: (myfunc args) + * %%% ...inner stuff... + * %%% sys: myfunc returning 56 + * + * so now they both print before in/outdenting + *) +val tracei : string -> Pretty.doc -> unit +val traceu : string -> Pretty.doc -> unit diff --git a/cil/ocamlutil/util.ml b/cil/ocamlutil/util.ml new file mode 100755 index 00000000..e6c2c679 --- /dev/null +++ b/cil/ocamlutil/util.ml @@ -0,0 +1,815 @@ +(** Utility functions for Coolaid *) +module E = Errormsg +module H = Hashtbl +module IH = Inthash + +open Pretty + +exception GotSignal of int + +let withTimeout (secs: float) (* Seconds for timeout *) + (handler: int -> 'b) (* What to do if we have a timeout. The + * argument passed is the signal number + * received. *) + (f: 'a -> 'b) (* The function to run *) + (arg: 'a) (* And its argument *) + : 'b = + let oldHandler = + Sys.signal Sys.sigalrm + (Sys.Signal_handle + (fun i -> + ignore (E.log "Got signal %d\n" i); + raise (GotSignal i))) + in + let reset_sigalrm () = + ignore (Unix.setitimer Unix.ITIMER_REAL { Unix.it_value = 0.0; + Unix.it_interval = 0.0;}); + Sys.set_signal Sys.sigalrm oldHandler; + in + ignore (Unix.setitimer Unix.ITIMER_REAL + { Unix.it_value = secs; + Unix.it_interval = 0.0;}); + (* ignore (Unix.alarm 2); *) + try + let res = f arg in + reset_sigalrm (); + res + with exc -> begin + reset_sigalrm (); + ignore (E.log "Got an exception\n"); + match exc with + GotSignal i -> + handler i + | _ -> raise exc + end + +(** Print a hash table *) +let docHash ?(sep=chr ',') (one: 'a -> 'b -> doc) () (h: ('a, 'b) H.t) = + (H.fold + (fun key data acc -> + if acc == align then acc ++ one key data + else acc ++ sep ++ one key data) + h + align) ++ unalign + + + +let hash_to_list (h: ('a, 'b) H.t) : ('a * 'b) list = + H.fold + (fun key data acc -> (key, data) :: acc) + h + [] + +let keys (h: ('a, 'b) H.t) : 'a list = + H.fold + (fun key data acc -> key :: acc) + h + [] + +let hash_copy_into (hfrom: ('a, 'b) H.t) (hto: ('a, 'b) H.t) : unit = + H.clear hto; + H.iter (H.add hto) hfrom + +let anticompare a b = compare b a +;; + + +let rec list_drop (n : int) (xs : 'a list) : 'a list = + if n < 0 then invalid_arg "Util.list_drop"; + if n = 0 then + xs + else begin + match xs with + | [] -> invalid_arg "Util.list_drop" + | y::ys -> list_drop (n-1) ys + end + +let list_droptail (n : int) (xs : 'a list) : 'a list = + if n < 0 then invalid_arg "Util.list_droptail"; + let (ndrop,r) = + List.fold_right + (fun x (ndrop,acc) -> + if ndrop = 0 then (ndrop, x :: acc) + else (ndrop-1, acc)) + xs + (n,[]) + in + if ndrop > 0 then invalid_arg "Util.listdroptail" + else r + +let rec list_span (p : 'a -> bool) (xs : 'a list) : 'a list * 'a list = + begin match xs with + | [] -> ([],[]) + | x::xs' -> + if p x then + let (ys,zs) = list_span p xs' in (x::ys,zs) + else ([],xs) + end +;; + +let rec list_rev_append revxs ys = + begin match revxs with + | [] -> ys + | x::xs -> list_rev_append xs (x::ys) + end +;; +let list_insert_by (cmp : 'a -> 'a -> int) + (x : 'a) (xs : 'a list) : 'a list = + let rec helper revhs ts = + begin match ts with + | [] -> List.rev (x::revhs) + | t::ts' -> + if cmp x t >= 0 then helper (t::revhs) ts' + else list_rev_append (x::revhs) ts + end + in + helper [] xs +;; + +let list_head_default (d : 'a) (xs : 'a list) : 'a = + begin match xs with + | [] -> d + | x::_ -> x + end +;; + +let rec list_iter3 f xs ys zs = + begin match xs, ys, zs with + | [], [], [] -> () + | x::xs, y::ys, z::zs -> f x y z; list_iter3 f xs ys zs + | _ -> invalid_arg "Util.list_iter3" + end +;; + +let rec get_some_option_list (xs : 'a option list) : 'a list = + begin match xs with + | [] -> [] + | None::xs -> get_some_option_list xs + | Some x::xs -> x :: get_some_option_list xs + end +;; + +(* tail-recursive append: reverses xs twice *) +let list_append (xs: 'a list) (ys: 'a list): 'a list = + match xs with (* optimize some common cases *) + [] -> ys + | [x] -> x::ys + | _ -> list_rev_append (List.rev xs) ys + +let list_iteri (f: int -> 'a -> unit) (l: 'a list) : unit = + let rec loop (i: int) (l: 'a list) : unit = + match l with + [] -> () + | h :: t -> f i h; loop (i + 1) t + in + loop 0 l + +let list_mapi (f: int -> 'a -> 'b) (l: 'a list) : 'b list = + let rec loop (i: int) (l: 'a list) : 'b list = + match l with + [] -> [] + | h :: t -> + let headres = f i h in + headres :: loop (i + 1) t + in + loop 0 l + +let list_fold_lefti (f: 'acc -> int -> 'a -> 'acc) (start: 'acc) + (l: 'a list) : 'acc = + let rec loop (i, acc) l = + match l with + [] -> acc + | h :: t -> loop (i + 1, f acc i h) t + in + loop (0, start) l + + +let list_init (len : int) (init_fun : int -> 'a) : 'a list = + let rec loop n acc = + if n < 0 then acc + else loop (n-1) ((init_fun n)::acc) + in + loop (len - 1) [] +;; + + +let rec list_find_first (l: 'a list) (f: 'a -> 'b option) : 'b option = + match l with + [] -> None + | h :: t -> begin + match f h with + None -> list_find_first t f + | r -> r + end + +(** Generates the range of integers starting with a and ending with b *) +let int_range_list (a: int) (b: int) = + list_init (b - a + 1) (fun i -> a + i) + + +(** Some handling of registers *) +type 'a growArrayFill = + Elem of 'a + | Susp of (int -> 'a) + +type 'a growArray = { + gaFill: 'a growArrayFill; + (** Stuff to use to fill in the array as it grows *) + + mutable gaMaxInitIndex: int; + (** Maximum index that was written to. -1 if no writes have + * been made. *) + + mutable gaData: 'a array; + } + +let growTheArray (ga: 'a growArray) (len: int) + (toidx: int) (why: string) : unit = + if toidx >= len then begin + (* Grow the array by 50% *) + let newlen = toidx + 1 + len / 2 in +(* + ignore (E.log "growing an array to idx=%d (%s)\n" toidx why); +*) + let data' = begin match ga.gaFill with + Elem x -> + + let data'' = Array.create newlen x in + Array.blit ga.gaData 0 data'' 0 len; + data'' + | Susp f -> Array.init newlen + (fun i -> if i < len then ga.gaData.(i) else f i) + end + in + ga.gaData <- data' + end + +let getReg (ga: 'a growArray) (r: int) : 'a = + let len = Array.length ga.gaData in + if r >= len then + growTheArray ga len r "get"; + + ga.gaData.(r) + +let setReg (ga: 'a growArray) (r: int) (what: 'a) : unit = + let len = Array.length ga.gaData in + if r >= len then + growTheArray ga len r "set"; + if r > ga.gaMaxInitIndex then ga.gaMaxInitIndex <- r; + ga.gaData.(r) <- what + +let newGrowArray (initsz: int) (fill: 'a growArrayFill) : 'a growArray = + { gaFill = fill; + gaMaxInitIndex = -1; + gaData = begin match fill with + Elem x -> Array.create initsz x + | Susp f -> Array.init initsz f + end; } + +let copyGrowArray (ga: 'a growArray) : 'a growArray = + { ga with gaData = Array.copy ga.gaData } + +let deepCopyGrowArray (ga: 'a growArray) (copy: 'a -> 'a): 'a growArray = + { ga with gaData = Array.map copy ga.gaData } + + + +(** Iterate over the initialized elements of the array *) +let growArray_iteri (f: int -> 'a -> unit) (ga: 'a growArray) = + for i = 0 to ga.gaMaxInitIndex do + f i ga.gaData.(i) + done + + +(** Fold left over the initialized elements of the array *) +let growArray_foldl (f: 'acc -> 'a -> 'acc) + (acc: 'acc) (ga: 'a growArray) : 'acc = + let rec loop (acc: 'acc) (idx: int) : 'acc = + if idx > ga.gaMaxInitIndex then + acc + else + loop (f acc ga.gaData.(idx)) (idx + 1) + in + loop acc 0 + + + + +let hasPrefix (prefix: string) (what: string) : bool = + let pl = String.length prefix in + try String.sub what 0 pl = prefix + with Invalid_argument _ -> false + + + +let restoreRef ?(deepCopy=(fun x -> x)) (r: 'a ref) : (unit -> unit) = + let old = deepCopy !r in + (fun () -> r := old) + +let restoreHash ?deepCopy (h: ('a, 'b) H.t) : (unit -> unit) = + let old = + match deepCopy with + None -> H.copy h + | Some f -> + let old = H.create (H.length h) in + H.iter (fun k d -> H.add old k (f d)) h; + old + in + (fun () -> hash_copy_into old h) + +let restoreIntHash ?deepCopy (h: 'a IH.t) : (unit -> unit) = + let old = + match deepCopy with + None -> IH.copy h + | Some f -> + let old = IH.create 13 in + IH.iter (fun k d -> IH.add old k (f d)) h; + old + in + (fun () -> + IH.clear old; + IH.iter (fun i k -> IH.add old i k) h) + +let restoreArray ?deepCopy (a: 'a array) : (unit -> unit) = + let old = Array.copy a in + (match deepCopy with + None -> () + | Some f -> Array.iteri (fun i v -> old.(i) <- f v) old); + (fun () -> Array.blit old 0 a 0 (Array.length a)) + +let runThunks (l: (unit -> unit) list) : (unit -> unit) = + fun () -> List.iter (fun f -> f ()) l + + + +(* Memoize *) +let memoize (h: ('a, 'b) Hashtbl.t) + (arg: 'a) + (f: 'a -> 'b) : 'b = + try + Hashtbl.find h arg + with Not_found -> begin + let res = f arg in + Hashtbl.add h arg res; + res + end + +(* Just another name for memoize *) +let findOrAdd h arg f = memoize h arg f + +(* A tryFinally function *) +let tryFinally + (main: 'a -> 'b) (* The function to run *) + (final: 'b option -> unit) (* Something to run at the end *) + (arg: 'a) : 'b = + try + let res: 'b = main arg in + final (Some res); + res + with e -> begin + final None; + raise e + end + + + + +let valOf : 'a option -> 'a = function + None -> raise (Failure "Util.valOf") + | Some x -> x + +(** + * An accumulating for loop. + * + * Initialize the accumulator with init. The current index and accumulator + * from the previous iteration is passed to f. + *) +let fold_for ~(init: 'a) ~(lo: int) ~(hi: int) (f: int -> 'a -> 'a) = + let rec forloop i acc = + if i > hi then acc + else forloop (i+1) (f i acc) + in + forloop lo init + +(************************************************************************) + +module type STACK = sig + type 'a t + (** The type of stacks containing elements of type ['a]. *) + + exception Empty + (** Raised when {!Stack.pop} or {!Stack.top} is applied to an empty stack. *) + + val create : unit -> 'a t + (** Return a new stack, initially empty. *) + + val push : 'a -> 'a t -> unit + (** [push x s] adds the element [x] at the top of stack [s]. *) + + val pop : 'a t -> 'a + (** [pop s] removes and returns the topmost element in stack [s], + or raises [Empty] if the stack is empty. *) + + val top : 'a t -> 'a + (** [top s] returns the topmost element in stack [s], + or raises [Empty] if the stack is empty. *) + + val clear : 'a t -> unit + (** Discard all elements from a stack. *) + + val copy : 'a t -> 'a t + (** Return a copy of the given stack. *) + + val is_empty : 'a t -> bool + (** Return [true] if the given stack is empty, [false] otherwise. *) + + val length : 'a t -> int + (** Return the number of elements in a stack. *) + + val iter : ('a -> unit) -> 'a t -> unit + (** [iter f s] applies [f] in turn to all elements of [s], + from the element at the top of the stack to the element at the + bottom of the stack. The stack itself is unchanged. *) +end + +module Stack = struct + + type 'a t = { mutable length : int; + stack : 'a Stack.t; } + + exception Empty + + let create () = { length = 0; + stack = Stack.create(); } + + let push x s = + s.length <- s.length + 1; + Stack.push x s.stack + + let pop s = + s.length <- s.length - 1; + Stack.pop s.stack + + let top s = + Stack.top s.stack + + let clear s = + s.length <- 0; + Stack.clear s.stack + + let copy s = { length = s.length; + stack = Stack.copy s.stack; } + + let is_empty s = + Stack.is_empty s.stack + + let length s = s.length + + let iter f s = + Stack.iter f s.stack + +end + +(************************************************************************) + +let absoluteFilename (fname: string) = + if Filename.is_relative fname then + Filename.concat (Sys.getcwd ()) fname + else + fname + + +(* mapNoCopy is like map but avoid copying the list if the function does not + * change the elements. *) +let rec mapNoCopy (f: 'a -> 'a) = function + [] -> [] + | (i :: resti) as li -> + let i' = f i in + let resti' = mapNoCopy f resti in + if i' != i || resti' != resti then i' :: resti' else li + +let rec mapNoCopyList (f: 'a -> 'a list) = function + [] -> [] + | (i :: resti) as li -> + let il' = f i in + let resti' = mapNoCopyList f resti in + match il' with + [i'] when i' == i && resti' == resti -> li + | _ -> il' @ resti' + + +(* Use a filter function that does not rewrite the list unless necessary *) +let rec filterNoCopy (f: 'a -> bool) (l: 'a list) : 'a list = + match l with + [] -> [] + | h :: rest when not (f h) -> filterNoCopy f rest + | h :: rest -> + let rest' = filterNoCopy f rest in + if rest == rest' then l else h :: rest' + +(** Join a list of strings *) +let rec joinStrings (sep: string) (sl: string list) = + match sl with + [] -> "" + | [s1] -> s1 + | s1 :: ((_ :: _) as rest) -> s1 ^ sep ^ joinStrings sep rest + + +(************************************************************************ + + Configuration + + ************************************************************************) +(** The configuration data can be of several types **) +type configData = + ConfInt of int + | ConfBool of bool + | ConfFloat of float + | ConfString of string + | ConfList of configData list + + +(* Store here window configuration file *) +let configurationData: (string, configData) H.t = H.create 13 + +let clearConfiguration () = H.clear configurationData + +let setConfiguration (key: string) (c: configData) = + H.replace configurationData key c + +let findConfiguration (key: string) : configData = + H.find configurationData key + +let findConfigurationInt (key: string) : int = + match findConfiguration key with + ConfInt i -> i + | _ -> + ignore (E.warn "Configuration %s is not an integer" key); + raise Not_found + +let useConfigurationInt (key: string) (f: int -> unit) = + try f (findConfigurationInt key) + with Not_found -> () + +let findConfigurationString (key: string) : string = + match findConfiguration key with + ConfString s -> s + | _ -> + ignore (E.warn "Configuration %s is not a string" key); + raise Not_found + +let useConfigurationString (key: string) (f: string -> unit) = + try f (findConfigurationString key) + with Not_found -> () + + +let findConfigurationBool (key: string) : bool = + match findConfiguration key with + ConfBool b -> b + | _ -> + ignore (E.warn "Configuration %s is not a boolean" key); + raise Not_found + +let useConfigurationBool (key: string) (f: bool -> unit) = + try f (findConfigurationBool key) + with Not_found -> () + +let findConfigurationList (key: string) : configData list = + match findConfiguration key with + ConfList l -> l + | _ -> + ignore (E.warn "Configuration %s is not a list" key); + raise Not_found + +let useConfigurationList (key: string) (f: configData list -> unit) = + try f (findConfigurationList key) + with Not_found -> () + + +let saveConfiguration (fname: string) = + (** Convert configuration data to a string, for saving externally *) + let configToString (c: configData) : string = + let buff = Buffer.create 80 in + let rec loop (c: configData) : unit = + match c with + ConfInt i -> + Buffer.add_char buff 'i'; + Buffer.add_string buff (string_of_int i); + Buffer.add_char buff ';' + + | ConfBool b -> + Buffer.add_char buff 'b'; + Buffer.add_string buff (string_of_bool b); + Buffer.add_char buff ';' + + | ConfFloat f -> + Buffer.add_char buff 'f'; + Buffer.add_string buff (string_of_float f); + Buffer.add_char buff ';' + + | ConfString s -> + if String.contains s '"' then + E.s (E.unimp "Guilib: configuration string contains quotes"); + Buffer.add_char buff '"'; + Buffer.add_string buff s; + Buffer.add_char buff '"'; (* '"' *) + + | ConfList l -> + Buffer.add_char buff '['; + List.iter loop l; + Buffer.add_char buff ']' + in + loop c; + Buffer.contents buff + in + try + let oc = open_out fname in + ignore (E.log "Saving configuration to %s\n" (absoluteFilename fname)); + H.iter (fun k c -> + output_string oc (k ^ "\n"); + output_string oc ((configToString c) ^ "\n")) + configurationData; + close_out oc + with _ -> + ignore (E.warn "Cannot open configuration file %s\n" fname) + + +(** Make some regular expressions early *) +let intRegexp = Str.regexp "i\\([0-9]+\\);" +let floatRegexp = Str.regexp "f\\([0-9]+\\.[0-9]+\\);" +let boolRegexp = Str.regexp "b\\(\\(true\\)\\|\\(false\\)\\);" +let stringRegexp = Str.regexp "\"\\([^\"]*\\)\"" + +let loadConfiguration (fname: string) : unit = + H.clear configurationData; + + let stringToConfig (s: string) : configData = + let idx = ref 0 in (** the current index *) + let l = String.length s in + + let rec getOne () : configData = + if !idx >= l then raise Not_found; + + if Str.string_match intRegexp s !idx then begin + idx := Str.match_end (); + ConfInt (int_of_string (Str.matched_group 1 s)) + end else if Str.string_match floatRegexp s !idx then begin + idx := Str.match_end (); + ConfFloat (float_of_string (Str.matched_group 1 s)) + end else if Str.string_match boolRegexp s !idx then begin + idx := Str.match_end (); + ConfBool (bool_of_string (Str.matched_group 1 s)) + end else if Str.string_match stringRegexp s !idx then begin + idx := Str.match_end (); + ConfString (Str.matched_group 1 s) + end else if String.get s !idx = '[' then begin + (* We are starting a list *) + incr idx; + let rec loop (acc: configData list) : configData list = + if !idx >= l then begin + ignore (E.warn "Non-terminated list in configuration %s" s); + raise Not_found + end; + if String.get s !idx = ']' then begin + incr idx; + List.rev acc + end else + loop (getOne () :: acc) + in + ConfList (loop []) + end else begin + ignore (E.warn "Bad configuration element in a list: %s\n" + (String.sub s !idx (l - !idx))); + raise Not_found + end + in + getOne () + in + (try + let ic = open_in fname in + ignore (E.log "Loading configuration from %s\n" (absoluteFilename fname)); + (try + while true do + let k = input_line ic in + let s = input_line ic in + try + let c = stringToConfig s in + setConfiguration k c + with Not_found -> () + done + with End_of_file -> ()); + close_in ic; + with _ -> () (* no file, ignore *)); + + () + + + +(*********************************************************************) +type symbol = int + +(**{ Registering symbol names} *) +let registeredSymbolNames: (string, symbol) H.t = H.create 113 +let symbolNames: string IH.t = IH.create 113 +let nextSymbolId = ref 0 + +(* When we register symbol ranges, we store a naming function for use later + * when we print the symbol *) +let symbolRangeNaming: (int * int * (int -> string)) list ref = ref [] + +(* Reset the symbols. We want to allow the registration of symbols at the + * top-level. This means that we cannot simply clear the hash tables. The + * first time we call "reset" we actually remember the state. *) +let resetThunk: (unit -> unit) option ref = ref None + +let snapshotSymbols () : unit -> unit = + runThunks [ restoreIntHash symbolNames; + restoreRef nextSymbolId; + restoreHash registeredSymbolNames; + restoreRef symbolRangeNaming ] + +let resetSymbols () = + match !resetThunk with + None -> resetThunk := Some (snapshotSymbols ()) + | Some t -> t () + + +let dumpSymbols () = + ignore (E.log "Current symbols\n"); + IH.iter (fun i k -> ignore (E.log " %s -> %d\n" k i)) symbolNames; + () + +let newSymbol (n: string) : symbol = + assert(not (H.mem registeredSymbolNames n)); + let id = !nextSymbolId in + incr nextSymbolId; + H.add registeredSymbolNames n id; + IH.add symbolNames id n; + id + +let registerSymbolName (n: string) : symbol = + try H.find registeredSymbolNames n + with Not_found -> begin + newSymbol n + end + +(** Register a range of symbols. The mkname function will be invoked for + * indices starting at 0 *) +let registerSymbolRange (count: int) (mkname: int -> string) : symbol = + if count < 0 then E.s (E.bug "registerSymbolRange: invalid counter"); + let first = !nextSymbolId in + nextSymbolId := !nextSymbolId + count; + symbolRangeNaming := + (first, !nextSymbolId - 1, mkname) :: !symbolRangeNaming; + first + +let symbolName (id: symbol) : string = + try IH.find symbolNames id + with Not_found -> + (* Perhaps it is one of the lazily named symbols *) + try + let (fst, _, mkname) = + List.find + (fun (fst,lst,_) -> fst <= id && id <= lst) + !symbolRangeNaming in + let n = mkname (id - fst) in + IH.add symbolNames id n; + n + with Not_found -> + ignore (E.warn "Cannot find the name of symbol %d" id); + "symbol" ^ string_of_int id + +(************************************************************************) + +(** {1 Int32 Operators} *) + +module Int32Op = struct + exception IntegerTooLarge + let to_int (i: int32) = + let i' = Int32.to_int i in (* Silently drop the 32nd bit *) + if i = Int32.of_int i' then i' + else raise IntegerTooLarge + + let (<%) = (fun x y -> (Int32.compare x y) < 0) + let (<=%) = (fun x y -> (Int32.compare x y) <= 0) + let (>%) = (fun x y -> (Int32.compare x y) > 0) + let (>=%) = (fun x y -> (Int32.compare x y) >= 0) + let (<>%) = (fun x y -> (Int32.compare x y) <> 0) + + let (+%) = Int32.add + let (-%) = Int32.sub + let ( *% ) = Int32.mul + let (/%) = Int32.div + let (~-%) = Int32.neg + + (* We cannot use the <<% because it trips camlp4 *) + let sll = fun i j -> Int32.shift_left i (to_int j) + let (>>%) = fun i j -> Int32.shift_right i (to_int j) + let (>>>%) = fun i j -> Int32.shift_right_logical i (to_int j) +end + + +(*********************************************************************) + +let equals x1 x2 : bool = + (compare x1 x2) = 0 diff --git a/cil/ocamlutil/util.mli b/cil/ocamlutil/util.mli new file mode 100644 index 00000000..d701c65f --- /dev/null +++ b/cil/ocamlutil/util.mli @@ -0,0 +1,311 @@ +(** A bunch of generally useful functions *) + +exception GotSignal of int + +val withTimeout : float -> (* Seconds for timeout *) + (int -> 'b) -> (* What to do if we have a timeout. The + * argument passed is the signal number + * received. *) + ('a -> 'b) -> (* The function to run *) + 'a -> (* And its argument *) + 'b + +val docHash : ?sep:Pretty.doc -> ('a -> 'b -> Pretty.doc) -> unit -> + (('a, 'b) Hashtbl.t) -> Pretty.doc + + +val hash_to_list: ('a, 'b) Hashtbl.t -> ('a * 'b) list + +val keys: ('a, 'b) Hashtbl.t -> 'a list + + +(** Copy a hash table into another *) +val hash_copy_into: ('a, 'b) Hashtbl.t -> ('a, 'b) Hashtbl.t -> unit + +(** First, a few utility functions I wish were in the standard prelude *) + +val anticompare: 'a -> 'a -> int + +val list_drop : int -> 'a list -> 'a list +val list_droptail : int -> 'a list -> 'a list +val list_span: ('a -> bool) -> ('a list) -> 'a list * 'a list +val list_insert_by: ('a -> 'a -> int) -> 'a -> 'a list -> 'a list +val list_head_default: 'a -> 'a list -> 'a +val list_iter3 : ('a -> 'b -> 'c -> unit) -> + 'a list -> 'b list -> 'c list -> unit +val get_some_option_list : 'a option list -> 'a list +val list_append: ('a list) -> ('a list) -> ('a list) (* tail-recursive append*) + +(** Iterate over a list passing the index as you go *) +val list_iteri: (int -> 'a -> unit) -> 'a list -> unit +val list_mapi: (int -> 'a -> 'b) -> 'a list -> 'b list + +(** Like fold_left but pass the index into the list as well *) +val list_fold_lefti: ('acc -> int -> 'a -> 'acc) -> 'acc -> 'a list -> 'acc + +(** Generates the range of integers starting with a and ending with b *) +val int_range_list : int -> int -> int list + +(* Create a list of length l *) +val list_init : int -> (int -> 'a) -> 'a list + +(** Find the first element in a list that returns Some *) +val list_find_first: 'a list -> ('a -> 'b option) -> 'b option + +(** mapNoCopy is like map but avoid copying the list if the function does not + * change the elements *) + +val mapNoCopy: ('a -> 'a) -> 'a list -> 'a list + +val mapNoCopyList: ('a -> 'a list) -> 'a list -> 'a list + +val filterNoCopy: ('a -> bool) -> 'a list -> 'a list + + +(** Join a list of strings *) +val joinStrings: string -> string list -> string + + +(**** Now in growArray.mli + +(** Growable arrays *) +type 'a growArrayFill = + Elem of 'a + | Susp of (int -> 'a) + +type 'a growArray = { + gaFill: 'a growArrayFill; + (** Stuff to use to fill in the array as it grows *) + + mutable gaMaxInitIndex: int; + (** Maximum index that was written to. -1 if no writes have + * been made. *) + + mutable gaData: 'a array; + } + +val newGrowArray: int -> 'a growArrayFill -> 'a growArray +(** [newGrowArray initsz fillhow] *) + +val getReg: 'a growArray -> int -> 'a +val setReg: 'a growArray -> int -> 'a -> unit +val copyGrowArray: 'a growArray -> 'a growArray +val deepCopyGrowArray: 'a growArray -> ('a -> 'a) -> 'a growArray + + +val growArray_iteri: (int -> 'a -> unit) -> 'a growArray -> unit +(** Iterate over the initialized elements of the array *) + +val growArray_foldl: ('acc -> 'a -> 'acc) -> 'acc ->'a growArray -> 'acc +(** Fold left over the initialized elements of the array *) + +****) + +(** hasPrefix prefix str returns true with str starts with prefix *) +val hasPrefix: string -> string -> bool + + +(** Given a ref cell, produce a thunk that later restores it to its current value *) +val restoreRef: ?deepCopy:('a -> 'a) -> 'a ref -> unit -> unit + +(** Given a hash table, produce a thunk that later restores it to its current value *) +val restoreHash: ?deepCopy:('b -> 'b) -> ('a, 'b) Hashtbl.t -> unit -> unit + +(** Given an integer hash table, produce a thunk that later restores it to + * its current value *) +val restoreIntHash: ?deepCopy:('b -> 'b) -> 'b Inthash.t -> unit -> unit + +(** Given an array, produce a thunk that later restores it to its current value *) +val restoreArray: ?deepCopy:('a -> 'a) -> 'a array -> unit -> unit + + +(** Given a list of thunks, produce a thunk that runs them all *) +val runThunks: (unit -> unit) list -> unit -> unit + + +val memoize: ('a, 'b) Hashtbl.t -> + 'a -> + ('a -> 'b) -> 'b + +(** Just another name for memoize *) +val findOrAdd: ('a, 'b) Hashtbl.t -> + 'a -> + ('a -> 'b) -> 'b + +val tryFinally: + ('a -> 'b) -> (* The function to run *) + ('b option -> unit) -> (* Something to run at the end. The None case is + * used when an exception is thrown *) + 'a -> 'b + + + + +(** Get the value of an option. Raises Failure if None *) +val valOf : 'a option -> 'a + +(** + * An accumulating for loop. + * + * Initialize the accumulator with init. The current index and accumulator + * from the previous iteration is passed to f. + *) +val fold_for : init:'a -> lo:int -> hi:int -> (int -> 'a -> 'a) -> 'a + +(************************************************************************) + +module type STACK = sig + type 'a t + (** The type of stacks containing elements of type ['a]. *) + + exception Empty + (** Raised when {!Util.Stack.pop} or {!Util.Stack.top} is applied to an + * empty stack. *) + + val create : unit -> 'a t + + + val push : 'a -> 'a t -> unit + (** [push x s] adds the element [x] at the top of stack [s]. *) + + val pop : 'a t -> 'a + (** [pop s] removes and returns the topmost element in stack [s], + or raises [Empty] if the stack is empty. *) + + val top : 'a t -> 'a + (** [top s] returns the topmost element in stack [s], + or raises [Empty] if the stack is empty. *) + + val clear : 'a t -> unit + (** Discard all elements from a stack. *) + + val copy : 'a t -> 'a t + (** Return a copy of the given stack. *) + + val is_empty : 'a t -> bool + (** Return [true] if the given stack is empty, [false] otherwise. *) + + val length : 'a t -> int + (** Return the number of elements in a stack. *) + + val iter : ('a -> unit) -> 'a t -> unit + (** [iter f s] applies [f] in turn to all elements of [s], + from the element at the top of the stack to the element at the + bottom of the stack. The stack itself is unchanged. *) +end + +module Stack : STACK + +(************************************************************************ + Configuration +************************************************************************) +(** The configuration data can be of several types **) +type configData = + ConfInt of int + | ConfBool of bool + | ConfFloat of float + | ConfString of string + | ConfList of configData list + + +(** Load the configuration from a file *) +val loadConfiguration: string -> unit + +(** Save the configuration in a file. Overwrites the previous values *) +val saveConfiguration: string -> unit + + +(** Clear all configuration data *) +val clearConfiguration: unit -> unit + +(** Set a configuration element, with a key. Overwrites the previous values *) +val setConfiguration: string -> configData -> unit + +(** Find a configuration elements, given a key. Raises Not_found if it canont + * find it *) +val findConfiguration: string -> configData + +(** Like findConfiguration but extracts the integer *) +val findConfigurationInt: string -> int + +(** Looks for an integer configuration element, and if it is found, it uses + * the given function. Otherwise, does nothing *) +val useConfigurationInt: string -> (int -> unit) -> unit + + +val findConfigurationBool: string -> bool +val useConfigurationBool: string -> (bool -> unit) -> unit + +val findConfigurationString: string -> string +val useConfigurationString: string -> (string -> unit) -> unit + +val findConfigurationList: string -> configData list +val useConfigurationList: string -> (configData list -> unit) -> unit + + +(************************************************************************) + +(** Symbols are integers that are uniquely associated with names *) +type symbol = int + +(** Get the name of a symbol *) +val symbolName: symbol -> string + +(** Register a symbol name and get the symbol for it *) +val registerSymbolName: string -> symbol + +(** Register a number of consecutive symbol ids. The naming function will be + * invoked with indices from 0 to the counter - 1. Returns the id of the + * first symbol created. The naming function is invoked lazily, only when the + * name of the symbol is required. *) +val registerSymbolRange: int -> (int -> string) -> symbol + + +(** Make a fresh symbol. Give the name also, which ought to be distinct from + * existing symbols. This is different from registerSymbolName in that it + * always creates a new symbol. *) +val newSymbol: string -> symbol + +(** Reset the state of the symbols to the program startup state *) +val resetSymbols: unit -> unit + +(** Take a snapshot of the symbol state. Returns a thunk that restores the + * state. *) +val snapshotSymbols: unit -> unit -> unit + + +(** Dump the list of registered symbols *) +val dumpSymbols: unit -> unit + +(************************************************************************) + +(** {1 Int32 Operators} *) + +module Int32Op : sig + val (<%) : int32 -> int32 -> bool + val (<=%) : int32 -> int32 -> bool + val (>%) : int32 -> int32 -> bool + val (>=%) : int32 -> int32 -> bool + val (<>%) : int32 -> int32 -> bool + + val (+%) : int32 -> int32 -> int32 + val (-%) : int32 -> int32 -> int32 + val ( *% ) : int32 -> int32 -> int32 + val (/%) : int32 -> int32 -> int32 + val (~-%) : int32 -> int32 + + val sll : int32 -> int32 -> int32 + val (>>%) : int32 -> int32 -> int32 + val (>>>%) : int32 -> int32 -> int32 + + exception IntegerTooLarge + val to_int : int32 -> int +end + +(************************************************************************) + +(** This has the semantics of (=) on OCaml 3.07 and earlier. It can + handle cyclic values as long as a structure in the cycle has a unique + name or id in some field that occurs before any fields that have cyclic + pointers. *) +val equals: 'a -> 'a -> bool -- cgit