From 5bfbb47591e46139c10ff3e674731de6061ec872 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 24 Aug 2018 18:22:12 +0100
Subject: 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
---
 src/rewriter.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'src/rewriter.ml')

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)
-- 
cgit v1.2.3