Tools

Chapter 4 Tools

4.1 The interactive toplevel (`flowcaml`)

The toplevel tool for Flow Caml, flowcaml, permits interactive use of the Flow Caml system through a read--type-check loop. In this mode, the system repeatedly reads Flow Caml phrases from the input, type-checks them and outputs the inferred type, if any. The system prints a # (sharp) prompt before reading each phrase.

Input to the toplevel can span several lines. It is terminated by ;; (a double-semicolon). The toplevel input has the following syntax.

toplevel-input	::=	<toplevel-phrase> `;;`
	\|	flows-declaration `;;`
	\|	`#` ident [directive-argument];;
toplevel-phrase	::=	definition
	\|	expr
directive-argument	::=	string-literal \| integer-literal \| value-path \| level \| typeconstr \| exception

A toplevel input can consists in a series of definition, similar to those found in implementations of compilation units or in struct ...end module expressions. It can also consist in a flow declaration, which extend the current security policy, or in a toplevel directive, starting with # (the sharp sign). These directives control the behavior of the toplevel; they are listed below in section 4.1.3.

4.1.1 Graphical output

The toplevel offers a graphical output of inferred type schemes. It is enabled by the -graph command line option or the directive #open_graph. For a description of the graphical output of type schemes, see section 2.2.6 of the tutorial.

4.1.2 Options

The following command-line options are recognized by the flowcaml command.

-display

host:display
Specify the host and screen to be used for displaying the graphic window (see the option -graph). By default this is obtained from the environment variable DISPLAY.

-font

fontname
Set the font used on the graphical window.

-geometry

widthxheight+x-offset+y-offset
Specify the initial geometry of the graphical window. The four parameters are numbers giving (in pixels) the width, height, horizontal offset and vertical offset respectively. Partial specifications of the form widthxheight or +x-offset+y-offset are also allowed.

-graph

Enable the graphic window. The toplevel may produce a graphical representation of inferred type schemes (in addition to the textual standard one), displayed a X graphical window. The display and geometry of this window may be controlled by the options -display and -geometry.

-I

directory
Add the given directory to the list of directories searched for source and compiled files. By default, the current directory is searched first, the standard library directory. Directories added with -I are searched after the current directory, in the order in which they were given on the command line, but before the standard library directory.

-linewidth

width
Sets the number of columns of the terminal used for printing messages. Default is 78.

-nopervasives

Does not initially open then Pervasives module.

-pprint

flags
Configure the pretty-print of types. The argument is a string of one or several characters, with the following meaning for each character:

	`C/c`	enable/disable use of colors for displaying polarities of type variables (on VT100 compatible terminals).
	`0/1/2`	Set which universally quantified and unconstrained type variables are hidden. In mode `0`, all are hidden or replaced by `_`, in mode `1`, only those which appear on functions arrows are hidden, in mode `2`, all are displayed.
	`H/h`	enable/disable the hiding of universally quantified and unconstrained type variables (`h` implies `g`).
	`V/v`	enable/disable printing of the polarities of type variables (with the symbols `+`, `-` and `=`)

Default is Cv1.

4.1.3 Toplevel directives

The following directives control the toplevel behavior.

#close_graph: Close the graphical window (see section 4.1.1).
#lookup_exception: "ident"
Lookup for an exception in the environment and print its declaration.
#lookup_level: "ident"
Lookup for a level in the environment and print its declaration.
#lookup_type: "ident"
Lookup for a type in the environment and print its declaration.
#lookup_value: "ident"
Lookup for a value in the environment and print its description.
#open_graph: Open the graphical window (see section 4.1.1).
#pprint: "flags"
Set flags for pretty-print (see option -pprint above for a description of available flags).
#reset_context: Reset the security level associated to the toplevel evaluation context to its initial value, as if a new program were started.
#quit: Exit the toplevel loop and terminate the flowcaml command.

