Merge branch 'sail2' of github.com:rems-project/sail into sail2

2 files changed, 25 insertions, 15 deletions

diff --git a/src/jib/anf.ml b/src/jib/anf.ml
index 0a410249..c7f86cd4 100644
--- a/src/jib/anf.ml
+++ b/src/jib/anf.ml
@@ -518,7 +518,7 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) =
      raise (Reporting.err_unreachable l __POS__
        ("Encountered complex l-expression " ^ string_of_lexp lexp ^ " when converting to ANF"))
 
-  | E_loop (loop_typ, cond, exp) ->
+  | E_loop (loop_typ, _, cond, exp) ->
      let acond = anf cond in
      let aexp = anf exp in
      mk_aexp (AE_loop (loop_typ, acond, aexp))
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index 4a72ffff..a59f6c80 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -254,23 +254,32 @@ let rec compile_aval l ctx = function
      (F_id gs, ctyp),
      [iclear ctyp gs]
 
-  | AV_vector ([], _) ->
-     raise (Reporting.err_general l "Encountered empty vector literal")
+  | AV_vector ([], typ) ->
+     let vector_ctyp = ctyp_of_typ ctx typ in
+     begin match ctyp_of_typ ctx typ with
+     | CT_fbits (0, _) ->
+        [], (F_lit (V_bits []), vector_ctyp), []
+     | _ ->
+        let gs = ngensym () in
+        [idecl vector_ctyp gs;
+         iextern (CL_id (gs, vector_ctyp)) (mk_id "internal_vector_init") [(F_lit (V_int Big_int.zero), CT_fint 64)]],
+        (F_id gs, vector_ctyp),
+        [iclear vector_ctyp gs]
+     end
 
   (* Convert a small bitvector to a uint64_t literal. *)
   | AV_vector (avals, typ) when is_bitvector avals && List.length avals <= 64 ->
-     begin
-       let bitstring = F_lit (V_bits (List.map value_of_aval_bit avals)) in
-       let len = List.length avals in
-       match destruct_vector ctx.tc_env typ with
-       | Some (_, Ord_aux (Ord_inc, _), _) ->
-          [], (bitstring, CT_fbits (len, false)), []
-       | Some (_, Ord_aux (Ord_dec, _), _) ->
-          [], (bitstring, CT_fbits (len, true)), []
-       | Some _ ->
-          raise (Reporting.err_general l "Encountered order polymorphic bitvector literal")
-       | None ->
-          raise (Reporting.err_general l "Encountered vector literal without vector type")
+     let bitstring = F_lit (V_bits (List.map value_of_aval_bit avals)) in
+     let len = List.length avals in
+     begin match destruct_vector ctx.tc_env typ with
+     | Some (_, Ord_aux (Ord_inc, _), _) ->
+        [], (bitstring, CT_fbits (len, false)), []
+     | Some (_, Ord_aux (Ord_dec, _), _) ->
+        [], (bitstring, CT_fbits (len, true)), []
+     | Some _ ->
+        raise (Reporting.err_general l "Encountered order polymorphic bitvector literal")
+     | None ->
+        raise (Reporting.err_general l "Encountered vector literal without vector type")
      end
 
   (* Convert a bitvector literal that is larger than 64-bits to a
@@ -1264,6 +1273,7 @@ and compile_def' n total ctx = function
 
   (* Termination measures only needed for Coq, and other theorem prover output *)
   | DEF_measure _ -> [], ctx
+  | DEF_loop_measures _ -> [], ctx
 
   | DEF_internal_mutrec fundefs ->
      let defs = List.map (fun fdef -> DEF_fundef fdef) fundefs in