Merge branch 'sail2' into smt_experiments

1 files changed, 115 insertions, 19 deletions

diff --git a/src/rewrites.ml b/src/rewrites.ml
index 2138207b..7ff500b9 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -1772,7 +1772,7 @@ let rewrite_split_fun_ctor_pats fun_name env (Defs defs) =
       in
       let val_spec =
         VS_aux (VS_val_spec
-          (mk_typschm (mk_typquant quants) fun_typ, id, (fun _ -> None), false),
+          (mk_typschm (mk_typquant quants) fun_typ, id, [], false),
           (Parse_ast.Unknown, empty_tannot))
       in
       let fundef = FD_aux (FD_function (r_o, t_o, e_o, funcls), fdannot) in
@@ -2153,6 +2153,10 @@ let rewrite_simple_assignments env defs =
   let assign_e_aux e_aux annot =
     let env = env_of_annot annot in
     match e_aux with
+    | E_assign (LEXP_aux (LEXP_id _, _), _) ->
+       E_aux (e_aux, annot)
+    | E_assign (LEXP_aux (LEXP_cast (_, _), _), _) ->
+       E_aux (e_aux, annot)
     | E_assign (lexp, exp) ->
        let (lexp, rhs) = rewrite_lexp_to_rhs lexp in
        let assign = mk_exp (E_assign (strip_lexp lexp, strip_exp (rhs exp))) in
@@ -2369,10 +2373,15 @@ let rewrite_defs_letbind_effects env =
        n_exp_name by (fun by ->
        let body = n_exp_term (effectful body) body in
        k (rewrap (E_for (id,start,stop,by,dir,body))))))
-    | E_loop (loop, cond, body) ->
+    | E_loop (loop, measure, cond, body) ->
+       let measure = match measure with
+         | Measure_aux (Measure_none,_) -> measure
+         | Measure_aux (Measure_some exp,l) ->
+            Measure_aux (Measure_some (n_exp_term false exp),l)
+       in
        let cond = n_exp_term (effectful cond) cond in
        let body = n_exp_term (effectful body) body in
-       k (rewrap (E_loop (loop,cond,body)))
+       k (rewrap (E_loop (loop,measure,cond,body)))
     | E_vector exps ->
        n_exp_nameL exps (fun exps ->
        k (rewrap (E_vector exps)))
@@ -2718,7 +2727,7 @@ let construct_toplevel_string_append_func env f_id pat =
                                                           ), unk)]
   in
   let fun_typ = (mk_typ (Typ_fn ([string_typ], option_typ, no_effect))) in
-  let new_val_spec = VS_aux (VS_val_spec (mk_typschm (TypQ_aux (TypQ_no_forall, unk)) fun_typ, f_id, (fun _ -> None), false), unkt) in
+  let new_val_spec = VS_aux (VS_val_spec (mk_typschm (TypQ_aux (TypQ_no_forall, unk)) fun_typ, f_id, [], false), unkt) in
   let new_val_spec, env = Type_check.check_val_spec env new_val_spec in
   let non_rec = (Rec_aux (Rec_nonrec, Parse_ast.Unknown)) in
   let no_tannot = (Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown)) in
@@ -3448,7 +3457,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
              el env (typ_of exp4))))
            el env (typ_of exp4)) in
        Added_vars (v, tuple_pat (if overwrite then varpats else pat :: varpats))
-     | E_loop(loop,cond,body) ->
+     | E_loop(loop,Measure_aux (measure,_),cond,body) ->
         (* Find variables that might be updated in the loop body and are used
            either after or within the loop. *)
         let vars, varpats =
@@ -3458,11 +3467,14 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
         in
         let body = rewrite_var_updates (add_vars overwrite body vars) in
         let (E_aux (_,(_,bannot))) = body in
-        let fname = match loop with
-          | While -> "while#"
-          | Until -> "until#" in
+        let fname, measure = match loop, measure with
+          | While, Measure_none -> "while#", []
+          | Until, Measure_none -> "until#", []
+          | While, Measure_some exp -> "while#t", [exp]
+          | Until, Measure_some exp -> "until#t", [exp]
+        in
         let funcl = Id_aux (Id fname,gen_loc el) in
-        let v = E_aux (E_app (funcl,[cond;tuple_exp vars;body]), (gen_loc el, bannot)) in
+        let v = E_aux (E_app (funcl,[cond;tuple_exp vars;body]@measure), (gen_loc el, bannot)) in
         Added_vars (v, tuple_pat (if overwrite then varpats else pat :: varpats))
     | E_if (c,e1,e2) ->
        let vars, varpats =
