Merge branch 'rewrite' of github.com:PLSysSec/FaCT into rewrite

.merlin

@@ -7,14 +7,12 @@ PKG llvm
 PKG Llvm_executionengine
 PKG ounit
 PKG core
-PKG dolog
 PKG ppx_deriving.std
-PKG ctypes
-PKG ctype.foreign
 PKG ocamlgraph
 PKG lwt
 PKG ANSITerminal
-PKG str
-PKG batteries
+PKG dolog
+PKG lwt.unix
+PKG z3
 
 EXT lwt

README.md

@@ -5,7 +5,7 @@
 
 To install you can either build the source or download ```fact.byte```. We recommend to build from source if possible.
 
-```fact.byte``` is the executable used to compile FaCT programs. Execute ```./fact.byte``` for a list of the command line options.
+```fact.byte``` is the executable used to compile FaCT programs. Execute ```./fact.byte -help``` for a list of the command line options.
 
 ## Usage
 
@@ -19,12 +19,12 @@ Many debugging options and intermediate data structures are available. Run ```./
 
 ## Set Up And Build On Local Machine
 
-FaCT is developed using Ocaml and LLVM 3.8. Make sure both of these are installed.
+FaCT is developed using Ocaml and LLVM 6.0. Make sure both of these are installed.
 On OS X it can be done with brew.
 
 ```
 brew install ocaml
-brew install llvm38
+brew install llvm60
 ```
 
 We also need dependency management for Ocaml.
@@ -33,23 +33,23 @@ We also need dependency management for Ocaml.
 
 Then we need the actual dependencies for Ocaml.
 
-```opam install llvm.6.0.0 core.v0.9.2 ounit.2.0.7 ctypes-foreign.0.4.0 utop.2.1.0 dolog.3.0 menhir.20171222 oasis.0.4.10 ppx_deriving.4.2.1 ANSITerminal.0.8 ocamlgraph.1.8.8 yojson.1.4.0 jbuilder.1.0+beta16 batteries.2.8.0 zarith.1.7```
+```
+opam switch 4.06.0
+eval $(opam config env)
+opam switch import ocamlswitch.txt
+```
 
 If you have not setup oasis, then you must do that first.
 
 ```oasis setup```
 
-Then we must configure oasis.
-
-```make configure```
-
-If you're having trouble, try reconfiguring your opam env.
+Make sure the Z3 lib is in the path:
 
-```eval $(opam config env)```
+```export LD_LIBRARY_PATH="$HOME/.opam/4.06.0/lib/z3"```
 
 Finally we can build the compiler.
 
-```make build```
+```make```
 
 If you want to add a dependency, add it to ```_oasis```, then run the 3 previous commands again.
 
@@ -65,21 +65,20 @@ This will add FaCT to your path so that you can compile const files with the com
 
 ## Link to a C library
 
-FaCT is designed to be called from C code. In order to do so, write your FaCT functions and compile them. This will output an object file. This can then be linked to a C file. A full working example is in the `example` directory. First, we must compile ```main.c``` in the `example` directory:
+FaCT is designed to be called from C code. In order to do so, write your FaCT functions and compile them. This will output an object file. This can then be linked to a C file. For example:
+
+```fact ex.fact```
+
+Then we compile the calling C file:
 
 ```
