Fix rewriter issues

Allow pat_lits rewrite to map L_unit to wildcard patterns, rather than
introducing eq_unit tests as guards.

Add a fold_function and fold_funcl functions in rewriter.ml that apply
the pattern and expression algebras to top-level functions, which
means that they correctly get applied to top-level function patterns
when they are used. Currently modifying the re-writing passes to do
this introduces some bugs which needs investigated further. The
current situation is that top-level patterns and patterns elsewhere
are often treated differently because rewrite_exp doesn't (and indeed
cannot, due to how the re-writer is structured) rewrite top level
patterns.

Fix pattern completeness check for unit literals

Fix a bug in Sail->ANF transform where blocks were always annotated
with type unit incorrectly. This caused issues in pattern literal
re-writes where the guard was a block returning a boolean. A test case
for this is added as test/c/and_block.sail.

Fix a bug caused by nested polymorphic function calls and matching in
top-level patterns. Test case is test/c/tl_poly_match.sail.

Pass location info through codegen_conversion for better error
reporting

7 files changed, 40 insertions, 10 deletions

diff --git a/src/anf.ml b/src/anf.ml
index 845759cd..46e7a2fb 100644
--- a/src/anf.ml
+++ b/src/anf.ml
@@ -468,6 +468,7 @@ let rec anf_pat ?global:(global=false) (P_aux (p_aux, annot) as pat) =
   | P_var (pat, _) -> anf_pat ~global:global pat
   | P_cons (hd_pat, tl_pat) -> mk_apat (AP_cons (anf_pat ~global:global hd_pat, anf_pat ~global:global tl_pat))
   | P_list pats -> List.fold_right (fun pat apat -> mk_apat (AP_cons (anf_pat ~global:global pat, apat))) pats (mk_apat (AP_nil (pat_typ_of pat)))
+  | P_lit (L_aux (L_unit, _)) -> mk_apat (AP_wild (pat_typ_of pat))
   | _ -> anf_error ~loc:(fst annot) ("Could not convert pattern to ANF: " ^ string_of_pat pat)
 
 let rec apat_globals (AP_aux (aux, _, _)) =
@@ -497,10 +498,11 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) =
       | AE_field (_, _, typ)
       | AE_case (_, _, typ)
       | AE_try (_, _, typ)
-      | AE_record_update (_, _, typ) ->
+      | AE_record_update (_, _, typ)
+      | AE_block (_, _, typ) ->
        let id = gensym () in
        (AV_id (id, Local (Immutable, typ)), fun x -> mk_aexp (AE_let (Immutable, id, typ, aexp, x, typ_of exp)))
-    | AE_assign _ | AE_block _ | AE_for _ | AE_loop _ ->
+    | AE_assign _ | AE_for _ | AE_loop _ ->
        let id = gensym () in
        (AV_id (id, Local (Immutable, unit_typ)), fun x -> mk_aexp (AE_let (Immutable, id, unit_typ, aexp, x, typ_of exp)))
   in
diff --git a/src/bytecode_util.ml b/src/bytecode_util.ml
index 856c9b47..4ddb0c81 100644
--- a/src/bytecode_util.ml
+++ b/src/bytecode_util.ml
@@ -222,6 +222,7 @@ let rec ctyp_equal ctyp1 ctyp2 =
   | CT_vector (d1, ctyp1), CT_vector (d2, ctyp2) -> d1 = d2 && ctyp_equal ctyp1 ctyp2
   | CT_list ctyp1, CT_list ctyp2 -> ctyp_equal ctyp1 ctyp2
   | CT_ref ctyp1, CT_ref ctyp2 -> ctyp_equal ctyp1 ctyp2
+  | CT_poly, CT_poly -> true
   | _, _ -> false
 
 let rec ctyp_unify ctyp1 ctyp2 =
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 63bfc734..83f8df31 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -815,7 +815,7 @@ let compile_funcall l ctx id args typ =
     setup := List.rev arg_setup @ !setup;
     cleanup := arg_cleanup @ !cleanup;
     let have_ctyp = cval_ctyp cval in
-    if is_polymorphic ctyp then
+    if ctyp_equal CT_poly ctyp then
       (F_poly (fst cval), have_ctyp)
     else if ctyp_equal ctyp have_ctyp then
       cval
@@ -2102,7 +2102,7 @@ let rec sgen_clexp_pure = function
    insert any needed type conversions from big integers to small
    integers (or vice versa), or from arbitrary-length bitvectors to
    and from uint64 bitvectors as needed. *)
-let rec codegen_conversion clexp cval =
+let rec codegen_conversion l clexp cval =
   let open Printf in
   let ctyp_to = clexp_ctyp clexp in
   let ctyp_from = cval_ctyp cval in
@@ -2115,12 +2115,12 @@ let rec codegen_conversion clexp cval =
        ksprintf string "  COPY(%s)(%s, %s);" (sgen_ctyp_name ctyp_to) (sgen_clexp clexp) (sgen_cval cval)
 
   | CT_ref ctyp_to, ctyp_from ->
-     codegen_conversion (CL_addr clexp) cval
+     codegen_conversion l (CL_addr clexp) cval
 
   (* If we have to convert between tuple types, convert the fields individually. *)
   | CT_tup ctyps_to, CT_tup ctyps_from when List.length ctyps_to = List.length ctyps_from ->
      let conversions =
-       List.mapi (fun i ctyp -> codegen_conversion (CL_tuple (clexp, i)) (F_field (fst cval, "ztup" ^ string_of_int i), ctyp)) ctyps_from
+       List.mapi (fun i ctyp -> codegen_conversion l (CL_tuple (clexp, i)) (F_field (fst cval, "ztup" ^ string_of_int i), ctyp)) ctyps_from
      in
      separate hardline conversions
 
