signed multiplication and quot

5 files changed, 88 insertions, 5 deletions

diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 860f76d7..22250e46 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -481,11 +481,16 @@ let function_map = [
   ("mult_range_vec", arith_op_range_vec ( * ) Unsigned 2);
   ("mult_vec_range", arith_op_vec_range ( * ) Unsigned 2);
   ("mult_overload_vec", arith_op_overflow_vec ( * ) Unsigned 2);
+  ("multiply_vec_signed", arith_op_vec ( * ) Signed 2);
+  ("mult_range_vec_signed", arith_op_range_vec ( * ) Signed 2);
+  ("mult_vec_range_signed", arith_op_vec_range ( * ) Signed 2);
+  ("mult_overflow_vec_signed", arith_op_overflow_vec ( * ) Signed 2);
   ("mod", arith_op_no0 (mod));
   ("mod_vec", arith_op_vec_no0 (mod)  Unsigned 1);
   ("mod_vec_range", arith_op_vec_range_no0 (mod) Unsigned 1);
   ("quot", arith_op_no0 (/));
   ("quot_vec", arith_op_vec_no0 (/)  Unsigned 1);
+  ("quot_vec_signed", arith_op_vec_no0 (/)  Signed 1);
   ("eq", eq);
   ("eq_vec_range", eq_vec_range);
   ("eq_range_vec", eq_range_vec);
diff --git a/src/lexer.mll b/src/lexer.mll
index 9866390a..e39d7c65 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -108,6 +108,7 @@ let kw_table =
      ("div",			 (fun x -> Div_));
      ("mod",			 (fun x -> Mod));
      ("quot",			 (fun x -> Quot));
+     ("quot_s",                  (fun x -> QuotUnderS));
      ("rem",			 (fun x -> Rem));
 
      ("barr",                    (fun x -> Barr));
@@ -219,6 +220,7 @@ rule token = parse
   | "<_si"				{ (LtUnderSi(r"<_si")) }
   | "<_u"				{ (LtUnderU(r"<_u")) }
   | "<_ui"				{ (LtUnderUi(r"<_ui")) }
+  | "*_s"                               { (StarUnderS(r"*_s")) }
   | "**_s"				{ (StarStarUnderS(r"**_s")) }
   | "**_si"				{ (StarStarUnderSi(r"**_si")) }
   | "*_u"				{ (StarUnderU(r"*_u")) }
diff --git a/src/parser.mly b/src/parser.mly
index 943a2669..040dbb7d 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -140,7 +140,7 @@ let make_vector_sugar order_set is_inc typ typ1 =
 %nonassoc Then
 %nonassoc Else
 
-%token Div_ Mod Quot Rem
+%token Div_ Mod Quot Rem QuotUnderS
 
 %token Bar Comma Dot Eof Minus Semi Under
 %token Lcurly Rcurly Lparen Rparen Lsquare Rsquare
@@ -160,7 +160,7 @@ let make_vector_sugar order_set is_inc typ typ1 =
 %token <string> GtEqUnderS GtEqUnderSi GtEqUnderU GtEqUnderUi GtGtUnderU GtUnderS
 %token <string> GtUnderSi GtUnderU GtUnderUi LtEqUnderS LtEqUnderSi LtEqUnderU
 %token <string> LtEqUnderUi LtUnderS LtUnderSi LtUnderU LtUnderUi StarStarUnderS StarStarUnderSi StarUnderS
-%token <string> StarUnderSi StarUnderU StarUnderUi TwoCarrot PlusUnderS MinusUnderS
+%token <string> StarUnderSi StarUnderU StarUnderUi TwoCarrot PlusUnderS MinusUnderS 
 
 %token <string> AmpI AtI CarrotI  DivI EqI ExclI GtI LtI PlusI StarI TildeI
 %token <string> AmpAmpI CarrotCarrotI ColonColonI EqDivEqI EqEqI ExclEqI ExclExclI
@@ -199,6 +199,8 @@ id:
     { idl (DeIid($3)) }
   | Lparen Deinfix Quot Rparen
     { idl (DeIid("quot")) }
+  | Lparen Deinfix QuotUnderS Rparen
+    { idl (DeIid("quot_s")) }
   | Lparen Deinfix Eq Rparen
     { Id_aux(DeIid($3),loc ()) }
   | Lparen Deinfix Excl Lparen
@@ -219,6 +221,8 @@ id:
     { idl (DeIid("+_s")) }
   | Lparen Deinfix Star Rparen
     { idl (DeIid($3)) }
+  | Lparen Deinfix StarUnderS Rparen
+    { idl (DeIid("*_s")) }
   | Lparen Deinfix AmpAmp Rparen
     { idl (DeIid($3)) }
   | Lparen Deinfix Bar Rparen
@@ -662,6 +666,8 @@ star_exp:
     { eloc (E_app_infix($1,Id_aux(Id("div"), locn 2 2), $3)) }
   | star_exp Quot starstar_exp
     { eloc (E_app_infix($1,Id_aux(Id("quot"), locn 2 2), $3)) }
+  | star_exp QuotUnderS starstar_exp
+    { eloc (E_app_infix($1,Id_aux(Id("quot_s"), locn 2 2), $3)) }
   | star_exp Rem starstar_exp
     { eloc (E_app_infix($1,Id_aux(Id("rem"), locn 2 2), $3)) }
   | star_exp Mod starstar_exp
@@ -686,6 +692,8 @@ star_right_atomic_exp:
     { eloc (E_app_infix($1,Id_aux(Id("div"), locn 2 2), $3)) }
   | star_exp Quot starstar_right_atomic_exp
     { eloc (E_app_infix($1,Id_aux(Id("quot"), locn 2 2), $3)) }
+  | star_exp QuotUnderS starstar_right_atomic_exp
+    { eloc (E_app_infix($1,Id_aux(Id("quot_s"), locn 2 2), $3)) }
   | star_exp Rem starstar_right_atomic_exp
     { eloc (E_app_infix($1,Id_aux(Id("rem"), locn 2 2), $3)) }
   | star_exp Mod starstar_right_atomic_exp
@@ -718,6 +726,10 @@ plus_right_atomic_exp:
     { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
   | plus_exp Minus star_right_atomic_exp
     { eloc (E_app_infix($1,Id_aux(Id("-"), locn 2 2), $3)) }
+  | plus_exp PlusUnderS star_right_atomic_exp
+    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
+  | plus_exp MinusUnderS star_right_atomic_exp
+    { eloc (E_app_infix($1,Id_aux(Id("-_s"), locn 2 2), $3)) }
 
 shift_exp:
   | plus_exp
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index b07b16c3..4ea9ea63 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -834,7 +834,7 @@ let doc_exp, doc_let =
   and star_exp ((E_aux(e,_)) as expr) = match e with
   | E_app_infix(l,(Id_aux(Id (
       "*" | "/"
-    | "div" | "quot" | "rem" | "mod"
+    | "div" | "quot" | "quot_s" | "rem" | "mod"
     | "*_s" | "*_si" | "*_u" | "*_ui"),_) as op),r) ->
       doc_op (doc_id op) (star_exp l) (starstar_exp r)
   | _ -> starstar_exp expr
@@ -958,7 +958,7 @@ let doc_exp, doc_let =
     | ">>" | ">>>" | "<<" | "<<<"
     | "+" | "-" | "+_s" | "-_s"
     | "*" | "/"
-    | "div" | "quot" | "rem" | "mod"
+    | "div" | "quot" | "quot_s" | "rem" | "mod"
     | "*_s" | "*_si" | "*_u" | "*_ui"
     | "**"), _))
     , _) ->
