Split libASL and isolate Z3 into virtual library (#91)

Z3 links to a native shared library, and so is unsuitable for use via js-of-ocaml. This separates the one use of Z3 in the code (the type-checker's constraint solver) into a separate library which may be stubbed for non-native platforms.

This separates libASL into two parts: libASL_ast which is the minimum needed to define the ASL syntax tree, and libASL which contains the rest of the library. libASL should still be used as the public interface of the library. Since libASL re-exports all of libASL_ast, this should not affect the API visible by downstream users.

This is required since we need to insert a platform-specific library, libASL_support, which introduces z3 only on native builds. The dependency tree now looks like: libASL_ast <- libASL_support (virtual) <- libASL.

bin/dune

@@ -5,7 +5,7 @@
  (modes exe byte)
  (modules asli)
  (flags (-cclib -lstdc++))
- (libraries libASL linenoise pprint pcre)
+ (libraries libASL libASL_native linenoise pprint pcre)
  )
 
 (executable
@@ -14,7 +14,7 @@
  (modes exe)
  (modules server)
  (flags (-cclib -lstdc++))
- (libraries libASL pprint pcre lwt.unix yojson cohttp-lwt cohttp-lwt-unix))
+ (libraries libASL libASL_native pprint pcre lwt.unix yojson cohttp-lwt cohttp-lwt-unix))
 
 
 (executable
@@ -39,12 +39,12 @@
  (modes exe)
  (modules offline_coverage)
  (flags (-cclib -lstdc++))
- (libraries libASL offlineASL))
+ (libraries libASL libASL_native offlineASL))
 
 (executable
  (name offline_sem)
  (public_name asloff-sem)
  (modes exe)
  (modules offline_sem)
  (flags (-cclib -lstdc++))
- (libraries libASL offlineASL))
+ (libraries libASL libASL_native offlineASL))

libASL/dune

@@ -14,18 +14,26 @@
      (with-stdout-to asl_parser_tail.mly (bash "OTT=${ASLI_OTT:-$(opam config var ott:share)};  grep -v '^%%' $OTT/menhir_library_extra.mly"))
      (with-stdout-to asl_parser.mly (run cat asl_parser_head.mly asl_parser_tail.mly)))))
 
+(library
+ (name libASL_ast)
+ (public_name asli.libASL-ast)
+ (flags (:standard -w -27))
+ (wrapped false)
+ (modules asl_ast asl_parser asl_parser_pp asl_utils asl_visitor visitor utils)
+ (libraries pprint (re_export zarith)))
+
 (library
  (name libASL)
  (public_name asli.libASL)
  (flags
   (:standard -w -27 -cclib -lstdc++))
- (modules asl_ast asl_parser asl_parser_pp asl_utils asl_visitor cpu dis elf eval
-   lexer lexersupport loadASL monad primops rws symbolic tcheck testing transforms utils value visitor res
+ (modules cpu dis elf eval
+   lexer lexersupport loadASL monad primops rws symbolic tcheck testing transforms value res
    symbolic_lifter decoder_program call_graph req_analysis
    offline_transform ocaml_backend dis_tc
    offline_opt
    )
- (libraries pprint zarith z3 str pcre  dune-site))
+ (libraries libASL_support (re_export libASL_ast) str pcre dune-site))
 
 (generate_sites_module
  (module res)

libASL/ocaml_backend.ml

@@ -333,7 +333,7 @@ let write_fn name (ret_tyo,_,targs,args,_,body) st =
  ****************************************************************)
 
 let init_st oc = { depth = 0; skip_seq = false; oc ; ref_vars = IdentSet.empty } 
-let global_deps = ["Utils"]
+let global_deps = ["Offline_utils"]
 
 (* Write an instruction file, containing just the behaviour of one instructions *)
 let write_instr_file fn fnsig dir =
@@ -372,7 +372,8 @@ let write_decoder_file fn fnsig deps dir =
 (* Write the dune build file *)
 let write_dune_file files dir =
   let oc = open_out (dir ^ "/dune") in
