FFI generated

Author: tycon

README.md

@@ -0,0 +1,33 @@
+About C Intermediate Language (CIL)
+===================================
+
+[CIL][] is a front-end for the C programming language that facilitates
+program analysis and transformation. CIL will parse and typecheck a
+program, and compile it into a simplified subset of C.
+
+[CIL]: http://www.cs.berkeley.edu/~necula/cil/
+
+About Z3
+=============
+
+[Z3] is a state-of-the-art SMT solver by Microsoft Research.
+[Z3]: www.rise4fun.com/Z3
+
+About MLton
+=============
+
+[MLton] is a whole-program optimising Standard ML compiler
+[MLton]: http://mlton.org/
+
+
+About Z3MLton
+==============
+
+Z3MLton is an extension for CIL that parses Z3 [C API] and generates
+MLton Foreign Function Interface ([MLFFI]) that enables MLton programs
+to access Z3 C APIs.
+
+[C API]: http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html
+[MLFFI]: http://mlton.org/ForeignFunctionInterface
+
+

run.sh

@@ -0,0 +1,2 @@
+#! /bin/sh
+cilly --merge --keepunused --domakesml $@

src/ext/makesml/META

@@ -0,0 +1 @@
+description = "converting z3_api.h to Z3_FFI.sml"

src/ext/makesml/default

@@ -0,0 +1,140 @@
+open Pretty
+open Cil
+open Feature
+module E = Errormsg
+module H = Hashtbl
+
+let typtbl = H.create 117
+
+let _ = 
+  H.add typtbl "int" "int";
+  H.add typtbl "void" "unit";
+  H.add typtbl "float" "double";
+  H.add typtbl "ptr" "MLton.Pointer.t"
+
+type varinfo = {mltyp : string; args : string}
+
+let vartbl = H.create 1009
+
+let mkFunTy (argTy,resTy) = argTy ^ " -> " ^ resTy
+
+let mkTupleTy tys = "("^(match tys with 
+  | [] -> "" 
+  | x::xs -> List.fold_left (fun acc ty ->
+      acc^" * "^ty) x xs)^")"
+
+let rec maptype typ = match typ with
+  | TVoid _ -> H.find typtbl "void"
+  | TInt _ -> H.find typtbl "int"
+  | TFloat _ -> H.find typtbl "float"
+  | TPtr _ -> H.find typtbl "ptr"
+  | TArray _ -> H.find typtbl "ptr"
+  | TFun (retTy,None,_,_) -> mkFunTy (H.find typtbl "void",maptype retTy)
+  | TFun (retTy,Some argTys,_,_) -> mkFunTy (mkTupleTy 
+      (List.map (fun (_,ty,_) -> maptype ty) argTys), maptype retTy)
+  | TNamed ({tname=tname;ttype=ttype},_) -> (try H.find typtbl tname with 
+      | Not_found ->
+          let mltyname = match Str.string_match (Str.regexp "^Z3_") 
+            tname 0 with
+              | false -> "Tunknown_"^tname
+              | true -> "z3_"^(Str.string_after tname 3) in
+            (H.add typtbl tname mltyname;
+             mltyname))
+  | TComp _ | TEnum _ | TBuiltin_va_list _ -> 
+      (E.log "Unknown type : %a\n" d_type typ; "Tunknown")
+
+let mapargs typ = match typ with
+  | TFun (_,None,_,_) -> "()"
+  | TFun (_,Some argTys,_,_) -> "("^(match argTys with 
+      [] -> ""
+    | (x,_,_)::xs -> List.fold_left (fun acc (a,b,c) -> 
+        acc^","^a) x xs)^")"
+
+let globalFolder x glob = match glob with
+  | GVarDecl ({vname=vname;vtype=vtype},_) -> 
+      let case = Str.string_match (Str.regexp "^Z3_") vname 0 in
+        (match case with 
+        | true -> H.add vartbl vname {mltyp = maptype vtype;
+            args = mapargs vtype}
+        | false -> ())
+  | _ -> ()
+
+let myconcat docs = List.fold_left concat nil docs
+
+let info = "(*\n * Automatically generated by makesml CIL plugin\n *)\n"
+
+let instantiateFunDec (name,args,typ) = 
+  let decs = myconcat [
+      text ("val dyn_"^name^" = _import * : DynLink.fptr -> "
+        ^typ^";");
+      line;
+      text ("val "^name^"_ptr = DynLink.dlsym(hndl, \""^name^"\")");
+    ] in
+  let expr = text ("dyn_"^name^" "^name^"_ptr "^args) in
+    myconcat [
+      text ("fun "^name^" "^args^" = ");
+      line;
+      text "let";
+      line;
+      indent 2 decs;
+      line;
+      text "in";
+      line;
+      indent 2 expr;
+      line;
+      text "end";
+      line;
+    ]
+
+let makeStructDoc () =
+  let header = myconcat [text "structure Z3_FFI : Z3_FFI_INTERFACE =";
+    line; text "struct"; line] in
+  let typedecs = H.fold (fun _ mlTy doc -> 
+    if Str.string_match (Str.regexp "^z3_") mlTy 0
+    then myconcat [text ("type "^mlTy^" = MLton.Pointer.t");
+        line; doc]
+    else doc) typtbl nil in
+  let fundecs = H.fold (fun name {mltyp=typ;args=args} doc ->
+    myconcat [doc;line;instantiateFunDec (name,args,typ)]) 
+    vartbl nil in
+  let decs = myconcat [typedecs; line; fundecs] in
+  let footer = text "end" in
+  let doc = myconcat [header; indent 2 decs; footer] in
+  let outf = open_out "z3_ffi.sml" in
+    output_string outf info;
+    output_string outf (sprint 70 doc)
+    (*E.log "%s\n" (sprint 80 doc)*)
+
+let makeSigDoc () = 
+  let header = concat (concat (concat (text "signature Z3_FFI_INTERFACE =")
+    line) (text "sig")) line  in
+  let typedecs = H.fold (fun _ mlTy doc -> 
+    if Str.string_match (Str.regexp "^z3_") mlTy 0
+    then concat (concat (text ("type "^mlTy)) line) doc
+    else doc) typtbl nil in
+  let vardecs = H.fold (fun vname {mltyp=mlTy;} doc -> myconcat
+    [text ("val "^vname^" : "^mlTy);line;doc]) vartbl nil in
+  let decs = myconcat [typedecs;line;vardecs] in
+  let footer = text "end" in
+  let doc = concat (concat header (indent 2 decs)) footer in
+  let outf = open_out "z3_ffi.sig" in
+    output_string outf info;
+    output_string outf (sprint 70 doc)
+    (*E.log "%s\n" (sprint 80 doc)*)
+
+let featureHook (f : file) =
+  let _ = foldGlobals f globalFolder () in
+  let sigdoc = makeSigDoc () in
+  let structdoc = makeStructDoc () in
+    ()
+
+let feature = 
+  { fd_name = "makesml";
+    fd_enabled = false;
+    fd_description = "Convert z3_api.h to Z3_FFI.sml";
+    fd_extraopt = [];
+    fd_doit = featureHook;
+    fd_post_check = false;
+  } 
+let _ = E.log "makesml feature registered\n"
+let () = Feature.register feature