13 files changed, 124 insertions, 57 deletions

diff --git a/lib/arith.sail b/lib/arith.sail
index 6b064433..58f25bbc 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -88,13 +88,38 @@ val tdiv_int = {
 } : (int, int) -> int
 
 /*! Remainder for truncating division (has sign of dividend) */
-val tmod_int = {
+val _tmod_int = {
   ocaml: "tmod_int",
   interpreter: "tmod_int",
   lem: "tmod_int",
   c: "tmod_int",
   coq: "Z.rem"
-} : (int, int) -> nat
+} : (int, int) -> int
+
+/*! If we know the second argument is positive, we know the result is positive */
+val _tmod_int_positive = {
+  ocaml: "tmod_int",
+  interpreter: "tmod_int",
+  lem: "tmod_int",
+  c: "tmod_int",
+  coq: "Z.rem"
+} : forall 'n, 'n >= 1. (int, int('n)) -> nat
+
+overload tmod_int = {_tmod_int_positive, _tmod_int}
+
+function fdiv_int(n: int, m: int) -> int = {
+  if n < 0 & m > 0 then {
+    tdiv_int(n + 1, m) - 1
+  } else if n > 0 & m < 0 then {
+    tdiv_int(n - 1, m) - 1
+  } else {
+    tdiv_int(n, m)
+  }
+}
+
+function fmod_int(n: int, m: int) -> int = {
+  n - (m * fdiv_int(n, m))
+}
 
 val abs_int_plain = {
   smt : "abs",
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index cd86840b..11bfa2fc 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -711,8 +711,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      let ctyp = ctyp_of_typ ctx typ in
      let aexp_setup, aexp_call, aexp_cleanup = compile_aexp ctx aexp in
      let try_return_id = ngensym () in
-     let handled_exception_label = label "handled_exception_" in
-     let fallthrough_label = label "fallthrough_exception_" in
+     let post_exception_handlers_label = label "post_exception_handlers_" in
      let compile_case (apat, guard, body) =
        let trivial_guard = match guard with
          | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _, _)
@@ -733,19 +732,19 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
               @ [icomment "end guard"]
             else [])
          @ body_setup @ [body_call (CL_id (try_return_id, ctyp))] @ body_cleanup @ destructure_cleanup
-         @ [igoto handled_exception_label]
+         @ [igoto post_exception_handlers_label]
        in
        [iblock case_instrs; ilabel try_label]
      in
      assert (ctyp_equal ctyp (ctyp_of_typ ctx typ));
      [idecl ctyp try_return_id;
       itry_block (aexp_setup @ [aexp_call (CL_id (try_return_id, ctyp))] @ aexp_cleanup);
-      ijump l (V_call (Bnot, [V_id (have_exception, CT_bool)])) handled_exception_label]
+      ijump l (V_call (Bnot, [V_id (have_exception, CT_bool)])) post_exception_handlers_label;
+      icopy l (CL_id (have_exception, CT_bool)) (V_lit (VL_bool false, CT_bool))]
      @ List.concat (List.map compile_case cases)
-     @ [igoto fallthrough_label;
-        ilabel handled_exception_label;
-        icopy l (CL_id (have_exception, CT_bool)) (V_lit (VL_bool false, CT_bool));
-        ilabel fallthrough_label],
+     @ [(* fallthrough *)
+        icopy l (CL_id (have_exception, CT_bool)) (V_lit (VL_bool true, CT_bool));
+        ilabel post_exception_handlers_label],
      (fun clexp -> icopy l clexp (V_id (try_return_id, ctyp))),
      []
 
