CN: split CN into a library and an executable (#429)

* CN: split CN into library and executable components

* CN: remove CLI dependency from library

* CN: update filepath references in docs

backend/cn/ONBOARDING.md

@@ -48,7 +48,7 @@ General principles:
 * Core adjustments: if you run CN with `-d N` for `N = {1,2,3}` then it will
   produce `/tmp/0__original.core`, `/tmp/1__without_unspec.core`,
   `/tmp/2__after_peval.core`, `/tmp/3__mucore.mucore`. Some of these are referred to as 'milicore'.
-* Core to mucore: `backend/cn/core_to_mucore.ml`
+* Core to mucore: `backend/cn/lib/core_to_mucore.ml`
 * Mucore: This is the thing that CN typechecks.
 
 ### CN Pipeline Entry
@@ -66,30 +66,30 @@ with a different entry point from which a parser can be started:
   inserted as string annotations (attributes).
 4. Cabs is desugared, then elaborated into Core (including the CN toplevel declarations).
 5. Core is turned into mucore, during which process the remaining magic
-  comments are parsed and desugared into mucore as well (`backend/cn/parse.ml`).
+  comments are parsed and desugared into mucore as well (`backend/cn/lib/parse.ml`).
 
 ## Key Files
 
-* Entry point to the executable: `backend/cn/main.ml`
-* Specification well-formedness checking: `backend/cn/wellTyped.ml`
-* Actual C code type checking: `backend/cn/check.ml`
-* Type checking mondad: `backend/cn/typing.ml{i}`
-* SMT solver interface: `backend/cn/solver.ml`
-* CN errors: `backend/cn/typeErrors.ml`
-* HTML report generation: `backend/cn/report.ml`
+* Entry point to the executable: `backend/cn/bin/main.ml`
+* Specification well-formedness checking: `backend/cn/lib/wellTyped.ml`
+* Actual C code type checking: `backend/cn/lib/check.ml`
+* Type checking mondad: `backend/cn/lib/typing.ml{i}`
+* SMT solver interface: `backend/cn/lib/solver.ml`
+* CN errors: `backend/cn/lib/typeErrors.ml`
+* HTML report generation: `backend/cn/lib/report.ml`
 
 ## Key Types
 
-* Basetypes: `backend/cn/baseTypes.ml`
-* Terms: `backend/cn/terms.ml`
-* Logical Argument Types: `backend/cn/logicalArgumentTypes.ml`
+* Basetypes: `backend/cn/lib/baseTypes.ml`
+* Terms: `backend/cn/lib/terms.ml`
+* Logical Argument Types: `backend/cn/lib/logicalArgumentTypes.ml`
     ```
     let x = 5 + 5;      // Define
     take X = Pred(..);  // Resource
     assert (expr);      // Constraint
     ```
-* Resource Types: the "signatures" of predicates, in `backend/cn/resourceTypes.ml`
-* Resource Predicates: the defintion of predicates, in `backend/cn/resourcePredicates.ml`
+* Resource Types: the "signatures" of predicates, in `backend/cn/lib/resourceTypes.ml`
+* Resource Predicates: the defintion of predicates, in `backend/cn/lib/resourcePredicates.ml`
 
 ## Code Cleanup
 
@@ -100,7 +100,7 @@ You can generate them using the below **from the root of the repo** and **on a w
 [ ! -d backend/cn ] && echo "DO NOT PROCEED: Go to cerberus repo root" 
 make && make install && make install_cn
 opam install ocaml-print-intf
-dune exec -- ocaml-print-intf backend/cn/XXXXX.ml | sed 's/Dune__exe.//g' > XXXXX.mli
+dune exec -- ocaml-print-intf backend/cn/lib/XXXXX.ml | sed 's/Dune__exe.//g' > XXXXX.mli
 # edit it
 make && make install && make install_cn
 ```
@@ -112,7 +112,7 @@ make && make install && make install_cn
      ... enormous amount of stuff
     end
   ```
-  replace it with something like the below (see `backend/cn/setup.mli`).
+  replace it with something like the below (see `backend/cn/lib/setup.mli`).
   ```
   module StringSet : Set.S with type elt = string
   ```
@@ -138,7 +138,7 @@ make && make install && make install_cn
 
 ```
 opam install codept
-codept backend/cn/*.ml > cn-modules.dot
+codept backend/cn/lib/*.ml > cn-modules.dot
 dot -Tpdf -o cn-modules.pdf # -x optionally to "simplify"
 ```
 

backend/cn/README.md

@@ -50,7 +50,8 @@ via `opam init` after the installation of opam.)
    make install_cn
    ```
 
-   which installs Cerberus, CN, and dependencies.
+   which installs Cerberus, CN (as both a library and an executable), and
+   dependencies.
 
 ## Contributing
 

backend/cn/bin/dune

@@ -0,0 +1,33 @@
+(executable
+ (name main)
+ (modes exe)
+ (public_name cn)
+ (package cn)
+ (flags
+  (:standard -w -37 -open Monomorphic.Int))
+ (libraries
+  cerb_backend
+  cerb_frontend
+  cerb_util
+  cmdliner
+  cn
+  mem_concrete
+  menhirLib
+  monomorphic
+  ocamlgraph
+  result
+  str
+  unix
+  z3))
+
+; There is already a Version in Cerb_frontend, but if new commits only require
+; rebuilding the CN backend that module will be out of date.
+; So we add a CN specific version.
+
+(rule
+ (targets cn_version.ml)
+ (deps (universe))
+ (action
+  (with-stdout-to
+   cn_version.ml
+   (run ocaml -I +unix unix.cma %{dep:../../../tools/gen_version.ml}))))

backend/cn/main.ml → backend/cn/bin/main.ml

@@ -1,3 +1,4 @@
+open Cn
 open Builtins
 module CF = Cerb_frontend
 module CB = Cerb_backend

backend/cn/dune

@@ -1,41 +1 @@
-(include_subdirs qualified)
-
-(executable
- (name main)
- (modes exe)
- (public_name cn)
- (package cn)
- (flags
-  (:standard -w -37 -open Monomorphic.Int))
- (libraries
-  cerb_backend
-  cerb_frontend
-  cerb_util
-  cmdliner
-  mem_concrete
-  menhirLib
-  monomorphic
-  ocamlgraph
-  result
-  str
-  unix
-  z3)
- (preprocess
-  (pps
-   ppx_deriving.eq
-   ppx_deriving.fold
-   ppx_deriving.map
-   ppx_deriving.ord
-   ppx_deriving.show)))
-
-; There is already a Version in Cerb_frontend, but if new commits only require
-; rebuilding the CN backend that module will be out of date.
-; So we add a CN specific version.
-
-(rule
- (targets cn_version.ml)
- (deps (universe))
- (action
-  (with-stdout-to
-   cn_version.ml
-   (run ocaml -I +unix unix.cma %{dep:../../tools/gen_version.ml}))))
+(dirs lib bin)

backend/cn/cn_internal_to_ail.ml → backend/cn/lib/cn_internal_to_ail.ml

@@ -817,7 +817,7 @@ let rec cn_to_ail_expr_aux_internal
   : type a.
     _ option ->
     _ option ->
-    _ Cn.cn_datatype list ->
+    _ CF.Cn.cn_datatype list ->
     (C.union_tag * C.ctype) list ->
     IT.t ->
     a dest ->
@@ -1490,15 +1490,16 @@ let rec cn_to_ail_expr_aux_internal
 
 
 let cn_to_ail_expr_internal
-  : type a. _ Cn.cn_datatype list -> (C.union_tag * C.ctype) list -> IT.t -> a dest -> a
+  : type a.
+    _ CF.Cn.cn_datatype list -> (C.union_tag * C.ctype) list -> IT.t -> a dest -> a
   =
   fun dts globals cn_expr d -> cn_to_ail_expr_aux_internal None None dts globals cn_expr d
 
 
 let cn_to_ail_expr_internal_with_pred_name
   : type a.
     Sym.sym option ->
-    _ Cn.cn_datatype list ->
+    _ CF.Cn.cn_datatype list ->
     (C.union_tag * C.ctype) list ->
     IT.t ->
     a dest ->
@@ -2732,7 +2733,7 @@ let cn_to_ail_resource_internal
 
 let cn_to_ail_logical_constraint_internal
   : type a.
-    _ Cn.cn_datatype list ->
+    _ CF.Cn.cn_datatype list ->
     (C.union_tag * C.ctype) list ->
     a dest ->
     LC.logical_constraint ->
@@ -2837,7 +2838,7 @@ let cn_to_ail_function_internal
   let param_types = List.map (fun t -> (empty_qualifiers, t, false)) param_types in
   let matched_cn_functions =
     List.filter
-      (fun (cn_fun : (A.ail_identifier, C.ctype) Cn.cn_function) ->
+      (fun (cn_fun : (A.ail_identifier, C.ctype) CF.Cn.cn_function) ->
         Sym.equal cn_fun.cn_func_name fn_sym)
       cn_functions
   in
@@ -2986,7 +2987,7 @@ let cn_to_ail_predicate_internal
   in
   let matched_cn_preds =
     List.filter
-      (fun (cn_pred : (A.ail_identifier, C.ctype) Cn.cn_predicate) ->
+      (fun (cn_pred : (A.ail_identifier, C.ctype) CF.Cn.cn_predicate) ->
         Sym.equal cn_pred.cn_pred_name pred_sym)
       cn_preds
   in
@@ -3049,7 +3050,7 @@ let cn_to_ail_post_internal dts globals preds (RT.Computational (bound, oinfo, t
 (* TODO: Add destination passing *)
 let cn_to_ail_cnstatement_internal
   : type a.
-    _ Cn.cn_datatype list ->
+    _ CF.Cn.cn_datatype list ->
     (C.union_tag * C.ctype) list ->
     a dest ->
     Cnprog.cn_statement ->

backend/cn/lib/dune

@@ -0,0 +1,26 @@
+(include_subdirs qualified)
+
+(library
+ (name cn)
+ (public_name cn)
+ (flags
+  (:standard -w -37 -open Monomorphic.Int))
+ (libraries
+  cerb_backend
+  cerb_frontend
+  cerb_util
+  mem_concrete
+  menhirLib
+  monomorphic
+  ocamlgraph
+  result
+  str
+  unix
+  z3)
+ (preprocess
+  (pps
+   ppx_deriving.eq
+   ppx_deriving.fold
+   ppx_deriving.map
+   ppx_deriving.ord
+   ppx_deriving.show)))

backend/cn/executable_spec_internal.ml → backend/cn/lib/executable_spec_internal.ml

@@ -43,7 +43,7 @@ let generate_ail_stat_strs
 
 let populate_record_map_aux (sym, bt_ret_type) =
   match Cn_internal_to_ail.bt_to_cn_base_type bt_ret_type with
-  | Cn.CN_record members ->
+  | CF.Cn.CN_record members ->
     let sym' = Cn_internal_to_ail.generate_sym_with_suffix ~suffix:"_record" sym in
     Cn_internal_to_ail.records
     := Cn_internal_to_ail.RecordMap.add members sym' !Cn_internal_to_ail.records

backend/cn/mucore.ml → backend/cn/lib/mucore.ml

@@ -270,7 +270,7 @@ type 'TY mu_expr_ =
   | M_End of 'TY mu_expr list (* nondeterministic choice *)
   (* | M_Edone of 'TY mu_expr *)
   | M_Erun of symbol * 'TY mu_pexpr list (* run from label *)
-  | M_CN_progs of (Sym.t, Ctype.ctype) Cn.cn_statement list * Cnprog.cn_prog list
+  | M_CN_progs of (Sym.t, Ctype.ctype) CF.Cn.cn_statement list * Cnprog.cn_prog list
 
 and 'TY mu_expr = M_Expr of loc * annot list * 'TY * 'TY mu_expr_
 
@@ -458,7 +458,7 @@ let evaluate_fun mu_fun args =
      | _ -> None)
 
 
-type parse_ast_label_spec = { label_spec : (Sym.t, Ctype.ctype) Cn.cn_condition list }
+type parse_ast_label_spec = { label_spec : (Sym.t, Ctype.ctype) CF.Cn.cn_condition list }
 
 type 'TY mu_label_def =
   | M_Return of loc
@@ -489,8 +489,8 @@ type 'TY mu_proc_args_and_body = ('TY mu_expr * 'TY mu_label_defs * T.rt) mu_arg
 
 type parse_ast_function_specification =
   { accesses : (Sym.t * Ctype.ctype) list;
-    requires : (Sym.t, Ctype.ctype) Cn.cn_condition list;
-    ensures : (Sym.t, Ctype.ctype) Cn.cn_condition list
+    requires : (Sym.t, Ctype.ctype) CF.Cn.cn_condition list;
+    ensures : (Sym.t, Ctype.ctype) CF.Cn.cn_condition list
   }
 
 type 'TY mu_fun_map_decl =