-  Printf.fprintf oc "(library
+  Printf.fprintf oc "; AUTO-GENERATED BY OCAML BACKEND
+(library
   (name offlineASL)
   (flags
     (:standard -w -27 -w -33 -cclib -lstdc++))
@@ -381,10 +382,10 @@ let write_dune_file files dir =
     Printf.fprintf oc "    %s\n" (String.lowercase_ascii k)
   ) files;
   Printf.fprintf oc "  )
-  (libraries zarith libASL))";
+  (libraries libASL))";
   close_out oc
 
-(* Write all of the above, expecting Utils.ml to already be present in dir *)
+(* Write all of the above, expecting offline_utils.ml to already be present in dir *)
 let run dfn dfnsig tests fns dir =
   let files = Bindings.fold (fun fn fnsig acc -> (write_instr_file fn fnsig dir)::acc) fns [] in
   let files = (write_test_file tests dir)::files in

libASL/support/dune

@@ -0,0 +1,7 @@
+; provides platform-specific dependencies
+
+(library
+ (name libASL_support)
+ (public_name asli.libASL-support)
+ (libraries libASL_ast)
+ (virtual_modules solver))

libASL/support/native/dune

@@ -0,0 +1,4 @@
+(library
+ (name libASL_native)
+ (implements libASL_support)
+ (libraries z3 libASL_ast))

libASL/support/native/solver.ml