diff --git a/src/type_internal.ml b/src/type_internal.ml
index e2399d88..86eb618a 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -1044,6 +1044,42 @@ let initial_typ_env =
                         External (Some "mult_vec_range"),
                        [LtEq(Specc(Parse_ast.Int("*",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp = N2n (mk_nv "m",None)})],pure_e);
                                      ]));
+    ("*_s",Overload(Base(((mk_typ_params ["a";"b";"c"]),
+                          (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})), External (Some "multiply"),[],pure_e),
+		    true,
+                    [Base(((mk_nat_params["n";"m";"o";"p"]),
+                           (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m");
+						 mk_range (mk_nv "o") (mk_nv "p")])
+	                      (mk_range (mk_mult (mk_nv "n") (mk_nv "o")) (mk_mult (mk_nv "m") (mk_nv "p"))))),
+		          External (Some "multiply_signed"), [],pure_e);
+                     Base(((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]),
+                           (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n");
+						 mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")])
+                           (* could also use 2*n instead of n+n *)
+                              (mk_vector bit_t (Ovar "ord") (Nvar "o") (Nadd (mk_nv "n", mk_nv "n"))))),
+                          External (Some "multiply_vec_signed"), [],pure_e);
+                     Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]),
+                           (mk_pure_fun (mk_tup [mk_range (mk_nv "o") (mk_nv "p");
+						 mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")])
+                            (* could also use 2*m instead of m+m *)
+                              (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nadd (mk_nv "m", mk_nv "m"))))),
+                          External (Some "mult_range_vec_signed"),
+			  [LtEq(Specc(Parse_ast.Int("*",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp = N2n (mk_nv "m",None)})],pure_e);
+                     Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]),
+                           (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");
+						 mk_range (mk_nv "o") (mk_nv "p")])
+                        (* could also use 2*m instead of m+m *)
+                              (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nadd (mk_nv "m", mk_nv "m"))))),
+                          External (Some "mult_vec_range_signed"),
+			  [LtEq(Specc(Parse_ast.Int("*",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp = N2n (mk_nv "m",None)})],pure_e);
+		     Base(((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]),
+                           (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n");
+						 mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")])
+                           (* could also use 2*n instead of n+n *)
+                              (mk_tup [(mk_vector bit_t (Ovar "ord") (Nvar "o") (Nadd (mk_nv "n", mk_nv "n")));bit_t]))),
+                          External (Some "mult_overflow_vec_signed"), [],pure_e);
+                     
+                    ]));
     ("mod",
      Overload(Base(((mk_typ_params ["a";"b";"c"]),
                     (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})),
@@ -1081,7 +1117,35 @@ let initial_typ_env =
                      (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");
                                            mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "q")])
                                    (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))),
