[WIP] Use MoCHi as back-end

.gitignore

@@ -27,3 +27,4 @@ paper/related_work.tex
 paper/semantics.tex
 paper/typesystem.tex
 paper/wf_rules.tex
+src/test/to_mochi.ml

src/argOptions.ml

@@ -12,11 +12,13 @@ module ExecMode = struct
     | Consort
     | Ownership
     | Typecheck
+    | ConvMoCHi
 
   let pairs = [
     ("consort", Consort);
     ("ownership", Ownership);
-    ("typecheck", Typecheck)
+    ("typecheck", Typecheck);
+    ("convmochi", ConvMoCHi)
   ]
   let default = "consort"
   let candidates = List.map (fun (s, _) -> s) pairs
@@ -69,6 +71,7 @@ type t = {
   file_list : Arg.usage_msg list;
   output_channel : out_channel Cache.t;
   intrinsics : Intrinsics.interp_t Cache.t;
+  ownership_arity : int;
 }
 
 let default = {
@@ -95,6 +98,7 @@ let default = {
   file_list = [];
   output_channel = ref None;
   intrinsics = ref None;
+  ownership_arity = 2;
 }
 let close_output ~opts =
   Option.iter close_out !(opts.output_channel);
@@ -132,6 +136,7 @@ let parse anon_fun usage_msg =
   let cfa = ref default.cfa in
   let intrinsics_file = ref None in
   let file_list = ref default.file_list in
+  let ownership_arity = ref default.ownership_arity in
   let show_all () =
     List.iter (fun r -> r := true) show_all_flags; Log.all () in
   let debug s =
@@ -191,6 +196,8 @@ let parse anon_fun usage_msg =
      "<file>\t Load definitions of standard operations from <file>");
     ("-files", Rest (fun s -> file_list := s::!file_list),
      "<file> ...\t Interpret all remaining arguments as files to test");
+    ("-ownership-arity", Set_int ownership_arity,
+     "<integer>\t The number of different ownership variables used in recursive data structure (default: 2)");
   ] in
   Arg.parse spec anon_fun usage_msg;
   {
@@ -217,4 +224,5 @@ let parse anon_fun usage_msg =
     file_list = !file_list;
     output_channel = default.output_channel;
     intrinsics = default.intrinsics;
+    ownership_arity = !ownership_arity;
   }

src/ast.ml

@@ -28,7 +28,9 @@ type lhs =
   | Nondet of RefinementTypes.concr_refinement option
   | Read of string * string
   | LengthOf of string
-  | Null [@@deriving sexp]
+  | Null
+  | Nil
+  | Cons of lhs * lhs [@@deriving sexp]
 
 type patt =
   | PVar of string
@@ -64,7 +66,8 @@ type raw_exp =
   | Let of patt * lhs * exp
   | Alias of Paths.concr_ap * Paths.concr_ap * exp
   | Assert of relation * exp
-  | Return of string [@@deriving sexp]
+  | Return of string
+  | Match of lhs * exp * string * string * exp [@@deriving sexp]
 
 and exp = position * raw_exp [@@deriving sexp]
 

src/astPrinter.ml

@@ -47,6 +47,8 @@ let pp_ap r =
       | `Proj i::l ->
         pf "%a.%d" (ul loop) l i
       | `Deref::l -> pf "*%a" (ul loop) l
