More updates to C backend

Add support for short-ciruiting and/or. I forgot about this in the
original ANF specification and not having it causes problems for the
ARM spec.

3 files changed, 69 insertions, 0 deletions

diff --git a/lib/exception_basic.sail b/lib/exception_basic.sail
new file mode 100644
index 00000000..cab394b0
--- /dev/null
+++ b/lib/exception_basic.sail
@@ -0,0 +1,6 @@
+$ifndef _EXN_BASIC
+$define _EXN_BASIC
+
+newtype exception = Exception : unit
+
+$endif
diff --git a/lib/flow.sail b/lib/flow.sail
index 1a0e0f2f..b904c0bc 100644
--- a/lib/flow.sail
+++ b/lib/flow.sail
@@ -37,6 +37,11 @@ overload operator == = {eq_atom, eq_range, eq_int}
 overload operator | = {or_bool}
 overload operator & = {and_bool}
 
+overload operator <= = {lteq_atom, lteq_range_atom, lteq_atom_range}
+overload operator < = {lt_atom, lt_range_atom, lt_atom_range}
+overload operator >= = {gteq_atom, gteq_range_atom, gteq_atom_range}
+overload operator > = {gt_atom, gt_range_atom, gt_atom_range}
+
 $ifdef TEST
 
 val __flow_test : forall 'n 'm. (atom('n), atom('m)) -> unit
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 8a55ed61..130f4d63 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -1,15 +1,47 @@
 $ifndef _VECTOR_DEC
 $define _VECTOR_DEC
 
+$include <flow.sail>
+
 type bits ('n : Int) = vector('n, dec, bit)
 
+val "eq_bit" : (bit, bit) -> bool
+
+val "eq_bits" : forall 'n. (vector('n, dec, bit), vector('n, dec, bit)) -> bool
+
+overload operator == = {eq_bit, eq_bits}
+
+val bitvector_length = "length" : forall 'n. bits('n) -> atom('n)
+
+val vector_length = {
+  ocaml: "length",
+  lem: "length_list",
+  c: "length"
+} : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n)
+
+overload length = {bitvector_length, vector_length}
+
 val "zeros" : forall 'n. atom('n) -> bits('n)
 
 val "print_bits" : forall 'n. (string, bits('n)) -> unit
 
 val "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
+
 val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
 
+val "truncate" : forall 'm 'n, 'm <= 'n. (vector('n, dec, bit), atom('m)) -> vector('m, dec, bit)
+
+val mask : forall 'len 'v, 'v >= 0. (atom('len), vector('v, dec, bit)) -> vector('len, dec, bit)
+
+function mask(len, v) = if len <= length(v) then truncate(v, len) else zero_extend(v, len)
+
+overload operator ^ = {mask}
+
+val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int).
+  (bits('n), bits('m)) -> bits('n + 'm)
+
+overload append = {bitvector_concat}
+
 /* Used for creating long bitvector literals in the C backend. */
 val "append_64" : forall 'n. (bits('n), bits(64)) -> bits('n + 64)
 
@@ -35,4 +67,30 @@ val add_bits_int = {
   c: "add_bits_int"
 } : forall 'n. (bits('n), int) -> bits('n)
 
+overload operator + = {add_bits, add_bits_int}
+
+val vector_subrange = {
+  ocaml: "subrange",
+  lem: "subrange_vec_dec",
+  c: "vector_subrange"
+} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
+  (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
+
+val vector_update_subrange = {
+  ocaml: "update_subrange",
+  lem: "update_subrange_vec_dec",
+  c: "vector_update_subrange"
+} : forall 'n 'm 'o. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
+
+// Some ARM specific builtins
+
+val get_slice_int = "get_slice_int" : forall 'w. (atom('w), int, int) -> bits('w)
+
+val set_slice_int = "set_slice_int" : forall 'w. (atom('w), int, int, bits('w)) -> int
+
+val set_slice_bits = "set_slice" : forall 'n 'm.
+  (atom('n), atom('m), bits('n), int, bits('m)) -> bits('n)
+
+val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
+
 $endif