@@ -0,0 +1,78 @@
+(****************************************************************)
+(** {3 Z3 support code}                                         *)
+(****************************************************************)
+
+(** Convert ASL expression to Z3 expression.
+    This only copes with a limited set of operations: ==, +, -, * and DIV.
+    (It is possible that we will need to extend this list in the future but
+    it is sufficient for the current ASL specifications.)
+
+    The support for DIV is not sound - it is a hack needed to cope with
+    the way ASL code is written and generally needs a side condition
+    that the division is exact (no remainder).
+
+    ufs is a mutable list of conversions used to handle subexpressions
+    that cannot be translated.  We treat such subexpressions as
+    uninterpreted functions and add them to the 'ufs' list so that
+    we can reason that "F(x) == F(x)" without knowing "F".
+ *)
+
+module AST = Asl_ast
+
+let verbose = false
+
+let rec z3_of_expr (ctx: Z3.context) (ufs: (AST.expr * Z3.Expr.expr) list ref) (x: AST.expr): Z3.Expr.expr =
+    (match x with
+    | Expr_Var(v) ->
+        let intsort = Z3.Arithmetic.Integer.mk_sort ctx in
+        Z3.Expr.mk_const_s ctx (AST.pprint_ident v) intsort
+    | Expr_Parens y -> z3_of_expr ctx ufs y
+    | Expr_LitInt i -> Z3.Arithmetic.Integer.mk_numeral_s ctx i
+
+    (* todo: the following lines involving DIV are not sound *)
+    | Expr_TApply (FIdent ("mul_int",_), [], [Expr_TApply (FIdent ("fdiv_int",_), [], [a; b]); c]) when b = c -> z3_of_expr ctx ufs a
+    | Expr_TApply (FIdent ("mul_int",_), [], [a; Expr_TApply (FIdent ("fdiv_int",_), [], [b; c])]) when a = c -> z3_of_expr ctx ufs b
+    | Expr_TApply (FIdent ("add_int",_), [], [Expr_TApply (FIdent ("fdiv_int",_), [], [a1; b1]);
+                                         Expr_TApply (FIdent ("fdiv_int",_), [], [a2; b2])])
+         when a1 = a2 && b1 = b2 && b1 = Expr_LitInt "2"
+         -> z3_of_expr ctx ufs a1
+    | Expr_TApply (FIdent ("eq_int",_), [], [a; Expr_TApply (FIdent ("fdiv_int",_), [], [b; c])]) ->
+            Z3.Boolean.mk_eq ctx
+                (Z3.Arithmetic.mk_mul ctx [z3_of_expr ctx ufs c; z3_of_expr ctx ufs a])
+                (z3_of_expr ctx ufs b)
+
+    | Expr_TApply (FIdent ("add_int",_),  [], xs)    -> Z3.Arithmetic.mk_add ctx (List.map (z3_of_expr ctx ufs) xs)
+    | Expr_TApply (FIdent ("sub_int",_),  [], xs)    -> Z3.Arithmetic.mk_sub ctx (List.map (z3_of_expr ctx ufs) xs)
+    | Expr_TApply (FIdent ("mul_int",_),  [], xs)    -> Z3.Arithmetic.mk_mul ctx (List.map (z3_of_expr ctx ufs) xs)
+    | Expr_TApply (FIdent ("fdiv_int",_), [], [a;b]) -> Z3.Arithmetic.mk_div ctx (z3_of_expr ctx ufs a) (z3_of_expr ctx ufs b)
+    | Expr_TApply (FIdent ("eq_int",_),   [], [a;b]) -> Z3.Boolean.mk_eq ctx (z3_of_expr ctx ufs a) (z3_of_expr ctx ufs b)
+    | _ ->
+            if verbose then Printf.printf "    Unable to translate %s - using as uninterpreted function\n" (Asl_utils.pp_expr x);
+            let intsort = Z3.Arithmetic.Integer.mk_sort ctx in
+            (match List.assoc_opt x !ufs with
+            | None ->
+                    let uf = Z3.Expr.mk_fresh_const ctx "UNINTERPRETED" intsort in
+                    ufs := (x, uf) :: !ufs;
+                    uf
+            | Some uf ->
+                    uf
+            )
+    )
+
+(** check that bs => cs *)
+let check_constraints (bs: AST.expr list) (cs: AST.expr list): bool =
+    (* note that we rebuild the Z3 context each time.
+     * It is possible to share them across all invocations to save
+     * about 10% of execution time.
+     *)
+    let z3_ctx = Z3.mk_context [] in
+    let solver = Z3.Solver.mk_simple_solver z3_ctx in
+    let ufs = ref [] in (* uninterpreted function list *)
+    let bs' = List.map (z3_of_expr z3_ctx ufs) bs in
+    let cs' = List.map (z3_of_expr z3_ctx ufs) cs in
+    let p = Z3.Boolean.mk_implies z3_ctx (Z3.Boolean.mk_and z3_ctx bs') (Z3.Boolean.mk_and z3_ctx cs') in
+    if verbose then Printf.printf "      - Checking %s\n" (Z3.Expr.to_string p);
+    Z3.Solver.add solver [Z3.Boolean.mk_not z3_ctx p];
+    let q = Z3.Solver.check solver [] in
+    if q = SATISFIABLE then Printf.printf "Failed property %s\n" (Z3.Expr.to_string p);
+    q = UNSATISFIABLE

libASL/support/solver.mli

@@ -0,0 +1,6 @@
+(****************************************************************)
+(** {3 Z3 support code}                                         *)
+(****************************************************************)
+
+(** check that bs => cs *)
+val check_constraints : (Asl_ast.expr list) -> (Asl_ast.expr list) -> bool

libASL/tcheck.ml

@@ -709,83 +709,14 @@ let rec simplify_expr (x: AST.expr): AST.expr =
 (** Perform simple constant folding of expressions within a type *)
 let simplify_type (x: AST.ty): AST.ty =
     let repl = new replaceExprClass (fun e -> Some (simplify_expr e)) in
-    Asl_visitor.visit_type repl x
-
+    Visitor.visit_type repl x
 
 (****************************************************************)
-(** {3 Z3 support code}                                         *)
+(** {3 Constraint solver entry point}                           *)
 (****************************************************************)
 
