Add some missing functions

3 files changed, 97 insertions, 4 deletions

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 90d162e7..29deb6ec 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -175,9 +175,27 @@ let initial_instruction_state top_level main args =
   Interp.Thunk_frame (E_aux (E_app (Id_aux (Id main) Interp_ast.Unknown) e_args) (Interp_ast.Unknown, Nothing)) 
     top_level Interp.eenv Interp.emem Interp.Top
 
-(*For now, append to this list to add more external functions; should add to the mode record for more perhaps *)
+let rec countLeadingZeros_helper bits =
+  match bits with
+    | (Interp.V_lit (L_aux L_zero _))::bits -> 
+      let (Interp.V_lit (L_aux (L_num n) loc)) = countLeadingZeros_helper bits in
+      Interp.V_lit (L_aux (L_num (n+1)) loc)
+    | _ -> Interp.V_lit (L_aux (L_num 0) Interp_ast.Unknown)
+end
+let rec countLeadingZeros v = match v with
+  | Interp.V_unknown -> Interp.V_unknown
+  | Interp.V_track v r -> Interp.taint (countLeadingZeros v) r
+  | Interp.V_vector _ _ bits -> countLeadingZeros_helper bits
+end
+
+(*Power specific external functions*)
+let power_externs = [
+  ("countLeadingZeros", countLeadingZeros);
+]
+
+(*All external functions*)
 let external_functions = 
-  Interp_lib.function_map
+  Interp_lib.function_map ++ power_externs
 
 type mem_function = (string * 
                      (maybe read_kind * maybe write_kind * (interp_mode -> Interp.value -> (value * (maybe (list reg_name))))))
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 6c0d5b31..c5475017 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -289,6 +289,32 @@ let rec arith_op_vec_range_range op (V_tuple args) = match args with
   | [(V_vector _ ord _ as l1);n] ->
     arith_op op (V_tuple [(to_num Unsigned l1);n])
 end ;;
+let rec arith_op_no0 op (V_tuple args) = match args with
+  | [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] -> 
+    if y = 0 
+    then V_lit (L_aux L_undef ly)
+    else V_lit(L_aux (L_num (op x y)) lx)
+  | [V_track v1 r1;V_track v2 r2] -> taint (arith_op_no0 op (V_tuple [v1;v2])) (r1++r2)
+  | [V_track v1 r1;v2] -> taint (arith_op_no0 op (V_tuple [v1;v2])) r1
+  | [v1;V_track v2 r2] -> taint (arith_op_no0 op (V_tuple [v1;v2])) r2
+  | [V_unknown;_] -> V_unknown
+  | [_;V_unknown] -> V_unknown
+  end ;;
+let rec arith_op_vec_no0 op size (V_tuple args) = match args with
+  | [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
+    let (l1',l2') = (to_num Unsigned l1,to_num Unsigned l2) in
+    let n = arith_op_no0 op (V_tuple [l1';l2']) in
+    to_vec ord ((List.length cs) * size) n
+  | [V_track v1 r1;V_track v2 r2] ->
+    taint (arith_op_vec_no0 op size (V_tuple [v1;v2])) (r1++r2)
+  | [V_track v1 r1;v2] ->
+    taint (arith_op_vec_no0 op size (V_tuple [v1;v2])) r1
+  | [v1;V_track v2 r2] ->
+    taint (arith_op_vec_no0 op size (V_tuple [v1;v2])) r2
+  | [V_unknown;_] -> V_unknown
+  | [_;V_unknown] -> V_unknown
+end ;;
+
 
 let rec compare_op op (V_tuple args) = match args with
   | [V_track v1 r1;V_track v2 r2] ->
@@ -317,6 +343,21 @@ let rec compare_op_vec op (V_tuple args) = match args with
     let (l1',l2') = (to_num Signed l1, to_num Signed l2) in
     compare_op op (V_tuple[l1';l2'])
 end ;;
+let rec compare_op_vec_unsigned op (V_tuple args) = match args with
+  | [V_track v1 r1;V_track v2 r2] ->
+    taint (compare_op_vec_unsigned op (V_tuple [v1;v2])) (r1++r2)
+  | [V_track v1 r1;v2] ->
+    taint (compare_op_vec_unsigned op (V_tuple [v1;v2])) r1
+  | [v1;V_track v2 r2] ->
+    taint (compare_op_vec_unsigned op (V_tuple [v1;v2])) r2
+  | [V_unknown;_] -> V_unknown
+  | [_;V_unknown] -> V_unknown
+  | [((V_vector _ _ _) as l1);((V_vector _ _ _) as l2)] ->
+    let (l1',l2') = (to_num Unsigned l1, to_num Unsigned l2) in
+    compare_op op (V_tuple[l1';l2'])
+end ;;
+
+
 
 let rec duplicate (V_tuple args) = match args with
   | [V_track v1 r1;V_track v2 r2] -> taint (duplicate (V_tuple [v1;v2])) (r1++r2)
@@ -371,9 +412,11 @@ let function_map = [
   ("mult_range_vec", arith_op_range_vec ( * ) 2);
   ("mult_vec_range", arith_op_vec_range ( * ) 2);
   ("mult_overload_vec", arith_op_overflow_vec ( * ) 2);
-  ("mod", arith_op (mod));
-  ("mod_vec", arith_op_vec (mod) 1);
+  ("mod", arith_op_no0 (mod));
+  ("mod_vec", arith_op_vec_no0 (mod) 1);
   ("mod_vec_range", arith_op_vec_range (mod) 1);
+  ("quot", arith_op_no0 (/));
+  ("quot_vec", arith_op_vec_no0 (/) 1);
   ("eq", eq);
   ("eq_vec_range", eq_vec_range);
   ("eq_range_vec", eq_range_vec);
@@ -395,8 +438,14 @@ let function_map = [
   ("bitwise_xor_bit", bitwise_binop_bit xor);
   ("lt", compare_op (<));
   ("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 (>=));
+  ("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 83d40e64..0eb7f5e6 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -1086,6 +1086,32 @@ 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);]));
+    ("<=",
+     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"),
+		    [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"),[],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,
+     [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"),
+	   [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"),[],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));