diff --git a/test/builtins/divmod.sail b/test/builtins/divmod.sail
index f9d7e7c5..458d8dfd 100644
--- a/test/builtins/divmod.sail
+++ b/test/builtins/divmod.sail
@@ -5,39 +5,67 @@ $include <arith.sail>
 $include <smt.sail>
 
 function main (() : unit) -> unit = {
-  assert(ediv_int( 7 ,  5) ==  1);
-  assert(ediv_int( 7 , -5) == -1);
-  assert(ediv_int(-7 ,  5) == -2);
-  assert(ediv_int(-7 , -5) ==  2);
-  assert(ediv_int( 12 ,  3) ==  4);
-  assert(ediv_int( 12 , -3) == -4);
-  assert(ediv_int(-12 ,  3) == -4);
-  assert(ediv_int(-12 , -3) ==  4);
+  assert(ediv_int(7, 5) == 1);
+  assert(ediv_int(7, -5) == -1);
+  assert(ediv_int(-7, 5) == -2);
+  assert(ediv_int(-7, -5) == 2);
+  assert(ediv_int(12, 3) == 4);
+  assert(ediv_int(12, -3) == -4);
+  assert(ediv_int(-12, 3) == -4);
+  assert(ediv_int(-12, -3) == 4);
   
-  assert(emod_int( 7 ,  5) ==  2);
-  assert(emod_int( 7 , -5) ==  2);
-  assert(emod_int(-7 ,  5) ==  3);
-  assert(emod_int(-7 , -5) ==  3);
-  assert(emod_int( 12 ,  3) == 0);
-  assert(emod_int( 12 , -3) == 0);
-  assert(emod_int(-12 ,  3) == 0);
-  assert(emod_int(-12 , -3) == 0);
+  assert(emod_int(7, 5) == 2);
+  assert(emod_int(7, -5) == 2);
+  assert(emod_int(-7, 5) == 3);
+  assert(emod_int(-7, -5) == 3);
+  assert(emod_int(12, 3) == 0);
+  assert(emod_int(12, -3) == 0);
+  assert(emod_int(-12, 3) == 0);
+  assert(emod_int(-12, -3) == 0);
 
-  assert(tdiv_int( 7 ,  5) ==  1);
-  assert(tdiv_int( 7 , -5) == -1);
-  assert(tdiv_int(-7 ,  5) == -1);
-  assert(tdiv_int(-7 , -5) ==  1);
-  assert(tdiv_int( 12 ,  3) ==  4);
-  assert(tdiv_int( 12 , -3) == -4);
-  assert(tdiv_int(-12 ,  3) == -4);
-  assert(tdiv_int(-12 , -3) ==  4);
+  assert(tdiv_int(7, 5) == 1);
+  assert(tdiv_int(7, -5) == -1);
+  assert(tdiv_int(-7, 5) == -1);
+  assert(tdiv_int(-7, -5) == 1);
+  assert(tdiv_int(12, 3) == 4);
+  assert(tdiv_int(12, -3) == -4);
+  assert(tdiv_int(-12, 3) == -4);
+  assert(tdiv_int(-12, -3) == 4);
   
-  assert(tmod_int( 7 ,  5) ==  2);
-  assert(tmod_int( 7 , -5) ==  2);
-  assert(tmod_int(-7 ,  5) == -2);
-  assert(tmod_int(-7 , -5) == -2);
-  assert(tmod_int( 12 ,  3) == 0);
-  assert(tmod_int( 12 , -3) == 0);
-  assert(tmod_int(-12 ,  3) == 0);
-  assert(tmod_int(-12 , -3) == 0);
+  assert(tmod_int(7, 5) == 2);
+  assert(tmod_int(7, -5) == 2);
+  assert(tmod_int(-7, 5) == -2);
+  assert(tmod_int(-7, -5) == -2);
+  assert(tmod_int(12, 3) == 0);
+  assert(tmod_int(12, -3) == 0);
+  assert(tmod_int(-12, 3) == 0);
+  assert(tmod_int(-12, -3) == 0);
+
+  assert(fdiv_int(7, 5) == 1);
+  assert(fdiv_int(7, -5) == -2);
+  assert(fdiv_int(-7, 5) == -2);
+  assert(fdiv_int(-7, -5) == 1);
+  assert(fdiv_int(12, 3) == 4);
+  assert(fdiv_int(12, -3) == -4);
+  assert(fdiv_int(-12, 3) == -4);
+  assert(fdiv_int(-12, -3) == 4);
+
+  assert(fmod_int(7, 5) == 2);
+  assert(fmod_int(7, -5) == -3);
+  assert(fmod_int(-7, 5) == 3);
+  assert(fmod_int(-7, -5) == -2);
+  assert(fmod_int(12, 3) == 0);
+  assert(fmod_int(12, -3) == 0);
+  assert(fmod_int(-12, 3) == 0);
+  assert(fmod_int(-12, -3) == 0);
+
+  assert(fdiv_int(5, 2) == 2);
+  assert(fdiv_int(-5, -2) == 2);
+  assert(fdiv_int(5, -2) == -3);
+  assert(fdiv_int(-5, 2) == -3);
+
+  assert(tdiv_int(5, 2) == 2);
+  assert(tdiv_int(-5, -2) == 2);
+  assert(tdiv_int(5, -2) == -2);
+  assert(tdiv_int(-5, 2) == -2);
 }