-cd example/
 clang -c main.c
 ```
 
-Then we compile ```ex.fact``` using FaCT. This requires clang to use version ≥3.8:
-
-```../fact.byte ex.fact```
-
 Next, we link them together:
 
 ```clang -o final main.o ex.o```
 
 Finally, we can run the executable:
 
-```./final ```
+```./final```

_oasis

@@ -6,17 +6,12 @@ Authors:     Gary Soeller, Sunjay Cauligi, Brian Johannesmeyer, Ariana Mirian, Y
 Homepage:    https://github.com/PLSysSec/FaCT
 License:     MIT
 Plugins:     META (0.4), DevFiles (0.4)
-BuildDepends: llvm, llvm.analysis, llvm.bitwriter, llvm.executionengine, llvm.target, llvm.passmgr_builder, llvm.irreader, llvm.linker, llvm.transform_utils, llvm.scalar_opts, llvm.vectorize, llvm.ipo, core, oUnit, dolog, threads, ppx_deriving.std, ctypes, ctypes.foreign, ocamlgraph, lwt.unix, lwt.ppx, ANSITerminal, str, batteries, zarith
-OCamlVersion: >= 4.03
+BuildDepends: llvm, llvm.analysis, llvm.bitwriter, llvm.executionengine, llvm.target, llvm.passmgr_builder, llvm.irreader, llvm.linker, llvm.transform_utils, llvm.scalar_opts, llvm.vectorize, llvm.ipo, core, threads, ppx_deriving.std, lwt.unix, ANSITerminal, dolog, str, z3
+OCamlVersion: >= 4.06
 AlphaFeatures: ocamlbuild_more_args
 XOCamlbuildPluginTags: package(cppo_ocamlbuild)
 
 Executable fact
   Path:       src
   BuildTools: ocamlbuild
   MainIs:     fact.ml
-
-Executable facti
-  Path:       src
-  BuildTools: ocamlbuild
-  MainIs:     facti.ml

_tags

@@ -3,7 +3,7 @@ true: use_menhir, bin_annot, debug
 <*.{byte,native}>: g++, use_llvm, use_llvm_analysis, use_llvm_bitwriter, use_llvm_irreader, use_llvm_linker, use_llvm_target, use_llvm_X86, use_llvm_bitreader, use_llvm_executionengine
 
 # OASIS_START
-# DO NOT EDIT (digest: 4eac8801662b660eaae602ddd1d6536d)
+# DO NOT EDIT (digest: be84367006abea1c6aa9be4a8cc99ec3)
 # Ignore VCS directories, you can use the same kind of rule outside
 # OASIS_START/STOP if you want to exclude directories that contains
 # useless stuff for the build process
@@ -20,10 +20,7 @@ true: annot, bin_annot
 "_darcs": not_hygienic
 # Executable fact
 "src/fact.byte": package(ANSITerminal)
-"src/fact.byte": package(batteries)
 "src/fact.byte": package(core)
-"src/fact.byte": package(ctypes)
-"src/fact.byte": package(ctypes.foreign)
 "src/fact.byte": package(dolog)
 "src/fact.byte": package(llvm)
 "src/fact.byte": package(llvm.analysis)
@@ -37,46 +34,13 @@ true: annot, bin_annot
 "src/fact.byte": package(llvm.target)
 "src/fact.byte": package(llvm.transform_utils)
 "src/fact.byte": package(llvm.vectorize)
-"src/fact.byte": package(lwt.ppx)
 "src/fact.byte": package(lwt.unix)
-"src/fact.byte": package(oUnit)
-"src/fact.byte": package(ocamlgraph)
 "src/fact.byte": package(ppx_deriving.std)
 "src/fact.byte": package(str)
 "src/fact.byte": package(threads)
-"src/fact.byte": package(zarith)
-# Executable facti
-"src/facti.byte": package(ANSITerminal)
-"src/facti.byte": package(batteries)
-"src/facti.byte": package(core)
-"src/facti.byte": package(ctypes)
-"src/facti.byte": package(ctypes.foreign)
-"src/facti.byte": package(dolog)
-"src/facti.byte": package(llvm)
-"src/facti.byte": package(llvm.analysis)
-"src/facti.byte": package(llvm.bitwriter)
-"src/facti.byte": package(llvm.executionengine)
-"src/facti.byte": package(llvm.ipo)
-"src/facti.byte": package(llvm.irreader)
-"src/facti.byte": package(llvm.linker)
-"src/facti.byte": package(llvm.passmgr_builder)
-"src/facti.byte": package(llvm.scalar_opts)
-"src/facti.byte": package(llvm.target)
-"src/facti.byte": package(llvm.transform_utils)
-"src/facti.byte": package(llvm.vectorize)
-"src/facti.byte": package(lwt.ppx)
-"src/facti.byte": package(lwt.unix)
-"src/facti.byte": package(oUnit)
-"src/facti.byte": package(ocamlgraph)
-"src/facti.byte": package(ppx_deriving.std)
-"src/facti.byte": package(str)
-"src/facti.byte": package(threads)
-"src/facti.byte": package(zarith)
+"src/fact.byte": package(z3)
 <src/*.ml{,i,y}>: package(ANSITerminal)
-<src/*.ml{,i,y}>: package(batteries)
 <src/*.ml{,i,y}>: package(core)
-<src/*.ml{,i,y}>: package(ctypes)
-<src/*.ml{,i,y}>: package(ctypes.foreign)
 <src/*.ml{,i,y}>: package(dolog)
 <src/*.ml{,i,y}>: package(llvm)
 <src/*.ml{,i,y}>: package(llvm.analysis)
@@ -90,14 +54,11 @@ true: annot, bin_annot
 <src/*.ml{,i,y}>: package(llvm.target)
 <src/*.ml{,i,y}>: package(llvm.transform_utils)
 <src/*.ml{,i,y}>: package(llvm.vectorize)
-<src/*.ml{,i,y}>: package(lwt.ppx)
 <src/*.ml{,i,y}>: package(lwt.unix)
-<src/*.ml{,i,y}>: package(oUnit)
-<src/*.ml{,i,y}>: package(ocamlgraph)
 <src/*.ml{,i,y}>: package(ppx_deriving.std)
 <src/*.ml{,i,y}>: package(str)
 <src/*.ml{,i,y}>: package(threads)
-<src/*.ml{,i,y}>: package(zarith)
+<src/*.ml{,i,y}>: package(z3)
 # OASIS_STOP
 "perf": -traverse
 "perf": not_hygienic

ocamlswitch.txt

@@ -0,0 +1,85 @@
+ANSITerminal	0.8	root
+base	v0.11.1	installed
+base-bigarray	base	root
+base-bytes	base	installed
+base-threads	base	root
+base-unix	base	root
+bin_prot	v0.11.0	installed
+biniou	1.2.0	installed
+conf-cmake	1	installed
+conf-gmp	1	installed
+conf-llvm	6.0.0	installed
+conf-m4	1	installed
+conf-pkg-config	1.1	installed
+conf-python-2-7	1.0	installed
+conf-which	1	installed
+configurator	v0.11.0	installed
+core	v0.11.2	root
+core_kernel	v0.11.1	installed
+cppo	1.6.4	installed
+cppo_ocamlbuild	1.6.0	installed
+ctypes	0.14.0	root
+ctypes-foreign	0.4.0	root
+dolog	3.0	root
+dune	1.0.0	installed
+easy-format	1.3.1	installed
+fieldslib	v0.11.0	installed
+integers	0.2.2	installed
+jane-street-headers	v0.11.0	installed
+jbuilder	transition	installed
+llvm	6.0.0	root
+lwt	4.1.0	root
+lwt_ppx	1.2.1	root
+menhir	20180703	root
+merlin	3.1.0	root
+num	1.1	installed
+oasis	0.4.11	root
+ocaml-compiler-libs	v0.11.0	installed
+ocaml-migrate-parsetree	1.0.11	installed
+ocamlbuild	0.12.0	installed
+ocamlfind	1.8.0	installed
+ocamlify	0.0.1	installed
+ocamlmod	0.0.9	installed
+octavius	1.2.0	installed
+parsexp	v0.11.0	installed
+ppx_assert	v0.11.0	installed
+ppx_base	v0.11.0	installed
+ppx_bench	v0.11.0	installed
+ppx_bin_prot	v0.11.1	installed
+ppx_compare	v0.11.1	installed
+ppx_custom_printf	v0.11.0	installed
+ppx_derivers	1.0	installed
+ppx_deriving	4.2.1	root
+ppx_enumerate	v0.11.1	installed
+ppx_expect	v0.11.0	installed
+ppx_fail	v0.11.0	installed
+ppx_fields_conv	v0.11.0	installed
+ppx_hash	v0.11.1	installed
+ppx_here	v0.11.0	installed
+ppx_inline_test	v0.11.0	installed
+ppx_jane	v0.11.0	installed
+ppx_js_style	v0.11.0	installed
+ppx_let	v0.11.0	installed
+ppx_optcomp	v0.11.0	installed
+ppx_optional	v0.11.0	installed
+ppx_pipebang	v0.11.0	installed
+ppx_sexp_conv	v0.11.2	installed
+ppx_sexp_message	v0.11.0	installed
+ppx_sexp_value	v0.11.0	installed
+ppx_tools	5.1+4.06.0	installed
+ppx_tools_versioned	5.2	installed
+ppx_typerep_conv	v0.11.1	installed
+ppx_variants_conv	v0.11.1	installed
+ppxlib	0.3.0	installed
+re	1.7.3	installed
+result	1.3	installed
+sexplib	v0.11.0	installed
+sexplib0	v0.11.0	installed
+spawn	v0.12.0	installed
+splittable_random	v0.11.0	installed
+stdio	v0.11.0	installed
+topkg	0.9.1	installed
+typerep	v0.11.0	installed
+variantslib	v0.11.0	installed
+yojson	1.4.1	installed
+z3	4.7.1	root

src/arr_speccer.ml

@@ -0,0 +1,90 @@
+open Util
+open Pos
+open Err
+open Ast
+open Ast_util
+open Astmap
+
+let findfn fmap fname =
+  Core.List.Assoc.find fmap fname ~equal:vequal
+
+class array_spec_fncall =
+  object (visit)
+    inherit Astmap.ast_visitor as super
+    val mutable _fmap : (fun_name * params) list = []
+
+    method fact_module m =
+      let Module(_,fdecs) = m in
+        List.iter
+          (fun fdec ->
+             match fdec.data with
+               | FunDec(fn,_,_,params,_) ->
+                 _fmap <- (fn,params) :: _fmap
+               | _ -> ())
+          fdecs;
+        super#fact_module m
+
+    method _fncall fn args =
+      match findfn _fmap fn with
+        | Some params ->
+          let args' =
+            try List.map2
+                  (fun arg param ->
+                     let Param (x,bty) = param.data in
+                       match is_unspec_arr bty with
+                         | Some _ ->
+                           [arg ; arg.pos @> ArrayLen arg]
+                         | None -> [arg])
+                  args
+                  params
+            with Invalid_argument _ ->
+              raise @@ cerr fn.pos "arity mismatch on call to '%s'" fn.data
+          in
+            List.flatten args'
+        | None -> args
+
+    method stm_post ({pos=p;data} as stm_) =
+      match data with
+        | FnCall (x,bty,fn,args) ->
+          p @> FnCall (x,bty,fn,visit#_fncall fn args)
+        | VoidFnCall (fn,args) ->
+          p @> VoidFnCall (fn,visit#_fncall fn args)
+        | _ -> super#stm_post stm_
+
+  end
+
+class array_spec_fdec =
+  object (visit)
+    inherit Astmap.ast_visitor as super
+
+    method fdec_post =
+      wrap @@ fun p -> function
+        | FunDec (fn,ft,rt,params,body) ->
+          let params' =
+            List.map
+              (fun param ->
+                 match param.data with
+                   | Param (x,{pos;data=Arr (bty,{data=LUnspecified},vattr)}) ->
+                     let x_len = p @> make_fresh (x.data ^ "_len") in
+                     let var_expr = p@>Variable x_len in
+                       [p@>Param (x,{pos;data=Arr (bty,{pos;data=LExpression var_expr},vattr)});
+                        p@>Param (x_len,{pos;data=UInt (64,p@>Public)})]
+                   | _ -> [param])
+              params
+          in
+            FunDec(fn,ft,rt,List.flatten params',body)
+        | CExtern (fn,ft,rt,params) as fdec ->
+          List.iter
+            (fun param ->
+               match param.data with
+                 | _ -> ())
+            params;
+          fdec
+
+    end
+
+let transform m =
+  let visit_fncall = new array_spec_fncall in
+  let m' = visit_fncall#fact_module m in
+  let visit_fdec = new array_spec_fdec in
+    visit_fdec#fact_module m'