+      | `Cons(con, i) :: l ->
+        pf "%a.%s.%d" (ul loop) l con i
     in
     loop steps
   | _ -> failwith "Unsupported operation ap"
@@ -75,7 +77,7 @@ let rec pp_ref_ast (r: RefinementTypes.concr_refinement) =
       (ul pp_ref_ast) r2
   | _ -> failwith @@ "Cannot annotate with relation " ^ (string_of_refinement r)
 
-let pp_lhs = function
+let rec pp_lhs = function
   | Var x -> pv x
   | Const i -> pi i
   | Mkref il -> pl [
@@ -104,6 +106,15 @@ let pp_lhs = function
     pf "%s[%s]" b i
   | LengthOf v ->
     pf "%s.length" v
+  | Cons (h, r) ->
+    pl [
+      ps "cons";
+      pp_lhs h;
+      ps "(";
+      pp_lhs r;
+      ps ")"
+    ]
+  | Nil -> ps "nil"
 
 let rec pp_patt = function
   | PVar v -> pv v
@@ -161,6 +172,16 @@ let rec pp_expr ~ip:((po_id,pr_id) as ip) ~annot (id,e) =
     | Unit -> ps "()"
     | Return v -> pf "return%a %s" po_id id v
     | Fail -> ps "fail"
+    | Match (e1, e2, h, r, e3) ->
+      pl [
+        pf "match %a with " (ul pp_lhs) e1;
+        pf "Nil -> { ";
+        pp_expr ~ip ~annot e2;
+        ps " } ";
+        pf "| Cons %s (%s) -> { " h r;
+        pp_expr ~ip ~annot e3;
+        ps "}";
+      ]
   in
   match e with
   | Seq _ -> e_printer

src/consort.ml

@@ -29,25 +29,25 @@ let result_to_string = function
   | Verified -> "VERIFIED"
   | Unverified r -> Printf.sprintf "UNVERIFIED (%s)" @@ reason_to_string r true
 
-let solver_result_to_check_result =
+(* let solver_result_to_check_result =
   let open Solver in
   function
   | Unsat -> Unverified Unsafe
   | Sat _ -> Verified
   | Timeout -> Unverified Timeout
   | Unhandled msg -> Unverified (UnhandledSolverOutput msg)
   | Error msg -> Unverified (SolverError msg)
-  | Unknown -> Unverified Unknown
+  | Unknown -> Unverified Unknown *)
 
-let choose_solver =
+(* let choose_solver =
   let open ArgOptions.Solver in
   function
   | Eldarica -> EldaricaBackend.solve
   | Hoice -> HoiceBackend.solve
   | Null -> NullSolver.solve
   | Parallel -> ParallelBackend.solve
   | Spacer -> HornBackend.solve
-  | Z3SMT -> SmtBackend.solve
+  | Z3SMT -> SmtBackend.solve *)
 
 let pcomment ~body =
   let open PrettyPrint in
@@ -75,13 +75,14 @@ let print_program ~o_map ~o_printer r ast =
       pf "[%a]@ %a"
         (ul print_type) t
         (ul o_printer) (o_map o)
-    | Mu (id,t) ->
-      pf "%s '%d.@ %a"
-        Greek.mu
-        id
-        (ul print_type) t
     | TVar id ->
       pf "'%d" id
+    | IntList ol ->
+      pl [
+        ps "int list @[";
+        psep_gen (pf ", ") @@ List.map (fun o -> pf "%a" (ul o_printer) (o_map o)) ol;
+        ps "]"
+      ]
   in
   let print_type_binding (k, t) = pb [pf "%s: " k; print_type t] in
   let print_type_sep t = List.map print_type t |> psep_gen (pf ",@ ") in
@@ -113,12 +114,12 @@ let print_program ~o_map ~o_printer r ast =
   in
   AstPrinter.pretty_print_program ~annot:pp_ty_env ~annot_fn:pp_f_type stdout ast
 
-let print_fold_locations simple_res =
+(* let print_fold_locations simple_res =
   let open SimpleChecker.SideAnalysis in
   let _, side = simple_res in
   print_endline "FOLD LOCATIONS >>>";
   Std.IntSet.iter (Printf.printf "* %d\n") side.fold_locs;
-  print_endline "<<<"
+  print_endline "<<<" *)
 
 let print_inference infer_res ast =
   let open PrettyPrint in
@@ -164,10 +165,15 @@ let print_typecheck (f_types, side) ast =
   let annot (id, _) e =
     match Std.IntMap.find_opt id side.let_types, e with
     | Some ty, Let (patt, _, _) -> from_ty_patt ty patt
-    | _ -> null in
+    | _ -> (
+      match Std.IntMap.find_opt id side.match_bindings, e with
+      | Some l, Match _ -> pl [ps "/* "; pl @@ List.map (fun (v, t) -> pf "%s: %s; " v @@ type_to_string t) l; ps "*/"; newline]
+      | _ -> null
+    )
+  in
   AstPrinter.pretty_print_program ~annot_fn ~annot stdout ast
 
-let to_hint o_res record =
+(* let to_hint o_res record =
   let open OwnershipInference in
   let o_map = function
     | OVar v -> List.assoc v o_res
@@ -176,15 +182,15 @@ let to_hint o_res record =
   {
     splits = SplitMap.map s_map record.splits;
     gen = GenMap.map o_map record.gen
-  }
+  } *)
 
-let get_solve ~opts =
+(* let get_solve ~opts =
   let open ArgOptions in
   let module Backend = struct
     let solve = choose_solver opts.solver
   end in
   let module S = FlowBackend.Make(Backend) in
-  S.solve
+  S.solve *)
 
 let consort ~opts file =
   let ast = AstUtil.parse_file file in
@@ -195,18 +201,18 @@ let consort ~opts file =
   let ownership_res = OwnershipSolver.solve_ownership ~opts infer_res in
   match ownership_res with
   | None -> Unverified Aliasing
-  | Some o_res ->
-    let o_hint = to_hint o_res infer_res.op_record in
+  | Some _ -> Verified
+    (* let o_hint = to_hint o_res infer_res.op_record in
     let solve = get_solve ~opts in
     let ans = solve ~opts simple_res o_hint ast in
-    solver_result_to_check_result ans
+    solver_result_to_check_result ans *)
 
 let ownership ~opts file =
   let ast = AstUtil.parse_file file in
   let intr_op = (ArgOptions.get_intr opts).op_interp in
   let simple_op = RefinementTypes.to_simple_funenv intr_op in
   let simple_res = SimpleChecker.typecheck_prog simple_op ast in
-  print_fold_locations simple_res;
+  (* print_fold_locations simple_res; *)
   let infer_res = OwnershipInference.infer ~opts simple_res ast in
   print_inference infer_res ast;
   let ownership_res = OwnershipSolver.solve_ownership ~opts infer_res in
@@ -222,3 +228,22 @@ let typecheck ~opts file =
   let simple_res = SimpleChecker.typecheck_prog simple_op ast in
   print_typecheck simple_res ast;
   Verified
+
+let convmochi ~opts file =
+  let ast = AstUtil.parse_file file in
+  (* print_endline @@ Sexplib.Sexp.to_string @@ Ast.sexp_of_prog ast; *)
+  let intr_op = (ArgOptions.get_intr opts).op_interp in
+  let simple_op = RefinementTypes.to_simple_funenv intr_op in
+  let simple_res = SimpleChecker.typecheck_prog simple_op ast in
+  let infer_res = OwnershipInference.infer ~opts simple_res ast in
+  let ownership_res = OwnershipSolver.solve_ownership ~opts infer_res in
+  let prog =
+    ConvMoCHi.prog_to_mochi infer_res
+      ((function Some x -> x | None -> assert false) ownership_res)
+      ast
+  in
+  (* ConvMoCHi.Mochi.print_prog prog; *)
+  let file = open_out "./test/to_mochi.ml" in
+  ConvMoCHi.Mochi.write_to_channel_prog prog file;
+  Out_channel.close file;
+  match ownership_res with None -> Unverified Aliasing | Some _ -> Verified

src/consort.mli

@@ -16,3 +16,4 @@ val result_to_string : check_result -> string
 val consort : opts:ArgOptions.t -> string -> check_result
 val ownership : opts:ArgOptions.t -> string -> check_result
 val typecheck : opts:ArgOptions.t -> string -> check_result
+val convmochi : opts:ArgOptions.t -> string -> check_result