package libsail

  1. Overview
  2. Docs

This file implements utilities for dealing with $property and $counterexample pragmas.

val find_properties : 'a Ast_defs.ast -> (string * string * Ast.l * 'a Ast.val_spec) Ast_util.Bindings.t

find_properties defs returns a mapping from ids to of 4-tuples of the form (prop_type, command, loc, val_spec), which contains the information from any pragmas of the form

$prop_type command ... val <val_spec>

where prop_type is either "counterexample" or "property" and the location loc is the location that was attached to the pragma

For a property

$prop_type val f : forall X, C. T -> bool

find the function body for id:

function f(args) = exp

and rewrite the function body to

function f(args) = if constraint(not(C)) then true else exp

The reason we do this is that the type information in T constrained by C might be lost when translating to Jib, as Jib types are simpler and less precise. If we then do random test generation/proving we want to ensure that inputs outside the constraints of the function are ignored.

type event =
  1. | Overflow
  2. | Assertion
  3. | Assumption
  4. | Match
  5. | Return
val string_of_event : event -> string
module Event : sig ... end
type query =
  1. | Q_all of event
  2. | Q_exist of event
  3. | Q_not of query
  4. | Q_and of query list
  5. | Q_or of query list
val default_query : query
type pragma = {
  1. query : query;
  2. litmus : string list;
val parse_pragma : Parse_ast.l -> string -> pragma

Innovation. Community. Security.