Improvements to sail n_constraints

1) Added a new construct to the expression level: constraint. This is the
essentially the boolean form of sizeof. Whereas sizeof takes a nexp
and has type [:'n:], constraint takes a n_constraint and returns a
boolean. The hope is this will allow for flow typing to be represented
more explicitly in the generatated sail from ASL.

For example we could have something like:

default Order dec

val bit[64] -> unit effect pure test64

val forall 'n, ('n = 32 | 'n = 64 | 'n = 10) & 'n != 43. bit['n] -> unit effect pure test

function forall 'n. unit test addr =
{
  if constraint('n = 32) then {
    ()
  } else {
    assert(constraint('n = 64), "64-bit mode");
    test64(addr)
  }
}

2) The other thing this example demonstrates is that flow constraints
now work with assert and not just if. Even though flow typing will
only guarantee us that 'n != 32 in the else branch, the assert gives
us 'n = 64. This is very useful as it's a common idiom in the ARM
spec to guarantee such things with an assert.

3) Added != to the n_constraint language

4) Changed the n_constraint language to add or and and as constructs
in constraints. Previously one could have a list of conjuncts each of
which were simple inequalites or set constraints, now one can do for
example:

val forall 'n, ('n = 32 | 'n = 64) & 'n in {32, 64}. bit['n] -> unit effect pure test

This has the very nice upside that every n_constraint can now be
negatated when flow-typing if statements. Note also that 'in' has been
introduced as a synonym for 'IN' in the constraint 'n in {32,64}. The
use of a block capital keyword was a bit odd there because all the
other keywords are lowercase.

1 files changed, 21 insertions, 1 deletions

diff --git a/src/parser.mly b/src/parser.mly
index 6a76cec9..ef56934e 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -131,7 +131,7 @@ let make_vector_sugar order_set is_inc typ typ1 =
 %token And Alias As Assert Bitzero Bitone Bits By Case Clause Const Dec Def Default Deinfix Effect EFFECT End 
 %token Enumerate Else Exit Extern False Forall Foreach Overload Function_ If_ In IN Inc Let_ Member Nat NatNum Order Cast
 %token Pure Rec Register Return Scattered Sizeof Struct Switch Then True TwoStarStar Type TYPE Typedef 
-%token Undefined Union With When Val
+%token Undefined Union With When Val Constraint
 %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
 
 
@@ -593,6 +593,8 @@ atomic_exp:
     { eloc (E_case($2,$4)) }
   | Sizeof atomic_typ
     { eloc (E_sizeof($2)) }
+  | Constraint Lparen nexp_constraint Rparen
+    { eloc (E_constraint $3) }
   | Exit atomic_exp
       { eloc (E_exit $2) }
   | Return atomic_exp
@@ -1053,14 +1055,32 @@ nums:
     { $1::$3 }
 
 nexp_constraint:
+  | nexp_constraint1
+    { $1 }
+  | nexp_constraint1 Bar nexp_constraint
+    { NC_aux (NC_or ($1, $3), loc ()) }
+
+nexp_constraint1:
+  | nexp_constraint2
+    { $1 }
+  | nexp_constraint2 Amp nexp_constraint1
+    { NC_aux (NC_and ($1, $3), loc ()) }
+
+nexp_constraint2:
   | nexp_typ Eq nexp_typ
     { NC_aux(NC_fixed($1,$3), loc () ) }
+  | nexp_typ ExclEq nexp_typ
+    { NC_aux (NC_not_equal ($1, $3), loc ()) }
   | nexp_typ GtEq nexp_typ
     { NC_aux(NC_bounded_ge($1,$3), loc () ) }
   | nexp_typ LtEq nexp_typ
     { NC_aux(NC_bounded_le($1,$3), loc () ) }
+  | tyvar In Lcurly nums Rcurly
+    { NC_aux(NC_nat_set_bounded($1,$4), loc ()) }
   | tyvar IN Lcurly nums Rcurly
     { NC_aux(NC_nat_set_bounded($1,$4), loc ()) }
+  | Lparen nexp_constraint Rparen
+    { $2 }
 
 id_constraint:
   | nexp_constraint