SAW REPL Reference

The primary mechanism for interacting with SAW is through the saw executable included as part of the standard binary distribution. With no arguments, saw starts a read-evaluate-print loop (REPL) that allows the user to interactively evaluate commands in the SAWScript language.

REPL Commands

There are a number of REPL-specific commands that can be accessed by typing a colon and the command name, and perhaps some arguments.

• :? prints the list of :-commands with brief descriptions. If given an argument, it instead looks up a SAWScript builtin and prints its type and help text.

• :cd changes the REPL’s current directory.

• :env displays the values and types of all currently bound variables, including built-in functions and commands.

• :help or :h is the same as :?.

• :llvmdis disassembles an LLVM module. See separate subsection below.

• :pwd prints the REPL’s current directory.

• :quit or :q exits the REPL. (If the REPL was started as a subshell, it only exits that subshell, not the whole of SAW.)

• :search with one or more types (complex types go in parentheses) prints matching currently bound variables. See separate subsection below.

• :tenv displays the values and types of all currently bound types and type aliases, including many (but currently not all) built-in types.

• :type or :t checks and prints the type of an arbitrary SAWScript expression:

  sawscript> :t show
  {a.0} a.0 -> String
  

Using :search

The REPL :search command takes one or more type patterns as arguments, and searches the current value namespace (including functions and builtins) for objects that mention types matching all the patterns given. In practice this is mostly useful for searching for builtins.

Type patterns are type names extended with _ as a wildcard. Thus for example [_] matches any list type. You may also forall-bind type variables before the patterns using the {a} syntax. The scope of such bindings is the whole search.

Complex patterns should be written in parentheses; otherwise they become syntactically ambiguous. Note in particular that parentheses are required to treat a type constructor application to another type as a single search term. Without parentheses, :search would treat the unapplied type constructor and the other type as two separate search terms. For instance, :search ProofScript Int will search for objects mentioning both ProofScript (applied to anything) and Int. To search for objects that mention the type ProofScript Int, write :search (ProofScript Int).

Type variables in the search patterns are matched as follows:

• Already-bound type variables (typedef names, certain builtin types) must match exactly.

• Free type variables match any type, but all occurrences must match the same type. Thus for example [a] -> a matches sum : [Int] -> Int and head : {t} [t] -> t but not length : {t} [t] -> Int.

  This is true across all patterns in the same search; searching for [a], [b], and a -> b will match map : {a, b} (a -> b) -> [a] -> [b], as well as pam : {a, b} [a] -> (a -> b) -> [b] if you define such a thing. But it won’t match mapFirst : {a, b, c} (a -> b) [(a, c)] -> [(b, c)].

  Perhaps unfortunately, it will match intNth : [Int] -> Int -> Int. The search logic does not require distinct patterns to match distinct parts of the target type, nor is there a way to prevent it from picking the same substitution for both a and b. (Neither of these behaviors is entirely desirable and might be improved in the future.)

• Forall-bound type variables in the pattern are matched in the same way as free type variables, but will only match forall-bound type variables in the search space. Thus, :search {a} (a -> a) will match id : {a} a -> a but not inc: Int -> Int, while :search (a -> a) will match both. This is helpful to search specifically for polymorphic functions.

Because SAWScript functions are curried, searching for Int -> Int will match String -> Int -> Int. However, it will not match Int -> String -> Int. The best way to search for a function that takes Int in any argument position and also returns Int is by searching for both Int -> _ and _ -> Int: :search (Int -> _) (_ -> Int).

There is, however, no good way yet to search for a function that takes two Ints in arbitrary argument positions. Searching for Int -> Int -> _ will only find functions where the two arguments are adjacent, Int -> _ -> Int -> _ will only find functions where one other argument is between them, and searching for Int -> _ twice falls afoul of the limitation where two patterns can match the same thing.

Using :llvmdis

:llvmdis disassembles LLVM bitcode or prints other metadata from an LLVMModule. The first argument is the name of a SAWScript-level LLVMModule that has been loaded.

The second argument selects an object to disassemble. If it is a ! followed by a number N, the _N_th unnamed metadata reference is extracted and printed. If it contains a :, it is treated as a filename and line number and the code or data structure associated with that location is extracted and printed. Otherwise it is treated as a function name to disassemble.

The output is comparable to LLVM’s llvm-dis tool but is based on SAW’s internal representation and knowledge of the LLVM module.

Examples:

sawscript> bc <- llvm_load_module "intTests/testmulti/foo.bc"
sawscript> :llvmdis bc foo.c:2
  ... shows just line 2 of foo.c in LLVM textual format
sawscript> :llvmdis bc !10
  ... shows the metadata at index 10
sawscript> :llvmdis bc foo
  ... shows the foo function in LLVM textual format