\ No newline at end of file
diff --git a/test/c/exception.expect b/test/c/exception.expect
index 79d97c6a..faab808f 100644
--- a/test/c/exception.expect
+++ b/test/c/exception.expect
@@ -4,3 +4,5 @@ Caught Estring
 test
 2nd try Caught Epair
 x = 33
+in g()
+Fall through OK
diff --git a/test/c/exception.sail b/test/c/exception.sail
index 4e74fcae..251852c9 100644
--- a/test/c/exception.sail
+++ b/test/c/exception.sail
@@ -47,6 +47,19 @@ function main () = {
     },
     _            => ()
   };
+  try throw(Eunknown()) catch {
+    _ => try let _ = g() in () catch {
+      _ => print("caught old exception")
+    }
+  };
+  try
+    try throw Eunknown() catch {
+      Estring(_) => ()
+    }
+  catch {
+    Eunknown() => print("Fall through OK"),
+    _ => ()
+  };
   f();
   ()
-}
\ No newline at end of file
+}
diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect
index 8045141f..6605aba4 100644
--- a/test/typecheck/pass/Replicate/v2.expect
+++ b/test/typecheck/pass/Replicate/v2.expect
@@ -2,7 +2,7 @@ Type error:
 [Replicate/v2.sail]:13:4-30
 13 |    replicate_bits(x, 'N / 'M)
    |    ^------------------------^
-   | Tried performing type coercion from {('ex194# : Int), true. bitvector(('M * 'ex194#), dec)} to bitvector('N, dec) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x)))
+   | Tried performing type coercion from {('ex215# : Int), true. bitvector(('M * 'ex215#), dec)} to bitvector('N, dec) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x)))
    | Coercion failed because:
    | Mismatched argument types in subtype check
    | 
