C: Fix an issue with assigning to unitialized variables at end of blocks

Assigning to an uninitialized variable as the last statement in a
block is almost certainly a type, and if that occurs then the
lift_assign re-write will introduce empty blocks causing this error to
occur. Now when we see such an empty block when converting to A-normal
form we turn it into unit, and emit a warning stating that an empty
block has been found as well as the probable cause (uninitialized
variable).

3 files changed, 7 insertions, 2 deletions

diff --git a/src/anf.ml b/src/anf.ml
index e87f2bfd..38be1127 100644
--- a/src/anf.ml
+++ b/src/anf.ml
@@ -509,6 +509,10 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) =
   match e_aux with
   | E_lit lit -> mk_aexp (ae_lit lit (typ_of exp))
 
+  | E_block [] ->
+     Util.warn (Reporting_basic.loc_to_string l
+                ^ "\n\nTranslating empty block (possibly assigning to an uninitialized variable at the end of a block?)");
+     mk_aexp (ae_lit (L_aux (L_unit, l)) (typ_of exp))
   | E_block exps ->
      let exps, last = split_block l exps in
      let aexps = List.map anf exps in
diff --git a/src/rewrites.ml b/src/rewrites.ml
index f02943a5..eafbd6a8 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -1763,7 +1763,7 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f
          let e' = re' (rewrite_base e) in
          let exps' = walker exps in
          let effects = union_eff_exps exps' in
-         let block = E_aux (E_block exps', (l, mk_tannot env unit_typ effects)) in
+         let block = E_aux (E_block exps', (gen_loc l, mk_tannot env unit_typ effects)) in
          [fix_eff_exp (E_aux (E_var(le', e', block), annot))]
       (*| ((E_aux(E_if(c,t,e),(l,annot))) as exp)::exps ->
         let vars_t = introduced_variables t in
@@ -1815,7 +1815,7 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f
     when lexp_is_local_intro le (env_of full_exp) && not (lexp_is_effectful le) ->
     let (le', re') = rewrite_lexp_to_rhs le in
     let e' = re' (rewrite_base e) in
-    let block = annot_exp (E_block []) l (env_of full_exp) unit_typ in
+    let block = annot_exp (E_block []) (gen_loc l) (env_of full_exp) unit_typ in
     check_exp (env_of full_exp)
       (strip_exp (E_aux (E_var(le', e', block), annot))) (typ_of full_exp)
   | _ -> rewrite_base full_exp
diff --git a/src/sail.ml b/src/sail.ml
index ba19eb79..4cc22c40 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -324,6 +324,7 @@ let main() =
          let ast_c = rewrite_ast_c ast in
          let ast_c, type_envs = Specialize.specialize ast_c type_envs in
          let ast_c = Spec_analysis.top_sort_defs ast_c in
+         Util.opt_warnings := true;
          C_backend.compile_ast (C_backend.initial_ctx type_envs) (!opt_includes_c) ast_c
        else ());
       (if !(opt_print_lem)