Work on E_constraint removal pass and diagnosing bugs in E_sizeof removal pass

6 files changed, 49 insertions, 4 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index ddd83429..ad14f0f1 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -50,6 +50,11 @@ let mk_nc nc_aux = NC_aux (nc_aux, Parse_ast.Unknown)
 
 let mk_nexp nexp_aux = Nexp_aux (nexp_aux, Parse_ast.Unknown)
 
+let mk_exp exp_aux = E_aux (exp_aux, (Parse_ast.Unknown, ()))
+let unaux_exp (E_aux (exp_aux, _)) = exp_aux
+
+let mk_lit lit_aux = L_aux (lit_aux, Parse_ast.Unknown)
+
 let rec map_exp_annot f (E_aux (exp, annot)) = E_aux (map_exp_annot_aux f exp, f annot)
 and map_exp_annot_aux f = function
   | E_block xs -> E_block (List.map (map_exp_annot f) xs)
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 94f3f0cc..b0ccb7b8 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -46,6 +46,10 @@ open Ast
 
 val mk_nc : n_constraint_aux -> n_constraint
 val mk_nexp : nexp_aux -> nexp
+val mk_exp : unit exp_aux -> unit exp
+val mk_lit : lit_aux -> lit
+
+val unaux_exp : 'a exp -> 'a exp_aux
 
 (* Functions to map over the annotations in sub-expressions *)
 val map_exp_annot : ('a annot -> 'b annot) -> 'a exp -> 'b exp
diff --git a/src/rewriter.ml b/src/rewriter.ml
index c7477e93..f0e2a811 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -1080,8 +1080,10 @@ let rewrite_sizeof (Defs defs) =
         (* Retrieve instantiation of the type variables of the called function
            for the given parameters in the original environment *)
         let inst = instantiation_of orig_exp in
+        Bindings.bindings param_map |> List.iter (fun (id, kids) -> print_endline (string_of_id id ^ " => " ^ Util.string_of_list ", " string_of_kid (KidSet.elements kids)));
+        KBindings.bindings inst |> List.iter (fun (kid, uvar) -> print_endline (string_of_kid kid ^ " => " ^ string_of_uvar uvar));
         let kid_exp kid = begin
-          match KBindings.find kid inst with
+          match (try KBindings.find kid inst with e -> print_endline (string_of_kid kid ^ " " ^ string_of_exp full_exp); raise e) with
           | U_nexp nexp -> E_aux (E_sizeof nexp, simple_annot l (atom_typ nexp))
           | _ ->
             raise (Reporting_basic.err_unreachable l
@@ -2281,12 +2283,39 @@ let rewrite_defs_early_return =
 
   rewrite_defs_base { rewriters_base with rewrite_fun = rewrite_fun_early_return }
 
+let rewrite_constraint =
+  let rec rewrite_nc (NC_aux (nc_aux, l)) = mk_exp (rewrite_nc_aux nc_aux)
+  and rewrite_nc_aux = function
+    | NC_bounded_ge (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id ">=", mk_exp (E_sizeof n2))
+    | NC_bounded_le (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id ">=", mk_exp (E_sizeof n2))
+    | NC_fixed (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id "==", mk_exp (E_sizeof n2))
+    | NC_not_equal (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id "!=", mk_exp (E_sizeof n2))
+    | NC_and (nc1, nc2) -> E_app_infix (rewrite_nc nc1, mk_id "&", rewrite_nc nc2)
+    | NC_or (nc1, nc2) -> E_app_infix (rewrite_nc nc1, mk_id "|", rewrite_nc nc2)
+    | NC_false -> E_lit (mk_lit L_true)
+    | NC_true -> E_lit (mk_lit L_false)
+    | NC_nat_set_bounded (kid, ints) ->
+        unaux_exp (rewrite_nc (List.fold_left (fun nc int -> nc_or nc (nc_eq (nvar kid) (nconstant int))) nc_true ints))
+  in
+  let rewrite_e_aux (E_aux (e_aux, _) as exp) =
+    match e_aux with
+    | E_constraint nc ->
+       check_exp (env_of exp) (rewrite_nc nc) bool_typ
+    | _ -> exp
+  in
+
+  let rewrite_e_constraint = { id_exp_alg with e_aux = (fun (exp, annot) -> rewrite_e_aux (E_aux (exp, annot))) } in
+
+  rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_e_constraint) }
+
 let rewrite_defs_ocaml = [
   top_sort_defs;
   rewrite_defs_remove_vector_concat;
+  rewrite_constraint;
   rewrite_sizeof;
-  rewrite_defs_exp_lift_assign (* ;
-  rewrite_defs_separate_numbs *)
+  (*
+  (* rewrite_defs_exp_lift_assign (* ;
+  rewrite_defs_separate_numbs *) *) *)
   ]
 
 let rewrite_defs_remove_blocks =
diff --git a/src/sail.ml b/src/sail.ml
index cf366d42..dbc0eff4 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -158,6 +158,7 @@ let main() =
        else ());
       (if !(opt_print_ocaml)
        then let ast_ocaml = rewrite_ast_ocaml ast in
+         print_endline "Finished re-writing ocaml";
          if !(opt_libs_ocaml) = []
          then output "" (Ocaml_out None) [out_name,ast_ocaml]
          else output "" (Ocaml_out (Some (List.hd !opt_libs_ocaml))) [out_name,ast_ocaml]
diff --git a/src/type_check.ml b/src/type_check.ml
index ec0b4a58..da3ffec6 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -99,6 +99,10 @@ let mk_ord ord_aux = Ord_aux (ord_aux, Parse_ast.Unknown)
 
 let rec nexp_simp (Nexp_aux (nexp, l)) = Nexp_aux (nexp_simp_aux nexp, l)
 and nexp_simp_aux = function
+  | Nexp_minus (Nexp_aux (Nexp_sum (Nexp_aux (n1, _), Nexp_aux (Nexp_constant c1, _)), _), Nexp_aux (Nexp_constant c2, _)) when c1 = c2 ->
+     nexp_simp_aux n1
+  | Nexp_sum (Nexp_aux (Nexp_minus (Nexp_aux (n1, _), Nexp_aux (Nexp_constant c1, _)), _), Nexp_aux (Nexp_constant c2, _)) when c1 = c2 ->
+     nexp_simp_aux n1
   | Nexp_sum (n1, n2) ->
      begin
        let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in
@@ -1464,7 +1468,7 @@ let rec unify l env typ1 typ2 =
     | Typ_arg_nexp n1, Typ_arg_nexp n2 ->
        begin
          match unify_nexps l env goals (nexp_simp n1) (nexp_simp n2) with
-         | Some (kid, unifier) -> KBindings.singleton kid (U_nexp unifier)
+         | Some (kid, unifier) -> KBindings.singleton kid (U_nexp (nexp_simp unifier))
          | None -> KBindings.empty
        end
     | Typ_arg_typ typ1, Typ_arg_typ typ2 -> unify_typ l typ1 typ2
diff --git a/src/type_check.mli b/src/type_check.mli
index d451e4d9..c9069a6f 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -250,6 +250,8 @@ type uvar =
   | U_effect of effect
   | U_typ of typ
 
+val string_of_uvar : uvar -> string
+
 (* Throws Invalid_argument if the argument is not a E_app expression *)
 val instantiation_of : tannot exp -> uvar KBindings.t