@@ -2141,7 +2141,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
      ksprintf string "  %s %s;" (sgen_ctyp ctyp) (sgen_id id) ^^ hardline
      ^^ ksprintf string "  CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id)
 
-  | I_copy (clexp, cval) -> codegen_conversion clexp cval
+  | I_copy (clexp, cval) -> codegen_conversion l clexp cval
 
   | I_jump (cval, label) ->
      ksprintf string "  if (%s) goto %s;" (sgen_cval cval) label
diff --git a/src/pattern_completeness.ml b/src/pattern_completeness.ml
index c6fb5308..d54bbd3f 100644
--- a/src/pattern_completeness.ml
+++ b/src/pattern_completeness.ml
@@ -91,6 +91,9 @@ let is_wild = function
 
 let rec generalize ctx (P_aux (p_aux, _) as pat) =
   match p_aux with
+  | P_lit (L_aux (L_unit, _)) ->
+     (* Unit pattern always matches on unit, so generalize to wildcard *)
+     GP_wild
   | P_lit lit -> GP_lit lit
   | P_wild -> GP_wild
   | P_or (pat1, pat2) -> GP_or (generalize ctx pat1, generalize ctx pat2)
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 4521758b..15f100fd 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -308,6 +308,8 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot)) as orig_exp) =
   | E_field(exp,id) -> rewrap (E_field(rewrite exp,id))
   | E_case (exp,pexps) ->
     rewrap (E_case (rewrite exp, List.map (rewrite_pexp rewriters) pexps))
+  | E_try (exp,pexps) ->
+    rewrap (E_try (rewrite exp, List.map (rewrite_pexp rewriters) pexps))
   | E_let (letbind,body) -> rewrap (E_let(rewriters.rewrite_let rewriters letbind,rewrite body))
   | E_assign (lexp,exp) -> rewrap (E_assign(rewriters.rewrite_lexp rewriters lexp,rewrite exp))
   | E_sizeof n -> rewrap (E_sizeof n)
@@ -614,6 +616,12 @@ and fold_letbind_aux alg = function
   | LB_val (pat,e) -> alg.lB_val (fold_pat alg.pat_alg pat, fold_exp alg e)
 and fold_letbind alg (LB_aux (letbind_aux,annot)) = alg.lB_aux (fold_letbind_aux alg letbind_aux, annot)
 
+let fold_funcl alg (FCL_aux (FCL_Funcl (id, pexp), annot)) =
+  FCL_aux (FCL_Funcl (id, fold_pexp alg pexp), annot)
+
+let fold_function alg (FD_aux (FD_function (rec_opt, tannot_opt, effect_opt, funcls), annot)) =
+  FD_aux (FD_function (rec_opt, tannot_opt, effect_opt, List.map (fold_funcl alg) funcls), annot)
+
 let id_exp_alg =
   { e_block = (fun es -> E_block es)
   ; e_nondet = (fun es -> E_nondet es)
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 2acc1814..15e704df 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -189,6 +189,18 @@ val fold_pexp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_
       'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
       'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a pexp -> 'pexp
 
+val fold_pexp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
+      'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
+      'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a pexp -> 'pexp
+
+val fold_funcl : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
+      'opt_default_aux,'opt_default,'a pexp,'pexp_aux,'letbind_aux,'letbind,
+      'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a funcl -> 'a funcl
+
+val fold_function : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
+      'opt_default_aux,'opt_default, 'a pexp,'pexp_aux,'letbind_aux,'letbind,
+      'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a fundef -> 'a fundef
+
 val id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg
 val id_exp_alg :
   ('a,'a exp,'a exp_aux,'a lexp,'a lexp_aux,'a fexp,
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 8a1131e7..e818c0e2 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -3467,6 +3467,9 @@ let rewrite_defs_pat_lits rewrite_lit =
     let rewrite_pat = function
       (* HACK: ignore strings for now *)
       | P_lit (L_aux (L_string _, _)) as p_aux, p_annot -> P_aux (p_aux, p_annot)
+      (* Matching on unit is always the same as matching on wildcard *)
+      | P_lit (L_aux (L_unit, _) as lit), p_annot when rewrite_lit lit ->
+         P_aux (P_wild, p_annot)
       | P_lit lit, p_annot when rewrite_lit lit ->
          let env = env_of_annot p_annot in
          let typ = typ_of_annot p_annot in
@@ -3476,7 +3479,8 @@ let rewrite_defs_pat_lits rewrite_lit =
          guards := guard :: !guards;
          incr counter;
          P_aux (P_id id, p_annot)
-      | p_aux, p_annot -> P_aux (p_aux, p_annot)
+      | p_aux, p_annot ->
+         P_aux (p_aux, p_annot)
     in
 
     match pexp_aux with
@@ -3484,7 +3488,7 @@ let rewrite_defs_pat_lits rewrite_lit =
        begin
          let pat = fold_pat { id_pat_alg with p_aux = rewrite_pat } pat in
          match !guards with
-         | [] -> pexp
+         | [] -> Pat_aux (Pat_exp (pat, exp), annot)
          | (g :: gs) ->
             let guard_annot = (fst annot, mk_tannot (env_of exp) bool_typ no_effect) in
             Pat_aux (Pat_when (pat, List.fold_left (fun g g' -> E_aux (E_app (mk_id "and_bool", [g; g']), guard_annot)) g gs, exp), annot)
@@ -4632,7 +4636,7 @@ let rewrite_defs_c = [
   ("constraint", rewrite_constraint);
   ("trivial_sizeof", rewrite_trivial_sizeof);
   ("sizeof", rewrite_sizeof);
-  ("merge function clauses", merge_funcls);
+  ("merge_function_clauses", merge_funcls);
   ("recheck_defs", recheck_defs)
   ]