From 93d89c2b5e8497365be152fb53cb6cd4c5764d34 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 3 Mar 2010 10:25:25 +0000 Subject: Getting rid of CIL git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1270 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 deletions(-) delete mode 100644 cil/ocamlutil/Makefile.ocaml delete mode 100644 cil/ocamlutil/Makefile.ocaml.build delete mode 100755 cil/ocamlutil/alpha.ml delete mode 100755 cil/ocamlutil/alpha.mli delete mode 100644 cil/ocamlutil/clist.ml delete mode 100644 cil/ocamlutil/clist.mli delete mode 100644 cil/ocamlutil/errormsg.ml delete mode 100644 cil/ocamlutil/errormsg.mli delete mode 100644 cil/ocamlutil/growArray.ml delete mode 100644 cil/ocamlutil/growArray.mli delete mode 100755 cil/ocamlutil/inthash.ml delete mode 100755 cil/ocamlutil/inthash.mli delete mode 100755 cil/ocamlutil/intmap.ml delete mode 100755 cil/ocamlutil/intmap.mli delete mode 100755 cil/ocamlutil/perfcount.c.in delete mode 100644 cil/ocamlutil/pretty.ml delete mode 100644 cil/ocamlutil/pretty.mli delete mode 100644 cil/ocamlutil/stats.ml delete mode 100644 cil/ocamlutil/stats.mli delete mode 100644 cil/ocamlutil/trace.ml delete mode 100644 cil/ocamlutil/trace.mli delete mode 100755 cil/ocamlutil/util.ml delete mode 100644 cil/ocamlutil/util.mli (limited to 'cil/ocamlutil') diff --git a/cil/ocamlutil/Makefile.ocaml b/cil/ocamlutil/Makefile.ocaml deleted file mode 100644 index 36ac21a5..00000000 --- a/cil/ocamlutil/Makefile.ocaml +++ /dev/null @@ -1,395 +0,0 @@ -# -*- 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 - LINKFLAGS += -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 deleted file mode 100644 index 5271e461..00000000 --- a/cil/ocamlutil/Makefile.ocaml.build +++ /dev/null @@ -1,50 +0,0 @@ -# -*- 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 deleted file mode 100755 index 6a1ea017..00000000 --- a/cil/ocamlutil/alpha.ml +++ /dev/null @@ -1,156 +0,0 @@ -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 deleted file mode 100755 index e1e430dc..00000000 --- a/cil/ocamlutil/alpha.mli +++ /dev/null @@ -1,50 +0,0 @@ -(** {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 deleted file mode 100644 index 80f0fd64..00000000 --- a/cil/ocamlutil/clist.ml +++ /dev/null @@ -1,183 +0,0 @@ -(* - * - * 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 deleted file mode 100644 index c0378a60..00000000 --- a/cil/ocamlutil/clist.mli +++ /dev/null @@ -1,97 +0,0 @@ -(* - * - * 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 deleted file mode 100644 index 07e935d4..00000000 --- a/cil/ocamlutil/errormsg.ml +++ /dev/null @@ -1,337 +0,0 @@ -(* - * - * 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 deleted file mode 100644 index 8d9c6979..00000000 --- a/cil/ocamlutil/errormsg.mli +++ /dev/null @@ -1,164 +0,0 @@ -(* - * - * 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 deleted file mode 100644 index ccadc762..00000000 --- a/cil/ocamlutil/growArray.ml +++ /dev/null @@ -1,191 +0,0 @@ -(** 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 deleted file mode 100644 index 4cb5f48f..00000000 --- a/cil/ocamlutil/growArray.mli +++ /dev/null @@ -1,131 +0,0 @@ -(***********************************************************************) -(* 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 deleted file mode 100755 index b1ad0c07..00000000 --- a/cil/ocamlutil/inthash.ml +++ /dev/null @@ -1,188 +0,0 @@ -(** 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 deleted file mode 100755 index f62fcd2b..00000000 --- a/cil/ocamlutil/inthash.mli +++ /dev/null @@ -1,27 +0,0 @@ -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 deleted file mode 100755 index 00242bc1..00000000 --- a/cil/ocamlutil/intmap.ml +++ /dev/null @@ -1,171 +0,0 @@ -(***********************************************************************) -(* *) -(* 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 deleted file mode 100755 index eef89b55..00000000 --- a/cil/ocamlutil/intmap.mli +++ /dev/null @@ -1,87 +0,0 @@ -(***********************************************************************) -(* *) -(* 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 deleted file mode 100755 index ae532f69..00000000 --- a/cil/ocamlutil/perfcount.c.in +++ /dev/null @@ -1,184 +0,0 @@ -// -*- 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 deleted file mode 100644 index 47d07ac4..00000000 --- a/cil/ocamlutil/pretty.ml +++ /dev/null @@ -1,859 +0,0 @@ -(* - * - * 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 deleted file mode 100644 index 5422432d..00000000 --- a/cil/ocamlutil/pretty.mli +++ /dev/null @@ -1,316 +0,0 @@ -(* - * - * 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 deleted file mode 100644 index 8bbb7d05..00000000 --- a/cil/ocamlutil/stats.ml +++ /dev/null @@ -1,146 +0,0 @@ -(* 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 deleted file mode 100644 index 9ed98e56..00000000 --- a/cil/ocamlutil/stats.mli +++ /dev/null @@ -1,72 +0,0 @@ -(* - * - * 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 deleted file mode 100644 index b4292865..00000000 --- a/cil/ocamlutil/trace.ml +++ /dev/null @@ -1,169 +0,0 @@ -(* - * - * 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 deleted file mode 100644 index 46ca6523..00000000 --- a/cil/ocamlutil/trace.mli +++ /dev/null @@ -1,106 +0,0 @@ -(* - * - * 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 deleted file mode 100755 index e6c2c679..00000000 --- a/cil/ocamlutil/util.ml +++ /dev/null @@ -1,815 +0,0 @@ -(** 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 deleted file mode 100644 index d701c65f..00000000 --- a/cil/ocamlutil/util.mli +++ /dev/null @@ -1,311 +0,0 @@ -(** 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