From 65228f7ea61535fa8961dcb8ce8f030e7359c479 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Mon, 24 Feb 2020 19:34:02 +0000
Subject: Allow overloading of subrange builtins for non-bitvectors

---
 lib/vector_dec.sail                     |  8 ++++++--
 lib/vector_inc.sail                     |  8 ++++++--
 test/smt/update_subrange.unsat.sail     | 12 ++++++++++++
 test/typecheck/pass/reg_32_64/v3.expect | 16 +++++++++-------
 4 files changed, 33 insertions(+), 11 deletions(-)
 create mode 100644 test/smt/update_subrange.unsat.sail

diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 6014ab8c..2a9e96f0 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -173,7 +173,7 @@ val or_vec = {
 
 overload operator | = {or_vec}
 
-val vector_subrange = {
+val subrange_bits = {
   ocaml: "subrange",
   interpreter: "subrange",
   lem: "subrange_vec_dec",
@@ -182,7 +182,9 @@ val vector_subrange = {
 } : forall ('n : Int) ('m : Int) ('o : Int), 0 <= 'o <= 'm < 'n.
   (bits('n), int('m), int('o)) -> bits('m - 'o + 1)
 
-val vector_update_subrange = {
+overload vector_subrange = {subrange_bits}
+
+val update_subrange_bits = {
   ocaml: "update_subrange",
   interpreter: "update_subrange",
   lem: "update_subrange_vec_dec",
@@ -190,6 +192,8 @@ val vector_update_subrange = {
   coq: "update_subrange_vec_dec"
 } : forall 'n 'm 'o, 0 <= 'o <= 'm < 'n. (bits('n), int('m), int('o), bits('m - ('o - 1))) -> bits('n)
 
+overload vector_update_subrange = {update_subrange_bits}
+
 val sail_shiftleft = "shiftl" : forall 'n ('ord : Order).
     (bitvector('n, 'ord), int) -> bitvector('n, 'ord) effect pure
 
diff --git a/lib/vector_inc.sail b/lib/vector_inc.sail
index 381ae6bc..05f5c57f 100644
--- a/lib/vector_inc.sail
+++ b/lib/vector_inc.sail
@@ -108,7 +108,7 @@ val add_bits_int = {
 
 overload operator + = {add_bits, add_bits_int}
 
-val vector_subrange = {
+val subrange_bits = {
   ocaml: "subrange",
   interpreter: "subrange",
   lem: "subrange_vec_inc",
@@ -117,7 +117,9 @@ val vector_subrange = {
 } : forall ('n : Int) ('m : Int) ('o : Int), 0 <= 'm <= 'o < 'n.
   (bits('n), atom('m), atom('o)) -> bits('o - 'm + 1)
 
-val vector_update_subrange = {
+overload vector_subrange = {subrange_bits}
+
+val update_subrange_bits = {
   ocaml: "update_subrange",
   interpreter: "update_subrange",
   lem: "update_subrange_vec_inc",
@@ -125,6 +127,8 @@ val vector_update_subrange = {
   coq: "update_subrange_vec_inc"
 } : forall 'n 'm 'o, 0 <= 'm <= 'o < 'n. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
 
+overload vector_update_subrange = {update_subrange_bits}
+
 // Some ARM specific builtins
 
 /*
diff --git a/test/smt/update_subrange.unsat.sail b/test/smt/update_subrange.unsat.sail
new file mode 100644
index 00000000..5a6b2094
--- /dev/null
+++ b/test/smt/update_subrange.unsat.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <vector_dec.sail>
+
+$property
+function prop(xs: bits(65), ys: bits(5)) -> bool = {
+  xs' = xs;
+  xs'[63..59] = ys;
+  xs'[46..42] = ys;
+  xs'[4..0] = ys;
+  xs'[63..59] == ys & xs'[46..42] == ys & xs'[4..0] == ys
+}
diff --git a/test/typecheck/pass/reg_32_64/v3.expect b/test/typecheck/pass/reg_32_64/v3.expect
index cea45127..6de59040 100644
--- a/test/typecheck/pass/reg_32_64/v3.expect
+++ b/test/typecheck/pass/reg_32_64/v3.expect
@@ -1,10 +1,12 @@
 Type error:
-[reg_32_64/v3.sail]:29:15-21
+[reg_32_64/v3.sail]:29:2-27
 29 |  reg_deref(R)['d - 1 .. 0]
-   |               ^----^
-   | No overloading for (operator -), tried:
-   | * sub_atom
-   |    Cannot re-write sizeof('d)
-   | * sub_int
-   |    Cannot re-write sizeof('d)
+   |  ^-----------------------^
+   | No overloading for vector_subrange, tried:
+   | * subrange_bits
+   |    No overloading for (operator -), tried:
+   |    * sub_atom
+   |       Cannot re-write sizeof('d)
+   |    * sub_int
+   |       Cannot re-write sizeof('d)
    | 
-- 
cgit v1.2.3