-(** Convert ASL expression to Z3 expression.
-    This only copes with a limited set of operations: ==, +, -, * and DIV.
-    (It is possible that we will need to extend this list in the future but
-    it is sufficient for the current ASL specifications.)
-
-    The support for DIV is not sound - it is a hack needed to cope with
-    the way ASL code is written and generally needs a side condition
-    that the division is exact (no remainder).
-
-    ufs is a mutable list of conversions used to handle subexpressions
-    that cannot be translated.  We treat such subexpressions as
-    uninterpreted functions and add them to the 'ufs' list so that
-    we can reason that "F(x) == F(x)" without knowing "F".
- *)
-
-let rec z3_of_expr (ctx: Z3.context) (ufs: (AST.expr * Z3.Expr.expr) list ref) (x: AST.expr): Z3.Expr.expr =
-    (match x with
-    | Expr_Var(v) ->
-        let intsort = Z3.Arithmetic.Integer.mk_sort ctx in
-        Z3.Expr.mk_const_s ctx (pprint_ident v) intsort
-    | Expr_Parens y -> z3_of_expr ctx ufs y
-    | Expr_LitInt i -> Z3.Arithmetic.Integer.mk_numeral_s ctx i
-
-    (* todo: the following lines involving DIV are not sound *)
-    | Expr_TApply (FIdent ("mul_int",_), [], [Expr_TApply (FIdent ("fdiv_int",_), [], [a; b]); c]) when b = c -> z3_of_expr ctx ufs a
-    | Expr_TApply (FIdent ("mul_int",_), [], [a; Expr_TApply (FIdent ("fdiv_int",_), [], [b; c])]) when a = c -> z3_of_expr ctx ufs b
-    | Expr_TApply (FIdent ("add_int",_), [], [Expr_TApply (FIdent ("fdiv_int",_), [], [a1; b1]);
-                                         Expr_TApply (FIdent ("fdiv_int",_), [], [a2; b2])])
-         when a1 = a2 && b1 = b2 && b1 = Expr_LitInt "2"
-         -> z3_of_expr ctx ufs a1
-    | Expr_TApply (FIdent ("eq_int",_), [], [a; Expr_TApply (FIdent ("fdiv_int",_), [], [b; c])]) ->
-            Z3.Boolean.mk_eq ctx
-                (Z3.Arithmetic.mk_mul ctx [z3_of_expr ctx ufs c; z3_of_expr ctx ufs a])
-                (z3_of_expr ctx ufs b)
-
-    | Expr_TApply (FIdent ("add_int",_),  [], xs)    -> Z3.Arithmetic.mk_add ctx (List.map (z3_of_expr ctx ufs) xs)
-    | Expr_TApply (FIdent ("sub_int",_),  [], xs)    -> Z3.Arithmetic.mk_sub ctx (List.map (z3_of_expr ctx ufs) xs)
-    | Expr_TApply (FIdent ("mul_int",_),  [], xs)    -> Z3.Arithmetic.mk_mul ctx (List.map (z3_of_expr ctx ufs) xs)
-    | Expr_TApply (FIdent ("fdiv_int",_), [], [a;b]) -> Z3.Arithmetic.mk_div ctx (z3_of_expr ctx ufs a) (z3_of_expr ctx ufs b)
-    | Expr_TApply (FIdent ("eq_int",_),   [], [a;b]) -> Z3.Boolean.mk_eq ctx (z3_of_expr ctx ufs a) (z3_of_expr ctx ufs b)
-    | _ ->
-            if verbose then Printf.printf "    Unable to translate %s - using as uninterpreted function\n" (pp_expr x);
-            let intsort = Z3.Arithmetic.Integer.mk_sort ctx in
-            (match List.assoc_opt x !ufs with
-            | None ->
-                    let uf = Z3.Expr.mk_fresh_const ctx "UNINTERPRETED" intsort in
-                    ufs := (x, uf) :: !ufs;
-                    uf
-            | Some uf ->
-                    uf
-            )
-    )
-
-(** check that bs => cs *)
 let check_constraints (bs: expr list) (cs: expr list): bool =
