Fix bug when reading register through a cast

3 files changed, 70 insertions, 2 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 20fc1fb6..91e0ddc2 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -630,8 +630,8 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
 	                  (Action (Read_reg regform Nothing) 
 	                     (Frame (id_of_string "0")
 		                (E_aux (E_id (id_of_string "0")) (Unknown, (val_annot (reg_to_t regform)))) le lm Top), lm,le)
-                        | _ -> (Value v tag,lm,le) end)
-	              (fun a -> a )
+                        | _ -> (Value v Tag_empty,lm,le) end)
+	              (fun a -> update_stack a (add_to_top_frame (fun e -> (E_aux (E_cast typ e) (l,annot)))))
  (* TODO introduce coercions to change offset of vectors *)
     | E_id id -> 
       let name = get_id id in
diff --git a/src/test/run_tests.ml b/src/test/run_tests.ml
index d1a90f38..570c49aa 100644
--- a/src/test/run_tests.ml
+++ b/src/test/run_tests.ml
@@ -4,6 +4,7 @@ let tests = [
   "test1", Test1.defs;
   "test2", Test2.defs;
   "test3", Test3.defs;
+  "test4", Test4.defs;
   "pattern", Pattern.defs;
   "vectors", Vectors.defs;
   "regbits", Regbits.defs;
diff --git a/src/test/test4.sail b/src/test/test4.sail
new file mode 100644
index 00000000..50f3fa71
--- /dev/null
+++ b/src/test/test4.sail
@@ -0,0 +1,67 @@
+(* hack to display log messages. Syntax: LOG(0) := "log message"; *)
+val extern forall Type 'a . nat -> 'a effect { wmem , rmem }  LOG
+
+register (bit[1]) GPR0
+register (bit[1]) GPR1
+
+let (vector <0, 2, inc, (register<bit[1] >)>) GPR = [ GPR0, GPR1 ]
+
+(* if we access GPR with a bit or a nat - doing the conversion in the
+   caller, works as expected *)
+function unit good ((bit)  RA ) =
+{
+  LOG(0) := "good";
+  (nat) x := GPR[RA];
+}
+
+function unit good2 ((nat)  RA ) =
+{
+  LOG(0) := "good2";
+  (nat) x := GPR[RA];
+}
+
+(* but here, the first to_num_inc(RA) somehow inhibits the cast,
+   yielding to_num_inc(GPR0) instead of to_num_inc(0b0) *)
+function unit bad ((bit[1])  RA ) =
+{
+  LOG(0) := "bad";
+  (nat) x := GPR[RA];
+}
+
+(* and now, another bug - when DCR contains registers of bits instead of bit[0] *)
+
+register (bit) DCR0
+register (bit) DCR1
+
+let (vector <0, 2, inc, (register<bit >)>) DCR = [ DCR0, DCR1 ]
+
+(* also fails only when passing RA as a vector, nat and bit work fine as
+   above;
+   error message is different though, and very disturbing:
+   "error: No matching patterns in case", corresponding to the DCR[RA]
+   expression *)
+function unit bad2 ((bit[1])  RA ) =
+{
+  LOG(0) := "bad2";
+  (nat) x := DCR[RA];
+}
+
+
+function unit main () = {
+  LOG(0) := "init";
+
+  GPR[0] := 0b0;
+  GPR[1] := 0b1;
+
+  DCR[0] := bitzero;
+  DCR[1] := bitone;
+
+  good(bitzero);
+  good2(0);
+
+  (* a first bug *)
+  bad(0b0);
+
+  (* another bug :-) comment out first one to see it *)
+  bad2(0b0);
+}