Usage

How to use rif:

Installation

The project should run if you simply clone the repository and use dune to build it.

git clone https://github.com/UQ-PAC/rif.git
cd rif
dune install

If you're on linux, the symlink rif.exe should point to the location where dune compiles the executable to. If not, you can also use dune exec rif -- <args> instead of ./rif.exe <args> to run the program.

Usage

rif takes several arguments:

$ ./rif.exe --help
Usage: ./rif.exe [options] input.gtirb

  --function     the function to be RIF-checked
  --rely         the rely condition
  --guar         the guarantee condition
  --verbose      enables verbose-mode output
  --concurrency  concurrency mode (safe / easy)
  --help         display this list

input.gtirb is expected to be a plain gtirb file produced by ddisasm. You can run ddisasm using docker or however you want. You do not need to run gtirb-semantics or anything else on ddisasm's output. rif does this internally.

--function <name> is expected to be the name of a function locatable via the symbol table. e.g. for the example secret_write.c, you could run rif with --function reader or --function writer. rif will search through the symbol table in order to locate this function within the binary, and will only lift/further analyse this one function. This lets you only worry about having one, function-local spec per "run" of the rif tool, and also greatly reduces the time spent analysing/lifting.

--verbose is a boolean flag. If --verbose is specified, rif will produce more detailed output. As rif is a highly experimental tool, at any given commit the output format is not at all specified, and may include debug print messages basically at random. However, --verbose is generally going to provide more detailed output.

--concurrency <mode> is an either/or flag. This flag is not currently supported, but was supported earlier in development, and it would be good to support it in the future. This flag lets you choose between "safe" concurrency, where any variables not given in the rely go to arbitrary nondeterministic values, or "easy" concurrency, where any variables not given in the rely remain unchanged. Essentially, given the guarantee mentions some variable x, if rely doesn't mention x, then it will either be reinitialised at every rely step with a fresh nondeterministic value, or it will be unchanged at every rely step. This lets users write more simplified specifications, without needing to explicitly state "x goes to nondeterminism" or "x goes to x" for every variable in their guar.

Currently, --concurrency defaults to safe and cannot be changed (i.e. un-specified variables will be reinitialised at every rely step).

Specification

--rely <spec> and --guar <spec> both take strings and parse them as specifications. The specification format is described here.

A spec is a bracketed, semicolon-separated list of "functions" or "constraints". While a spec is agnostic to whether it contains "functions" or "constraints", in practice, "functions" are only really supported in rely conditions, and "constraints" are only really supported in guar conditions.

Additionally, while a body (described soon) is agnostic to what sort (cvc5 type) it is, in practice, constraints expect their bodies to be of boolean sort and functions expect their bodies to be of numeric sort. (Numeric sort here means the same sort as registers. This is internally defined as the integer sort, but may change.)

An grammar for specs is provided here:

digit = '0' .. '0' | 'a' .. 'f' | 'A' .. 'F'
word = '0' .. '9' | 'a' .. 'z' | 'A' .. 'Z' | '_'
prime = '\''
space = ' '

true = "true" | "True"
false = "false" | "False"
nondeterminism = "???"      # Represents "Some new unbound value"

var = word+
whitespace = space*

kind = "=="     # Equality
     | "!="     # Inequality
     | "~"      # Negation
     | "!"      # Also negation
     | "&&"     # Boolean and
     | "||"     # Boolean or
     | "==>"    # Boolean implies
     | "^"      # Boolean xor
     | "?"      # if-then-else
     | "+"      # Integer addition
     | "*"      # Integer multiplication
     | "&"      # Integer bitwise and
     | "-"      # Integer subtraction (must have bitwidth specified)
     | "/"      # Integer division
     | "<"      # Less-than
     | ">"      # Greater-than
     | "<="     # Less-than-equal
     | ">="     # Greater-than-equal

inner = '(' body ')' whitespace

body = var '(' var prime? ')'
     | digit+
     | true
     | false
     | nondeterminism
     | '(' kind whitespace inner+ ')'

spec = '(' body ')'
     | '(' var "->" body ')'

Examples

A rely spec that x and y are unchanged:

(x -> (x)); (y -> (y))

A rely spec that x and y could be arbitrarily modified:

(x -> ???); (y -> ???)

A rely spec where x is some lock variable, and if it is taken ("locked"), nothing changes, but otherwise, anything can happen:

(x -> (? (locked(x)) ((x)) (???))); (y -> (? (locked(x)) ((y)) (???)))

A guarantee spec that x and y are unmodified:

((== ((x)) ((x')))); ((== ((y)) ((y'))))

A rough gurarantee for the writer of secret_write:

((==> (locked(x')) (secret(y'))))