Basic loop termination measures for Coq

Currently only supports pure termination measures for loops with effects.

The user syntax uses separate termination measure declarations, as in the
previous recursive termination measures, which are rewritten into the
loop AST nodes before type checking (because it would be rather difficult
to calculate the correct environment to type check the separate declaration
in).

1 files changed, 224 insertions, 11 deletions

diff --git a/src/rewriter.ml b/src/rewriter.ml
index edf0d4a5..2573a135 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -151,7 +151,7 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match destruct_tannot (snd annot)
       union_effects (fun_app_effects f env) (union_eff_exps [e1;e2])
     | E_if (e1,e2,e3) -> union_eff_exps [e1;e2;e3]
     | E_for (_,e1,e2,e3,_,e4) -> union_eff_exps [e1;e2;e3;e4]
-    | E_loop (_,e1,e2) -> union_eff_exps [e1;e2]
+    | E_loop (_,_,e1,e2) -> union_eff_exps [e1;e2]
     | E_vector es -> union_eff_exps es
     | E_vector_access (e1,e2) -> union_eff_exps [e1;e2]
     | E_vector_subrange (e1,e2,e3) -> union_eff_exps [e1;e2;e3]
@@ -280,8 +280,12 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot)) as orig_exp) =
   | E_if (c,t,e) -> rewrap (E_if (rewrite c,rewrite t, rewrite e))
   | E_for (id, e1, e2, e3, o, body) ->
     rewrap (E_for (id, rewrite e1, rewrite e2, rewrite e3, o, rewrite body))
-  | E_loop (loop, e1, e2) ->
-    rewrap (E_loop (loop, rewrite e1, rewrite e2))
+  | E_loop (loop, m, e1, e2) ->
+     let m = match m with
+       | Measure_aux (Measure_none,_) -> m
+       | Measure_aux (Measure_some exp,l) -> Measure_aux (Measure_some (rewrite exp),l)
+     in
+    rewrap (E_loop (loop, m, rewrite e1, rewrite e2))
   | E_vector exps -> rewrap (E_vector (List.map rewrite exps))
   | E_vector_access (vec,index) -> rewrap (E_vector_access (rewrite vec,rewrite index))
   | E_vector_subrange (vec,i1,i2) ->
@@ -362,8 +366,9 @@ let rewrite_def rewriters d = match d with
   | DEF_internal_mutrec fdefs -> DEF_internal_mutrec (List.map (rewriters.rewrite_fun rewriters) fdefs)
   | DEF_val letbind -> DEF_val (rewriters.rewrite_let rewriters letbind)
   | DEF_pragma (pragma, arg, l) -> DEF_pragma (pragma, arg, l)
-  | DEF_scattered _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "DEF_scattered survived to rewritter")
+  | DEF_scattered _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "DEF_scattered survived to rewriter")
   | DEF_measure (id,pat,exp) -> DEF_measure (id,rewriters.rewrite_pat rewriters pat, rewriters.rewrite_exp rewriters exp)
+  | DEF_loop_measures (id,_) -> raise (Reporting.err_unreachable (id_loc id) __POS__ "DEF_loop_measures survived to rewriter")
 
 let rewrite_defs_base rewriters (Defs defs) =
   let rec rewrite ds = match ds with
@@ -539,7 +544,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
   ; e_tuple                  : 'exp list -> 'exp_aux
   ; e_if                     : 'exp * 'exp * 'exp -> 'exp_aux
   ; e_for                    : id * 'exp * 'exp * 'exp * Ast.order * 'exp -> 'exp_aux