-                    External (Some "quot_vec"),[GtEq(Specc(Parse_ast.Int("quot",None)), mk_nv "m", mk_nv "q")],pure_e)]));
+                    External (Some "quot_vec"),[GtEq(Specc(Parse_ast.Int("quot",None)), mk_nv "m", mk_nv "q")],pure_e);
+               Base(((mk_nat_params["n";"m";"p";"q"])@(mk_ord_params["ord"]),
+                     (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");
+                                           mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "q")])
+                                   (mk_tup [(mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")); bit_t]))),
+                    External (Some "quot_overflow_vec"),[GtEq(Specc(Parse_ast.Int("quot",None)), mk_nv "m", mk_nv "q")],pure_e)]));
+    ("quot_s",
+     Overload(Base(((mk_typ_params ["a";"b";"c"]),
+                    (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})),
+                   External (Some "quot_signed"),[],pure_e),
+	      true,
+              [Base(((mk_nat_params["n";"m";"o";"p";"q";"r"]),
+                     (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m"); mk_range (mk_nv "o") (mk_nv "p")])
+                        (mk_range (mk_nv "q") (mk_nv "r")))),
+                    External (Some "quot_signed"),[GtEq(Specc(Parse_ast.Int("quot",None)),(mk_nv "o"),{nexp = Nconst one});
+						   LtEq(Specc(Parse_ast.Int("quot",None)),
+							(mk_mult (mk_add (mk_nv "o") (mk_nv "p")) (mk_add (mk_nv "q") (mk_nv "r"))),
+							(mk_add (mk_nv "n") (mk_nv "m")))],pure_e);
+               Base(((mk_nat_params["n";"m";"p";"q"])@(mk_ord_params["ord"]),
+                     (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");
+                                           mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "q")])
+                        (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))),
+                    External (Some "quot_vec_signed"),[GtEq(Specc(Parse_ast.Int("quot",None)), mk_nv "m", mk_nv "q")],pure_e);
+	       Base(((mk_nat_params["n";"m";"p";"q"])@(mk_ord_params["ord"]),
+                     (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");
+                                           mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "q")])
+                                   (mk_tup [(mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")); bit_t]))),
+                    External (Some "quot_overflow_vec_signed"),[GtEq(Specc(Parse_ast.Int("quot",None)), mk_nv "m", mk_nv "q")],pure_e);
+]));
     (* incorrect types for typechecking processed sail code; do we care? *)
     ("length", Base((["a",{k=K_Typ}]@(mk_nat_params["n";"m"])@(mk_ord_params["ord"]),
 		     (mk_pure_fun (mk_vector {t=Tvar "a"} (Ovar "ord") (Nvar "n") (Nvar "m"))