Signed and unsigned comparisons

2 files changed, 64 insertions, 6 deletions

diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index edc7ebfd..1aed6521 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -430,7 +430,7 @@ let rec compare_op op (V_tuple args) = match args with
     then V_lit(L_aux L_one lx)
     else V_lit(L_aux L_zero lx)
 end ;;
-let rec compare_op_vec op (V_tuple args) = match args with
+let rec compare_op_vec op sign (V_tuple args) = match args with
   | [V_track v1 r1;V_track v2 r2] ->
     taint (compare_op_vec op (V_tuple [v1;v2])) (r1++r2)
   | [V_track v1 r1;v2] ->
@@ -440,7 +440,7 @@ let rec compare_op_vec op (V_tuple args) = match args with
   | [V_unknown;_] -> V_unknown
   | [_;V_unknown] -> V_unknown
   | [((V_vector _ _ _) as l1);((V_vector _ _ _) as l2)] ->
-    let (l1',l2') = (to_num Signed l1, to_num Signed l2) in
+    let (l1',l2') = (to_num sign l1, to_num sign l2) in
     compare_op op (V_tuple[l1';l2'])
 end ;;
 let rec compare_op_vec_unsigned op (V_tuple args) = match args with
@@ -559,10 +559,14 @@ let function_map = [
   ("gt", compare_op (>));
   ("lteq", compare_op (<=));
   ("gteq", compare_op (>=));
-  ("lt_vec", compare_op_vec (<));
-  ("gt_vec", compare_op_vec (>));
-  ("lteq_vec", compare_op_vec (<=));
-  ("gteq_vec", compare_op_vec (>=));
+  ("lt_vec", compare_op_vec Unsigned (<));
+  ("gt_vec", compare_op_vec Unsigned (>));
+  ("lteq_vec", compare_op_vec Unsigned (<=));
+  ("gteq_vec", compare_op_vec Unsigned (>=));
+  ("lt_vec_signed", compare_op_vec Signed (<));
+  ("gt_vec_signed", compare_op_vec Signed (>));
+  ("lteq_vec_signed", compare_op_vec Signed (<=));
+  ("gteq_vec_signed", compare_op_vec Signed (>=));
   ("ltu", compare_op_vec_unsigned (<));
   ("gtu", compare_op_vec_unsigned (>));
   ("duplicate", duplicate);
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 86eb618a..3fcc2d62 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -1198,6 +1198,19 @@ let initial_typ_env =
 	    (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")]) bit_t)),
 	   External (Some "lt_vec"),[],pure_e);]));
+    ("<_s",
+     Overload(Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)),External (Some "lt"),[],pure_e),
+	      false,
+	      [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")]) bit_t)),
+		    External (Some "lt_signed"),
+		    [LtEq(Specc(Parse_ast.Int("<",None)),
+			  {nexp=Nadd({nexp=Nadd({nexp=Nvar "n"},{nexp=Nvar "m"})},{nexp=Nconst one})},
+			  {nexp=Nadd({nexp=Nvar "o"},{nexp=Nvar "p"})})],pure_e);
+	       Base((((mk_nat_params ["n";"o";"p"])@["ord",{k=K_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")]) bit_t)),
+		    External (Some "lt_vec_signed"),[],pure_e);]));
     (">",
      Overload(Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)),External (Some "gt"),[],pure_e),
 	      false,
@@ -1211,6 +1224,19 @@ let initial_typ_env =
 	    (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")]) bit_t)), 
 	   External (Some "gt_vec"),[],pure_e);]));
+    (">_s",
+     Overload(Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)),External (Some "gt"),[],pure_e),
+	      false,
+	      [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")]) bit_t)),
+		    External (Some "gt_signed"),
+	   [GtEq(Specc(Parse_ast.Int(">",None)),
+		 {nexp=Nadd({nexp=Nvar "n"},{nexp=Nvar "m"})},
+		 {nexp=Nadd({nexp=Nadd({nexp=Nvar "o"},{nexp=Nvar "p"})},{nexp=Nconst one})})],pure_e);
+	       Base((((mk_nat_params ["n";"o";"p"])@[("ord",{k=K_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")]) bit_t)), 
+		    External (Some "gt_vec_signed"),[],pure_e);]));
     ("<=",
      Overload(Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)),External (Some "lteq"),[],pure_e),
 	      false,
@@ -1224,6 +1250,19 @@ let initial_typ_env =
 		     (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")]) bit_t)),
 		    External (Some "lteq_vec"),[],pure_e);]));
+    ("<=_s",
+     Overload(Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)),External (Some "lteq"),[],pure_e),
+	      false,
+	      [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")]) bit_t)),
+		    External (Some "lteq_signed"),
+		    [LtEq(Specc(Parse_ast.Int("<=",None)),
+			  {nexp=Nadd({nexp=Nadd({nexp=Nvar "n"},{nexp=Nvar "m"})},{nexp=Nconst one})},
+			  {nexp=Nadd({nexp=Nvar "o"},{nexp=Nvar "p"})})],pure_e);
+	       Base((((mk_nat_params ["n";"o";"p"])@["ord",{k=K_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")]) bit_t)),
+		    External (Some "lteq_vec_signed"),[],pure_e);]));
     (">=",
      Overload(Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)),External (Some "gteq"),[],pure_e),
 	      false,
@@ -1237,6 +1276,21 @@ let initial_typ_env =
 	    (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")]) bit_t)), 
 	   External (Some "gteq_vec"),[],pure_e);]));
+    (">=_s",
+     Overload(Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)),External (Some "gteq"),[],pure_e),
+	      false,
+	      [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")]) bit_t)),
+		    External (Some "gteq_signed"),
+		    [GtEq(Specc(Parse_ast.Int(">",None)),
+			  {nexp=Nadd({nexp=Nvar "n"},{nexp=Nvar "m"})},
+			  {nexp=Nadd({nexp=Nadd({nexp=Nvar "o"},{nexp=Nvar "p"})},{nexp=Nconst one})})],pure_e);
+	       Base((((mk_nat_params ["n";"o";"p"])@[("ord",{k=K_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")]) bit_t)), 
+		    External (Some "gteq_vec_signed"),[],pure_e);]));
+    (*Unlikely to be the correct type; probably needs to be bit vectors*)
+    ("<_u",Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)),External (Some "ltu"),[],pure_e));
     (*Unlikely to be the correct type; probably needs to be bit vectors*)
     ("<_u",Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)),External (Some "ltu"),[],pure_e));
     (">_u",Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)),External (Some "gtu"),[],pure_e));