4.2 The batch compiler (`flowcamlc`)

This section is interested with the Flow Caml batch compiler flowcamlc. To describe in a few words its working, let us say that it reads Flow Caml files as input, type-checks their content and produces regular Objective Caml code as output. These may be later compiled using the standard ocamlc or ocamlopt compilers to obtain executables.

4.2.1 Overview

The flowcamlc command has a command-line interface similar to that of the Objective Caml compilers. It accepts several types of arguments:

Arguments ending in .fmli are taken to be source files for compilation unit interfaces. From the file x.fmli, the flowcamlc compiler produces a compiled interface in the file x.fcmi and an Objective Caml compilation unit interface in the file x.mli.
Arguments ending in .fml are taken to be source files for compilation unit implementations. From the file x.fml, the flowcamlc compiler produces a Objective Caml compilation unit implementation in the file x.ml.

If the interface file x.fmli exists, the implementation x.fml is checked against the corresponding compiled interface x.fcmi, which is assumed to exist. If no interface x.fmli is provided, the compilation of x.ml produces a compiled interface file x.fcmi in addition to x.ml. The file x.fcmi produced corresponds to an interface that exports everything that is defined in the implementation x.fml.

4.2.2 Options

The following command-line options are recognized by the flowcamlc command:

-dump: Produce dumped abstract syntax tree for Objective Caml as output, instead of literal source code file. These dumped tree can be used as input for the Objective Caml compiler, which won't need to parse again the source code. However, the format of the abstract syntax tree depends on the version of the Objective Caml compiler, so it may be not compatible with yours.
-i: Cause the compiler to print the inferred interface when compiling an implementation (.fml file). This can be useful to check the types inferred by the compiler. Also, since the output follows the syntax of interface files, it can help in writing an explicit interface (.fmli file) for a file: just redirect the standard output of the compiler to a .fmli file, and edit that file to remove all declarations of unexported names.
-I: directory
Add the given directory to the list of directories searched for source and compiled files. By default, the current directory is searched first, the the standard library directory. Directories added with -I are searched after the current directory, in the order in which they were given on the command line, but before the standard library directory.
-nostdlib: Do not add the standard library directory in the default search path.
-pprint: flags
Configure the pretty-print of types. See the documentation of the command flowcaml for a description of available flags.
-runlib: Print the location of the run-time library and exit.
-stdlib: Print the location of the standard library and exit.
-v: Print the compiler version and location of libraries and exit.
-version: Print the compiler version and exit.
-nopervasives: Does not initially open the Pervasives module.

4.3 The security policy displayer (`flowcamlpol`)

4.3.1 Overview

The flowcamlpol tool aims at verifying that a series of compilation units can be linked together in order to produce a secure program. It moreover computes the minimal security policy under which the program can be safely run (which is the ``union'' of the security policies declared in the compilation units).

The flowcamlpol command takes as argument the list of the compiled interface files of the units which form the program, in the order they should be passed to the linker. For instance, for a program made of the compilation units unit₁, unit₂, ..., unit_n, which is linked with the command ocamlc unit₁.cmo unit₂.cmo ... unit_n.cmo, one have to run:

flowcamlpol unit₁.fcmi unit₂.fcmi ... unit_n.fcmi

This outputs the smallest set of assumptions between principals under which the whole program is type safe, i.e. the smallest security policy which allow its execution. (The tool can give a graphical representation of this set of inequalities with the -graph option.) flowcamlpol also checks that the bounds of the compilation units fit together, i.e. that for every i, the lower bound of unit_i is greater than or equal to the upper bounds of unit$_1$, ..., unit_i-1, in the printed security policy.

A concrete example of use of flowcamlpol is given in sections 2.8.2 and 2.8.3 of the tutorial.

4.3.2 Options

The following command-line options are recognized by the flowcamlpol command.

