SMT: Add property and counterexample directive

Rather than generating SMT from a function called check_sat, now find
any function with a $property directive and generate SMT for it, e.g.

$property
function prop_cap_round_trip(cap: bits(128)) -> bool = {
  let cap_rt = capToBits(capBitsToCapability(true, cap));
  cap == cap_rt
}

$property
function prop_base_lteq_top(capbits: bits(128)) -> bool = {
  let c = capBitsToCapability(true, capbits);
  let (base, top) = getCapBounds(c);
  let e = unsigned(c.E);
  e >= 51 | base <= top
}

The file property.ml has a function for gathering all the properties
in a file, as well as a rewrite-pass for properties with type
quantifiers, which allows us to handle properties like

function prop forall 'n, 'n <= 100. (bv: bits('n)) -> bool = exp

by rewriting to (conceptually)

function prop(bv: bits(MAX_BIT_WIDTH)) -> bool =
  if length(bv) > 100 then true else exp

The function return is now automatically negated (i.e. always true =
unsat, sometimes false = sat), which makes sense for quickcheck-type
properties.

1 files changed, 5 insertions, 2 deletions

diff --git a/src/error_format.ml b/src/error_format.ml
index 8e00c2b7..672373a2 100644
--- a/src/error_format.ml
+++ b/src/error_format.ml
@@ -50,7 +50,10 @@ let underline_double_from color cnum_from eol =
   Util.(String.make cnum_from ' ' ^ clear (color ("^" ^ String.make (eol - cnum_from - 1) '-')))
 
 let underline_double_to color cnum_to =
-  Util.(clear (color (String.make (cnum_to - 1) '-' ^ "^")))
+  if cnum_to = 0 then
+    Util.(clear (color "^"))
+  else
+    Util.(clear (color (String.make (cnum_to - 1) '-' ^ "^")))
 
 let format_code_double' fname in_chan lnum_from cnum_from lnum_to cnum_to contents ppf =
   skip_lines in_chan (lnum_from - 1);
@@ -85,7 +88,7 @@ let format_code_double fname lnum_from cnum_from lnum_to cnum_to contents ppf =
     begin
       try format_code_double' fname in_chan lnum_from cnum_from lnum_to cnum_to contents ppf; close_in in_chan
       with
-      | _ -> close_in_noerr in_chan; ()
+      | exn -> close_in_noerr in_chan; ()
     end
   with
   | _ -> ()