diff --git a/test/typecheck/pass/constant_nexp/v2.expect b/test/typecheck/pass/constant_nexp/v2.expect
index 7c0e8093..75a7f380 100644
--- a/test/typecheck/pass/constant_nexp/v2.expect
+++ b/test/typecheck/pass/constant_nexp/v2.expect
@@ -3,6 +3,6 @@ Type error:
 12 |  let _ = czeros(sizeof('n - 10) + 20);
    |          ^--------------------------^
    | Could not resolve quantifiers for czeros
-   | * is_constant(('fv50#n : Int))
+   | * is_constant(('fv130#n : Int))
    | * (('n - 10) + 20) >= 0
    | 
diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect
index 8d061933..80ebe927 100644
--- a/test/typecheck/pass/existential_ast/v3.expect
+++ b/test/typecheck/pass/existential_ast/v3.expect
@@ -3,5 +3,5 @@ Type error:
 26 |  Some(Ctor1(a, x, c))
    |       ^------------^
    | Could not resolve quantifiers for Ctor1
-   | * datasize('ex276#)
+   | * datasize('ex297#)
    | 
diff --git a/test/typecheck/pass/existential_ast3/v1.expect b/test/typecheck/pass/existential_ast3/v1.expect
index b8427446..4e65ab38 100644
--- a/test/typecheck/pass/existential_ast3/v1.expect
+++ b/test/typecheck/pass/existential_ast3/v1.expect
@@ -4,17 +4,17 @@ Type error:
    |                                                ^---------------^
    | Tried performing type coercion from (int(33), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & 'n < 'd)). (int('d), int('n))} on (33, unsigned(a))
    | Coercion failed because:
-   | (int(33), int('ex232#)) is not a subtype of (int('ex227#), int('ex228#))
+   | (int(33), int('ex253#)) is not a subtype of (int('ex248#), int('ex249#))
    | [existential_ast3/v1.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex227# bound here
+   |    | 'ex248# bound here
    | [existential_ast3/v1.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex228# bound here
+   |    | 'ex249# bound here
    | [existential_ast3/v1.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex232# bound here
+   |    | 'ex253# bound here
    | 
diff --git a/test/typecheck/pass/existential_ast3/v2.expect b/test/typecheck/pass/existential_ast3/v2.expect
index 4df0b3aa..04d53f11 100644
--- a/test/typecheck/pass/existential_ast3/v2.expect
+++ b/test/typecheck/pass/existential_ast3/v2.expect
@@ -4,17 +4,17 @@ Type error:
    |                                                ^---------------^
    | Tried performing type coercion from (int(31), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & 'n < 'd)). (int('d), int('n))} on (31, unsigned(a))
    | Coercion failed because:
-   | (int(31), int('ex232#)) is not a subtype of (int('ex227#), int('ex228#))
+   | (int(31), int('ex253#)) is not a subtype of (int('ex248#), int('ex249#))
    | [existential_ast3/v2.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex227# bound here
+   |    | 'ex248# bound here
    | [existential_ast3/v2.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex228# bound here
+   |    | 'ex249# bound here
    | [existential_ast3/v2.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex232# bound here
+   |    | 'ex253# bound here
    | 
diff --git a/test/typecheck/pass/existential_ast3/v3.expect b/test/typecheck/pass/existential_ast3/v3.expect
index 61a664c5..cae93129 100644
--- a/test/typecheck/pass/existential_ast3/v3.expect
+++ b/test/typecheck/pass/existential_ast3/v3.expect
@@ -3,5 +3,5 @@ Type error:
 25 |    Some(Ctor(64, unsigned(0b0 @ b @ a)))
    |         ^-----------------------------^
    | Could not resolve quantifiers for Ctor
-   | * (datasize(64) & (0 <= 'ex271# & 'ex271# < 64))
+   | * (datasize(64) & (0 <= 'ex292# & 'ex292# < 64))
    | 
diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect
index e6ce41c6..9810cfd4 100644
--- a/test/typecheck/pass/if_infer/v1.expect
+++ b/test/typecheck/pass/if_infer/v1.expect
@@ -5,7 +5,7 @@ Type error:
    | No overloading for vector_access, tried:
    | * bitvector_access
    |    Could not resolve quantifiers for bitvector_access
-   |    * (0 <= 'ex188# & 'ex188# < 3)
+   |    * (0 <= 'ex209# & 'ex209# < 3)
    | * plain_vector_access
    |    No valid casts resulted in unification
    | 
diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect
index 7d796f18..707d2217 100644
--- a/test/typecheck/pass/if_infer/v2.expect
+++ b/test/typecheck/pass/if_infer/v2.expect
@@ -5,7 +5,7 @@ Type error:
    | No overloading for vector_access, tried:
    | * bitvector_access
    |    Could not resolve quantifiers for bitvector_access
-   |    * (0 <= 'ex188# & 'ex188# < 4)
+   |    * (0 <= 'ex209# & 'ex209# < 4)
    | * plain_vector_access
    |    No valid casts resulted in unification
    |