-display: host:display
Specifies the host and screen to be used for displaying the graphic window (see the option -graph). By default this is obtained from the environment variable DISPLAY.
-font: fontname
Sets the font used on the graphical window.
-geometry: widthxheight+x-offset+y-offset
Specify the initial geometry of the graphical window. The four parameters are numbers giving (in pixels) the width, height, horizontal offset and vertical offset respectively. Partial specifications of the form widthxheight or +x-offset+y-offset are also allowed.
-graph: Gives a graphical representation of the security lattice. The display and geometry of this windows may be controlled by the options -display and -geometry.
-linewidth: width
Sets the number of columns of the terminal used for printing messages. Default is 78.

4.4 The dependency generator (`flowcamldep`)

The flowcamldep command scans a set of Flow Caml source files (.fml and .fmli files) for references to external compilation units, and outputs dependency lines in a format suitable for the make utility. This ensures that make will compile the source file in the correct order, and recompile those files that need to when a source file is modified.

The typical usage is

       flowcamldep *.fmli *.fml > Depend.flowcaml

where *.fmli *.fml expands to all source files in the current directory and Depend.flowcaml is the file that should contain the dependencies. (See below for a typical Makefile.)

Let us note that flowcamldep generates only the dependencies needed to the Flow Caml compiler, that is those relating .fmli and .fml files to .mli and .ml. To compile the files generated by Flow Caml with one of the Objective Caml compilers, you will need to run ocamldep on the intermediate files .mli and .mli.

4.4.1 Options

The following command-line options are recognized by flowcamldep:

-I: directory
Add the given directory to the list of directories searched for source files. If a source file foo.fml mentions an external compilation unit Bar, a dependency on that unit's interface bar.mli is generated only if the source for bar is found in the current directory or in one of the directories specified with -I. Otherwise, Bar is assumed to be a module from the standard library, and no dependencies are generated.

4.4.2 A typical Makefile

Here is a template Makefile for a Flow Caml program.

# Compilers
OCAMLC=ocamlc -I +flowcamlrun
OCAMLOPT=ocamlopt -I +flowcamlrun
FLOWCAMLC=flowcamlc

OCAMLDEP=ocamldep
FLOWCAMLDEP=flowcamldep

# The list of object files for the program
OBJECTS=mod1.cmo mod2.cmo mod3.cmo

# To check the security policy
pol: $(OBJECTS.cmo=.fcmi)
        flowcamlpol $^

# To build the program
prog: $(OBJECTS)
        $(OCAMLC) -o $@ flowcamlrun.cma $(OBJECTS)

# Common rules
.SUFFIXES: .ml .mli .fml .fmli .cmi .cmo .cmx .fcmi 

.ml.cmo:
        $(OCAMLC) -c $<

.mli.cmi:
        $(OCAMLC) -c $<

.ml.cmx:
        $(OCAMLOPT) -c $<

.fmli.mli:
        $(FLOWCAMLC) -c $<

.fml.ml:
        $(FLOWCAMLC) -c $<

# Clean up
        rm -f prog
        rm -f *.cm[iox] *.fcmi
        for i in *.mli; do \
        if test -f `basename $$i .mli`.fmli; then rm -f $$i; fi \
        done
        for i in *.ml; do \
        if test -f `basename $$i .ml`.fml; then rm -f $$i; fi \
        done

# Dependencies
depend-flowcaml:
        $(FLOWCAMLDEP) *.fml *.fmli > Depend.flowcaml

depend-ocaml:
        $(OCAMLDEP) *.ml *.mli > Depend.ocaml

# Dependencies
depend-flowcaml:
        $(FLOWCAMLDEP) *.fml *.fmli > Depend.flowcaml

depend-ocaml: $(patsubst %.fml,%.ml,$(wildcard *.fml))\
              $(patsubst %.fml,%.ml,$(wildcard *.fml))
        $(OCAMLDEP) *.ml *.mli > Depend.ocaml

include Depend.flowcaml
include Depend.ocaml