@@ -3763,8 +3775,10 @@ let rewrite_defs_remove_e_assign env (Defs defs) =
   let (Defs loop_specs) = fst (Type_error.check Env.empty (Defs (List.map gen_vs
     [("foreach#", "forall ('vars : Type). (int, int, int, bool, 'vars, 'vars) -> 'vars");
      ("while#", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars");
-     ("until#", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars")]))) in
-  let rewrite_exp _ e =
+     ("until#", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars");
+     ("while#t", "forall ('vars : Type). (bool, 'vars, 'vars, int) -> 'vars");
+     ("until#t", "forall ('vars : Type). (bool, 'vars, 'vars, int) -> 'vars")]))) in
+ let rewrite_exp _ e =
     replace_memwrite_e_assign (remove_reference_types (rewrite_var_updates e)) in
   rewrite_defs_base
     { rewrite_exp = rewrite_exp
@@ -3971,10 +3985,10 @@ let rewrite_defs_realise_mappings _ (Defs defs) =
     let backwards_typ = Typ_aux (Typ_fn ([typ2], typ1, no_effect), l) in
     let backwards_matches_typ = Typ_aux (Typ_fn ([typ2], bool_typ, no_effect), l) in
 
-    let forwards_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_typ, forwards_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
-    let backwards_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_typ, backwards_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
-    let forwards_matches_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_matches_typ, forwards_matches_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
-    let backwards_matches_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_matches_typ, backwards_matches_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
+    let forwards_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_typ, forwards_id, [], false), (Parse_ast.Unknown,())) in
+    let backwards_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_typ, backwards_id, [], false), (Parse_ast.Unknown,())) in
+    let forwards_matches_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_matches_typ, forwards_matches_id, [], false), (Parse_ast.Unknown,())) in
+    let backwards_matches_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_matches_typ, backwards_matches_id, [], false), (Parse_ast.Unknown,())) in
 
     let forwards_spec, env = Type_check.check_val_spec env forwards_spec in
     let backwards_spec, env = Type_check.check_val_spec env backwards_spec in
@@ -4008,7 +4022,7 @@ let rewrite_defs_realise_mappings _ (Defs defs) =
     let string_defs =
       begin if subtype_check env typ1 string_typ && subtype_check env string_typ typ1 then
               let forwards_prefix_typ = Typ_aux (Typ_fn ([typ1], app_typ (mk_id "option") [A_aux (A_typ (tuple_typ [typ2; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
-              let forwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_prefix_typ, prefix_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
+              let forwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_prefix_typ, prefix_id, [], false), (Parse_ast.Unknown,())) in
               let forwards_prefix_spec, env = Type_check.check_val_spec env forwards_prefix_spec in
               let forwards_prefix_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl true prefix_id) mapcls) |> List.flatten) @ [prefix_wildcard])) in
               let forwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_none, [mk_funcl prefix_id arg_pat forwards_prefix_match]), (l, ()))) in
@@ -4018,7 +4032,7 @@ let rewrite_defs_realise_mappings _ (Defs defs) =
             else
               if subtype_check env typ2 string_typ && subtype_check env string_typ typ2 then
                 let backwards_prefix_typ = Typ_aux (Typ_fn ([typ2], app_typ (mk_id "option") [A_aux (A_typ (tuple_typ [typ1; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
-                let backwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_prefix_typ, prefix_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
+                let backwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_prefix_typ, prefix_id, [], false), (Parse_ast.Unknown,())) in
                 let backwards_prefix_spec, env = Type_check.check_val_spec env backwards_prefix_spec in
                 let backwards_prefix_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl false prefix_id) mapcls) |> List.flatten) @ [prefix_wildcard])) in
                 let backwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_none, [mk_funcl prefix_id arg_pat backwards_prefix_match]), (l, ()))) in
@@ -4438,6 +4452,7 @@ let minimise_recursive_functions env (Defs defs) =
     | d -> d
   in Defs (List.map rewrite_def defs)
 
+(* Move recursive function termination measures into the function definitions. *)
 let move_termination_measures env (Defs defs) =
   let scan_for id defs =
     let rec aux = function
@@ -4568,15 +4583,16 @@ let rewrite_explicit_measure env (Defs defs) =
              | _, P_aux (P_tup ps,_) -> ps
              | _, _ -> [measure_pat]
            in
-           let mk_wrap i (P_aux (p,(l,_))) =
+           let mk_wrap i (P_aux (p,(l,_)) as p_full) =
              let id =
                match p with
                | P_id id
                | P_typ (_,(P_aux (P_id id,_))) -> id
+               | P_lit _
                | P_wild
                | P_typ (_,(P_aux (P_wild,_))) ->
                   mk_id ("_arg" ^ string_of_int i)
-               | _ -> raise (Reporting.err_todo l "Measure patterns can only be identifiers or wildcards")
+               | _ -> raise (Reporting.err_todo l ("Measure patterns can only be identifiers or wildcards, not " ^ string_of_pat p_full))
              in
              P_aux (P_id id,(loc,empty_tannot)),
              E_aux (E_id id,(loc,empty_tannot))
@@ -4614,6 +4630,29 @@ let rewrite_explicit_measure env (Defs defs) =
   in
   Defs (List.flatten (List.map rewrite_def defs))
 