-    (* note that we rebuild the Z3 context each time.
-     * It is possible to share them across all invocations to save
-     * about 10% of execution time.
-     *)
-    let z3_ctx = Z3.mk_context [] in
-    let solver = Z3.Solver.mk_simple_solver z3_ctx in
-    let ufs = ref [] in (* uninterpreted function list *)
-    let bs' = List.map (z3_of_expr z3_ctx ufs) bs in
-    let cs' = List.map (z3_of_expr z3_ctx ufs) cs in
-    let p = Z3.Boolean.mk_implies z3_ctx (Z3.Boolean.mk_and z3_ctx bs') (Z3.Boolean.mk_and z3_ctx cs') in
-    if verbose then Printf.printf "      - Checking %s\n" (Z3.Expr.to_string p);
-    Z3.Solver.add solver [Z3.Boolean.mk_not z3_ctx p];
-    let q = Z3.Solver.check solver [] in
-    if q = SATISFIABLE then Printf.printf "Failed property %s\n" (Z3.Expr.to_string p);
-    q = UNSATISFIABLE
+    LibASL_support.Solver.check_constraints bs cs
 
 
 (****************************************************************)
@@ -897,7 +828,7 @@ class unifier (loc: AST.l) (assumptions: expr list) = object (self)
             (* attempt to close an expression by replacing all fresh vars with a closed expression *)
         and close_expr (x: expr): expr option =
             let subst = new substFunClass (fun x -> if self#isFresh x then Some (close_ident x) else None) in
-            let x'    = Asl_visitor.visit_expr subst x in
+            let x'    = Visitor.visit_expr subst x in
             if isClosed x' then
                 Some x'
             else
@@ -1027,8 +958,8 @@ let unify_ixtype (u: unifier) (ty1: AST.ixtype) (ty2: AST.ixtype): unit =
 let rec unify_type (env: GlobalEnv.t) (u: unifier) (ty1: AST.ty) (ty2: AST.ty): unit =
     (* Substitute global constants in types *)
     let subst_consts = new substFunClass (GlobalEnv.getConstant env) in
-    let ty1' = Asl_visitor.visit_type subst_consts ty1 in
-    let ty2' = Asl_visitor.visit_type subst_consts ty2 in
+    let ty1' = Visitor.visit_type subst_consts ty1 in
+    let ty2' = Visitor.visit_type subst_consts ty2 in
     (match (derefType env ty1', derefType env ty2') with
     | (Type_Constructor c1,       Type_Constructor c2)       -> ()
     | (Type_Bits(e1),             Type_Bits(e2))             -> u#addEquality e1 e2
@@ -2521,7 +2452,7 @@ let env0 = GlobalEnv.mkempty ()
 
 (** Typecheck a list of declarations - main entrypoint into typechecker *)
 let tc_declarations (isPrelude: bool) (ds: AST.declaration list): AST.declaration list =
-    if verbose then Printf.printf "  - Using Z3 %s\n" Z3.Version.to_string;
+    (* if verbose then Printf.printf "  - Using Z3 %s\n" Z3.Version.to_string; *)
     (* Process declarations, starting by moving all function definitions to the
      * end of the list and replacing them with function prototypes.
      * As long as the type/var decls are all sorted correctly, this

offlineASL/decode_tests.ml

@@ -0,0 +1,4 @@
+(* AUTO-GENERATED LIFTER FILE *)
+
+open Offline_utils
+

offlineASL/dune

@@ -1,6 +1,11 @@
+; AUTO-GENERATED BY OCAML BACKEND
 (library
   (name offlineASL)
   (flags
-    (:standard -w -27 -cclib -lstdc++))
-  (modules offline utils)
-  (libraries zarith libASL))
+    (:standard -w -27 -w -33 -cclib -lstdc++))
+  (modules 
+    offline
+    decode_tests
+    offline_utils
+  )
+  (libraries libASL))

offlineASL/offline.ml

@@ -1,4 +1,7 @@
-open Utils
+(* AUTO-GENERATED LIFTER FILE *)
+
+open Offline_utils
+open Decode_tests
 
 let f_A64_decoder v_enc : unit = 
   failwith "unsupported"

tests/dune

@@ -1,4 +1,4 @@
 (test (name test_asl)
  (modes exe)
  (flags (-cclib -lstdc++))
- (libraries alcotest libASL))
+ (libraries alcotest libASL libASL_native))