-  ; e_loop                   : loop * 'exp * 'exp -> 'exp_aux
+  ; e_loop                   : loop * ('exp option * Parse_ast.l) * 'exp * 'exp -> 'exp_aux
   ; e_vector                 : 'exp list -> 'exp_aux
   ; e_vector_access          : 'exp * 'exp -> 'exp_aux
   ; e_vector_subrange        : 'exp * 'exp * 'exp -> 'exp_aux
@@ -602,8 +607,12 @@ let rec fold_exp_aux alg = function
   | E_if (e1,e2,e3) -> alg.e_if (fold_exp alg e1, fold_exp alg e2, fold_exp alg e3)
   | E_for (id,e1,e2,e3,order,e4) ->
      alg.e_for (id,fold_exp alg e1, fold_exp alg e2, fold_exp alg e3, order, fold_exp alg e4)
-  | E_loop (loop_type, e1, e2) ->
-     alg.e_loop (loop_type, fold_exp alg e1, fold_exp alg e2)
+  | E_loop (loop_type, m, e1, e2) ->
+     let m = match m with
+       | Measure_aux (Measure_none,l) -> None,l
+       | Measure_aux (Measure_some exp,l) -> Some (fold_exp alg exp),l
+     in
+     alg.e_loop (loop_type, m, fold_exp alg e1, fold_exp alg e2)
   | E_vector es -> alg.e_vector (List.map (fold_exp alg) es)
   | E_vector_access (e1,e2) -> alg.e_vector_access (fold_exp alg e1, fold_exp alg e2)
   | E_vector_subrange (e1,e2,e3) ->
@@ -681,7 +690,9 @@ let id_exp_alg =
   ; e_tuple = (fun es -> E_tuple es)
   ; e_if = (fun (e1,e2,e3) -> E_if (e1,e2,e3))
   ; e_for = (fun (id,e1,e2,e3,order,e4) -> E_for (id,e1,e2,e3,order,e4))
-  ; e_loop = (fun (lt, e1, e2) -> E_loop (lt, e1, e2))
+  ; e_loop = (fun (lt, (m,l), e1, e2) ->
+    let m = match m with None -> Measure_none | Some e -> Measure_some e in
+    E_loop (lt, Measure_aux (m,l), e1, e2))
   ; e_vector = (fun es -> E_vector es)
   ; e_vector_access = (fun (e1,e2) -> E_vector_access (e1,e2))
   ; e_vector_subrange =  (fun (e1,e2,e3) -> E_vector_subrange (e1,e2,e3))
@@ -776,8 +787,12 @@ let compute_exp_alg bot join =
   ; e_if = (fun ((v1,e1),(v2,e2),(v3,e3)) -> (join_list [v1;v2;v3], E_if (e1,e2,e3)))
   ; e_for = (fun (id,(v1,e1),(v2,e2),(v3,e3),order,(v4,e4)) ->
     (join_list [v1;v2;v3;v4], E_for (id,e1,e2,e3,order,e4)))
-  ; e_loop = (fun (lt, (v1, e1), (v2, e2)) ->
-    (join_list [v1;v2], E_loop (lt, e1, e2)))
+  ; e_loop = (fun (lt, (m,l), (v1, e1), (v2, e2)) ->
+    let vs,m = match m with
+    | None -> [], Measure_none
+    | Some (v,e) -> [v], Measure_some e
+    in
+    (join_list (vs@[v1;v2]), E_loop (lt, Measure_aux (m,l), e1, e2)))
   ; e_vector = split_join (fun es -> E_vector es)
   ; e_vector_access = (fun ((v1,e1),(v2,e2)) -> (join v1 v2, E_vector_access (e1,e2)))
   ; e_vector_subrange =  (fun ((v1,e1),(v2,e2),(v3,e3)) -> (join_list [v1;v2;v3], E_vector_subrange (e1,e2,e3)))
@@ -878,7 +893,8 @@ let pure_exp_alg bot join =
   ; e_tuple = join_list
   ; e_if = (fun (v1,v2,v3) -> join_list [v1;v2;v3])
   ; e_for = (fun (id,v1,v2,v3,order,v4) -> join_list [v1;v2;v3;v4])
-  ; e_loop = (fun (lt, v1, v2) -> join v1 v2)
+  ; e_loop = (fun (lt, (m,_), v1, v2) ->
+    let v = join v1 v2 in match m with None -> v | Some v' -> join v v')
   ; e_vector = join_list
   ; e_vector_access = (fun (v1,v2) -> join v1 v2)
   ; e_vector_subrange =  (fun (v1,v2,v3) -> join_list [v1;v2;v3])
@@ -927,3 +943,200 @@ let pure_exp_alg bot join =
   ; lB_aux = (fun (vl,annot) -> vl)
   ; pat_alg = pure_pat_alg bot join
   }