+(* Add a dummy assert to loops for backends that require loops to be able to
+   fail.  Note that the Coq backend will spot the assert and omit it. *)
+let rewrite_loops_with_escape_effect env defs =
+  let dummy_ann = Parse_ast.Unknown,empty_tannot in
+  let assert_exp =
+    E_aux (E_assert (E_aux (E_lit (L_aux (L_true,Unknown)),dummy_ann),
+                     E_aux (E_lit (L_aux (L_string "loop dummy assert",Unknown)),dummy_ann)),
+           dummy_ann)
+  in
+  let rewrite_exp rws exp =
+    let (E_aux (e,ann) as exp) = Rewriter.rewrite_exp rws exp in
+    match e with
+    | E_loop (l,(Measure_aux (Measure_some _,_) as m),guard,body) ->
+       if has_effect (effect_of exp) BE_escape then exp else
+       let body = match body with
+         | E_aux (E_block es,ann) ->
+            E_aux (E_block (assert_exp::es),ann)
+         | _ -> E_aux (E_block [assert_exp;body],dummy_ann)
+       in E_aux (E_loop (l,m,guard,body),ann)
+    | _ -> exp
+  in
+  rewrite_defs_base { rewriters_base with rewrite_exp } defs
+
 let recheck_defs env defs = fst (Type_error.check initial_env defs)
 let recheck_defs_without_effects env defs =
   let old = !opt_no_effects in
@@ -4631,6 +4670,59 @@ let remove_mapping_valspecs env (Defs defs) =
   Defs (List.filter allowed_def defs)
 
 
+(* Move loop termination measures into loop AST nodes.  This is used before
+   type checking so that we avoid the complexity of type checking separate
+   measures. *)
+let rec move_loop_measures (Defs defs) =
+  let loop_measures =
+    List.fold_left
+      (fun m d ->
+        match d with
+        | DEF_loop_measures (id, measures) ->
+           (* Allow multiple measure definitions, concatenating them *)
+           Bindings.add id
+             (match Bindings.find_opt id m with
+              | None -> measures
+              | Some m -> m @ measures)
+             m
+        | _ -> m) Bindings.empty defs
+  in
+  let do_exp exp_rec measures (E_aux (e,ann) as exp) =
+    match e, measures with
+    | E_loop (loop, _, e1, e2), (Loop (loop',exp))::t when loop = loop' ->
+       let t,e1 = exp_rec t e1 in
+       let t,e2 = exp_rec t e2 in
+       t,E_aux (E_loop (loop, Measure_aux (Measure_some exp, exp_loc exp), e1, e2),ann)
+    | _ -> exp_rec measures exp
+  in
+  let do_funcl (m,acc) (FCL_aux (FCL_Funcl (id, pexp),ann) as fcl) =
+    match Bindings.find_opt id m with
+    | Some measures ->
+       let measures,pexp = foldin_pexp do_exp measures pexp in
+       Bindings.add id measures m, (FCL_aux (FCL_Funcl (id, pexp),ann))::acc
+    | None -> m, fcl::acc
+  in
+  let unused,rev_defs =
+    List.fold_left
+      (fun (m,acc) d ->
+        match d with
+        | DEF_loop_measures _ -> m, acc
+        | DEF_fundef (FD_aux (FD_function (r,t,e,fcls),ann)) ->
+            let m,rfcls = List.fold_left do_funcl (m,[]) fcls in
+            m, (DEF_fundef (FD_aux (FD_function (r,t,e,List.rev rfcls),ann)))::acc
+        | _ -> m, d::acc)
+      (loop_measures,[]) defs
+  in let () = Bindings.iter
+                (fun id -> function
+                  | [] -> ()
+                  | _::_ ->
+                     Reporting.print_err (id_loc id) "Warning"
+                       ("unused loop measure for function " ^ string_of_id id))
+                unused
+  in Defs (List.rev rev_defs)
+
+
+
 let opt_mono_rewrites = ref false
 let opt_mono_complex_nexps = ref true
 
@@ -4750,6 +4842,7 @@ let all_rewrites = [
     ("minimise_recursive_functions", Basic_rewriter minimise_recursive_functions);
     ("move_termination_measures", Basic_rewriter move_termination_measures);
     ("rewrite_explicit_measure", Basic_rewriter rewrite_explicit_measure);
+    ("rewrite_loops_with_escape_effect", Basic_rewriter rewrite_loops_with_escape_effect);
     ("simple_types", Basic_rewriter rewrite_simple_types);
     ("overload_cast", Basic_rewriter rewrite_overload_cast);
     ("top_sort_defs", Basic_rewriter (fun _ -> top_sort_defs));
@@ -4844,6 +4937,7 @@ let rewrites_coq = [
     ("recheck_defs_without_effects", []);
     ("make_cases_exhaustive", []);
     ("rewrite_explicit_measure", []);
+    ("rewrite_loops_with_escape_effect", []);
     ("recheck_defs_without_effects", []);
     ("fix_val_specs", []);
     ("remove_blocks", []);
@@ -4927,6 +5021,8 @@ let rewrites_target tgt =
   | "sail" -> []
   | "latex" -> []
   | "interpreter" -> rewrites_interpreter
+  | "tofrominterp" -> rewrites_interpreter
+  | "marshal" -> rewrites_interpreter
   | _ ->
      raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ ("Invalid target for rewriting: " ^ tgt))