+
+let default_fold_fexp f x (FE_aux (FE_Fexp (id,e),annot)) =
+  let x,e = f x e in
+  x, FE_aux (FE_Fexp (id,e),annot)
+
+let default_fold_pexp f x (Pat_aux (pe,ann)) =
+  let x,pe = match pe with
+  | Pat_exp (p,e) ->
+     let x,e = f x e in
+     x,Pat_exp (p,e)
+  | Pat_when (p,e1,e2) ->
+     let x,e1 = f x e1 in
+     let x,e2 = f x e2 in
+     x,Pat_when (p,e1,e2)
+  in x, Pat_aux (pe,ann)
+
+let default_fold_letbind f x (LB_aux (LB_val (p,e),ann)) =
+  let x,e = f x e in
+  x, LB_aux (LB_val (p,e),ann)
+
+let rec default_fold_lexp f x (LEXP_aux (le,ann) as lexp) =
+  let re le = LEXP_aux (le,ann) in
+  match le with
+  | LEXP_id _
+  | LEXP_cast _
+    -> x, lexp
+  | LEXP_deref e ->
+     let x, e = f x e in
+     x, re (LEXP_deref e)
+  | LEXP_memory (id,es) ->
+     let x,es = List.fold_left (fun (x,es) e ->
+                    let x,e' = f x e in x,e'::es) (x,[]) es in
+     x, re (LEXP_memory (id, List.rev es))
+  | LEXP_tup les ->
+     let x,les = List.fold_left (fun (x,les) le ->
+                    let x,le' = default_fold_lexp f x le in x,le'::les) (x,[]) les in
+     x, re (LEXP_tup (List.rev les))
+  | LEXP_vector_concat les ->
+     let x,les = List.fold_left (fun (x,les) le ->
+                    let x,le' = default_fold_lexp f x le in x,le'::les) (x,[]) les in
+     x, re (LEXP_vector_concat (List.rev les))
+  | LEXP_vector (le,e) ->
+     let x, le = default_fold_lexp f x le in
+     let x, e = f x e in
+     x, re (LEXP_vector (le,e))
+  | LEXP_vector_range (le,e1,e2) ->
+     let x, le = default_fold_lexp f x le in
+     let x, e1 = f x e1 in
+     let x, e2 = f x e2 in
+     x, re (LEXP_vector_range (le,e1,e2))
+  | LEXP_field (le,id) ->
+     let x, le = default_fold_lexp f x le in
+     x, re (LEXP_field (le,id))
+
+let default_fold_exp f x (E_aux (e,ann) as exp) =
+  let re e = E_aux (e,ann) in
+  match e with
+  | E_block es ->
+     let x,es = List.fold_left (fun (x,es) e ->
+                    let x,e' = f x e in x,e'::es) (x,[]) es in
+     x, re (E_block (List.rev es))
+  | E_nondet es ->
+     let x,es = List.fold_left (fun (x,es) e ->
+                    let x,e' = f x e in x,e'::es) (x,[]) es in
+     x, re (E_nondet (List.rev es))
+  | E_id _
+  | E_ref _
+  | E_lit _ -> x, exp
+  | E_cast (typ,e) ->
+     let x,e = f x e in
+     x, re (E_cast (typ,e))
+  | E_app (id,es) ->
+     let x,es = List.fold_left (fun (x,es) e ->
+                    let x,e' = f x e in x,e'::es) (x,[]) es in
+     x, re (E_app (id, List.rev es))
+  | E_app_infix (e1,id,e2) ->
+     let x,e1 = f x e1 in
+     let x,e2 = f x e2 in
+     x, re (E_app_infix (e1,id,e2))
+  | E_tuple es ->
+     let x,es = List.fold_left (fun (x,es) e ->
+                    let x,e' = f x e in x,e'::es) (x,[]) es in
+     x, re (E_tuple (List.rev es))
+  | E_if (e1,e2,e3) ->
+     let x,e1 = f x e1 in
+     let x,e2 = f x e2 in
+     let x,e3 = f x e3 in
+     x, re (E_if (e1,e2,e3))
+  | E_for (id,e1,e2,e3,order,e4) ->
+     let x,e1 = f x e1 in
+     let x,e2 = f x e2 in
+     let x,e3 = f x e3 in
+     let x,e4 = f x e4 in
+     x, re (E_for (id,e1,e2,e3,order,e4))
+  | E_loop (loop_type, m, e1, e2) ->
+     let x,m = match m with
+       | Measure_aux (Measure_none,_) -> x,m
+       | Measure_aux (Measure_some exp,l) ->
+          let x, exp = f x exp in
+          x, Measure_aux (Measure_some exp,l)
+     in
+     let x,e1 = f x e1 in
+     let x,e2 = f x e2 in
+     x, re (E_loop (loop_type, m, e1, e2))
+  | E_vector es ->
+     let x,es = List.fold_left (fun (x,es) e ->
+                    let x,e' = f x e in x,e'::es) (x,[]) es in
+     x, re (E_vector (List.rev es))
+  | E_vector_access (e1,e2) ->
+     let x,e1 = f x e1 in
+     let x,e2 = f x e2 in
+     x, re (E_vector_access (e1,e2))
+  | E_vector_subrange (e1,e2,e3) ->
+     let x,e1 = f x e1 in
+     let x,e2 = f x e2 in
+     let x,e3 = f x e3 in
+     x, re (E_vector_subrange (e1,e2,e3))
+  | E_vector_update (e1,e2,e3) ->
+     let x,e1 = f x e1 in
+     let x,e2 = f x e2 in
+     let x,e3 = f x e3 in
+     x, re (E_vector_update (e1,e2,e3))
+  | E_vector_update_subrange (e1,e2,e3,e4) ->
+     let x,e1 = f x e1 in
+     let x,e2 = f x e2 in
+     let x,e3 = f x e3 in
+     let x,e4 = f x e4 in
+     x, re (E_vector_update_subrange (e1,e2,e3,e4))
+  | E_vector_append (e1,e2) ->
+     let x,e1 = f x e1 in
+     let x,e2 = f x e2 in
+     x, re (E_vector_append (e1,e2))
+  | E_list es ->
+     let x,es = List.fold_left (fun (x,es) e ->
+                    let x,e' = f x e in x,e'::es) (x,[]) es in
+     x, re (E_list (List.rev es))
+  | E_cons (e1,e2) ->
+     let x,e1 = f x e1 in
+     let x,e2 = f x e2 in
+     x, re (E_cons (e1,e2))
+  | E_record fexps ->
+     let x,fexps = List.fold_left (fun (x,fes) fe ->
+                       let x,fe' = default_fold_fexp f x fe in x,fe'::fes) (x,[]) fexps in
+     x, re (E_record (List.rev fexps))
+  | E_record_update (e,fexps) ->
+     let x,e = f x e in
+     let x,fexps = List.fold_left (fun (x,fes) fe ->
+                       let x,fe' = default_fold_fexp f x fe in x,fe'::fes) (x,[]) fexps in
+     x, re (E_record_update (e, List.rev fexps))
+  | E_field (e,id) ->
+     let x,e = f x e in x, re (E_field (e,id))
+  | E_case (e,pexps) ->
+     let x,e = f x e in
+     let x,pexps = List.fold_left (fun (x,pes) pe ->
+                       let x,pe' = default_fold_pexp f x pe in x,pe'::pes) (x,[]) pexps in
+     x, re (E_case (e, List.rev pexps))
+  | E_try (e,pexps) ->
+     let x,e = f x e in
+     let x,pexps = List.fold_left (fun (x,pes) pe ->
+                       let x,pe' = default_fold_pexp f x pe in x,pe'::pes) (x,[]) pexps in
+     x, re (E_try (e, List.rev pexps))
+  | E_let (letbind,e) ->
+     let x,letbind = default_fold_letbind f x letbind in
+     let x,e = f x e in
+     x, re (E_let (letbind,e))
+  | E_assign (lexp,e) ->
+     let x,lexp = default_fold_lexp f x lexp in
+     let x,e = f x e in
+     x, re (E_assign (lexp,e))
+  | E_sizeof _
+  | E_constraint _
+    -> x,exp
+  | E_exit e ->
+     let x,e = f x e in x, re (E_exit e)
+  | E_throw e ->
+     let x,e = f x e in x, re (E_throw e)
+  | E_return e ->
+     let x,e = f x e in x, re (E_return e)
+  | E_assert(e1,e2) ->
+     let x,e1 = f x e1 in
+     let x,e2 = f x e2 in
+     x, re (E_assert (e1,e2))
+  | E_var (lexp,e1,e2) ->
+     let x,lexp = default_fold_lexp f x lexp in
+     let x,e1 = f x e1 in
+     let x,e2 = f x e2 in
+     x, re (E_var (lexp,e1,e2))
+  | E_internal_plet (pat,e1,e2) ->
+     let x,e1 = f x e1 in
+     let x,e2 = f x e2 in
+     x, re (E_internal_plet (pat,e1,e2))
+  | E_internal_return e ->
+     let x,e = f x e in x, re (E_internal_return e)
+  | E_internal_value _ -> x,exp
+
+let rec foldin_exp f x e = f (default_fold_exp (foldin_exp f)) x e
+let rec foldin_pexp f x e = default_fold_pexp (foldin_exp f) x e