added Cache_IO: cache for output of external tools,
authorboehmes
Tue Feb 16 15:25:36 2010 +0100 (2010-02-16)
changeset 35151117247018b54
parent 35150 082fa4bd403d
child 35152 6007909a28bc
added Cache_IO: cache for output of external tools,
changed SMT solver interface to use Cache_IO
etc/components
src/HOL/IsaMakefile
src/HOL/SMT/SMT_Base.thy
src/HOL/SMT/Tools/smt_solver.ML
src/HOL/SMT/lib/scripts/run_smt_solver
src/Tools/Cache_IO/cache_io.ML
src/Tools/Cache_IO/etc/settings
src/Tools/Cache_IO/lib/scripts/compute_hash_key
     1.1 --- a/etc/components	Tue Feb 16 15:16:33 2010 +0100
     1.2 +++ b/etc/components	Tue Feb 16 15:25:36 2010 +0100
     1.3 @@ -13,6 +13,7 @@
     1.4  #misc components
     1.5  src/Tools/Code
     1.6  src/Tools/WWW_Find
     1.7 +src/Tools/Cache_IO
     1.8  src/HOL/Tools/ATP_Manager
     1.9  src/HOL/Mirabelle
    1.10  src/HOL/Library/Sum_Of_Squares
     2.1 --- a/src/HOL/IsaMakefile	Tue Feb 16 15:16:33 2010 +0100
     2.2 +++ b/src/HOL/IsaMakefile	Tue Feb 16 15:25:36 2010 +0100
     2.3 @@ -1226,7 +1226,8 @@
     2.4    SMT/Tools/smt_solver.ML SMT/Tools/cvc3_solver.ML                      \
     2.5    SMT/Tools/yices_solver.ML SMT/Tools/z3_proof_terms.ML                 \
     2.6    SMT/Tools/z3_proof_rules.ML SMT/Tools/z3_proof.ML                     \
     2.7 -  SMT/Tools/z3_model.ML SMT/Tools/z3_interface.ML SMT/Tools/z3_solver.ML
     2.8 +  SMT/Tools/z3_model.ML SMT/Tools/z3_interface.ML			\
     2.9 +  SMT/Tools/z3_solver.ML $(SRC)/Tools/Cache_IO/cache_io.ML
    2.10  	@cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT
    2.11  
    2.12  
     3.1 --- a/src/HOL/SMT/SMT_Base.thy	Tue Feb 16 15:16:33 2010 +0100
     3.2 +++ b/src/HOL/SMT/SMT_Base.thy	Tue Feb 16 15:25:36 2010 +0100
     3.3 @@ -8,6 +8,7 @@
     3.4  imports Real "~~/src/HOL/Word/Word"
     3.5    "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
     3.6  uses
     3.7 +  "~~/src/Tools/Cache_IO/cache_io.ML"
     3.8    ("Tools/smt_normalize.ML")
     3.9    ("Tools/smt_monomorph.ML")
    3.10    ("Tools/smt_translate.ML")
     4.1 --- a/src/HOL/SMT/Tools/smt_solver.ML	Tue Feb 16 15:16:33 2010 +0100
     4.2 +++ b/src/HOL/SMT/Tools/smt_solver.ML	Tue Feb 16 15:25:36 2010 +0100
     4.3 @@ -28,8 +28,10 @@
     4.4    val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
     4.5    val trace: bool Config.T
     4.6    val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
     4.7 +
     4.8 +  (*certificates*)
     4.9    val record: bool Config.T
    4.10 -  val certificates: string Config.T
    4.11 +  val select_certificates: string -> Context.generic -> Context.generic
    4.12  
    4.13    (*solvers*)
    4.14    type solver = Proof.context -> thm list -> thm
    4.15 @@ -88,30 +90,29 @@
    4.16  fun trace_msg ctxt f x =
    4.17    if Config.get ctxt trace then tracing (f x) else ()
    4.18  
    4.19 +
    4.20 +(* SMT certificates *)
    4.21 +
    4.22  val (record, setup_record) = Attrib.config_bool "smt_record" true
    4.23 -val no_certificates = ""
    4.24 -val (certificates, setup_certificates) =
    4.25 -  Attrib.config_string "smt_certificates" no_certificates
    4.26  
    4.27 +structure Certificates = Generic_Data
    4.28 +(
    4.29 +  type T = Cache_IO.cache option
    4.30 +  val empty = NONE
    4.31 +  val extend = I
    4.32 +  fun merge (s, _) = s
    4.33 +)
    4.34 +
    4.35 +fun select_certificates name = Certificates.put (
    4.36 +  if name = "" then NONE
    4.37 +  else SOME (Cache_IO.make (Path.explode name)))
    4.38  
    4.39  
    4.40  (* interface to external solvers *)
    4.41  
    4.42  local
    4.43  
    4.44 -fun with_files ctxt f =
    4.45 -  let
    4.46 -    val paths as (problem_path, proof_path) =
    4.47 -      "smt-" ^ serial_string ()
    4.48 -      |> (fn n => (n, n ^ ".proof"))
    4.49 -      |> pairself (File.tmp_path o Path.explode)
    4.50 -
    4.51 -    val y = Exn.capture f (problem_path, proof_path)
    4.52 -
    4.53 -    val _ = pairself (try File.rm) paths
    4.54 -  in Exn.release y end
    4.55 -
    4.56 -fun invoke ctxt output f (paths as (problem_path, proof_path)) =
    4.57 +fun invoke ctxt output f problem_path =
    4.58    let
    4.59      fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
    4.60        (map Pretty.str ls))
    4.61 @@ -120,11 +121,10 @@
    4.62      val _ = trace_msg ctxt (pretty "SMT problem:" o split_lines o File.read)
    4.63        problem_path
    4.64  
    4.65 -    val (s, _) = with_timeout ctxt f paths
    4.66 -    val _ = trace_msg ctxt (pretty "SMT solver:") (split_lines s)
    4.67 +    val (res, err) = with_timeout ctxt f problem_path
    4.68 +    val _ = trace_msg ctxt (pretty "SMT solver:") err
    4.69  
    4.70 -    fun lines_of path = the_default [] (try (File.fold_lines cons path) [])
    4.71 -    val ls = rev (dropwhile (equal "") (lines_of proof_path))
    4.72 +    val ls = rev (dropwhile (equal "") (rev res))
    4.73      val _ = trace_msg ctxt (pretty "SMT result:") ls
    4.74    in (x, ls) end
    4.75  
    4.76 @@ -135,37 +135,40 @@
    4.77      val remote_url = getenv "REMOTE_SMT_URL"
    4.78    in
    4.79      if local_solver <> ""
    4.80 -    then (["local", local_solver],
    4.81 -      "Invoking local SMT solver " ^ quote local_solver ^ " ...")
    4.82 -    else if remote_solver <> "" andalso remote_url <> ""
    4.83 -    then (["remote", remote_solver],
    4.84 -      "Invoking remote SMT solver " ^ quote remote_solver ^ " at " ^
    4.85 -      quote remote_url ^ " ...")
    4.86 +    then 
    4.87 +     (tracing ("Invoking local SMT solver " ^ quote local_solver ^ " ...");
    4.88 +      [local_solver])
    4.89 +    else if remote_solver <> ""
    4.90 +    then
    4.91 +     (tracing ("Invoking remote SMT solver " ^ quote remote_solver ^ " at " ^
    4.92 +        quote remote_url ^ " ...");
    4.93 +      [getenv "REMOTE_SMT", remote_solver])
    4.94      else error ("Undefined Isabelle environment variable: " ^ quote env_var)
    4.95    end
    4.96  
    4.97 -fun run ctxt cmd args (problem_path, proof_path) =
    4.98 -  let
    4.99 -    val certs = Config.get ctxt certificates
   4.100 -    val certs' = 
   4.101 -      if certs = no_certificates then "-"
   4.102 -      else File.shell_path (Path.explode certs)
   4.103 -    val (solver, msg) =
   4.104 -      if certs = no_certificates orelse Config.get ctxt record
   4.105 -      then choose cmd
   4.106 -      else (["certificate"], "Using certificate from " ^ quote certs' ^ " ...")
   4.107 -    val _ = tracing msg
   4.108 +fun make_cmd solver args problem_path proof_path = space_implode " " (
   4.109 +  map File.shell_quote (solver @ args) @
   4.110 +  [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])
   4.111 +
   4.112 +fun no_cmd _ _ = error ("Bad certificates cache: missing certificate")
   4.113 +
   4.114 +fun run ctxt cmd args problem_path =
   4.115 +  let val certs = Certificates.get (Context.Proof ctxt)
   4.116    in
   4.117 -    bash_output (space_implode " " (
   4.118 -      File.shell_path (Path.explode (getenv "RUN_SMT_SOLVER")) :: certs' ::
   4.119 -      map File.shell_quote (solver @ args) @
   4.120 -      map File.shell_path [problem_path, proof_path]) ^ " 2>&1")
   4.121 +    if is_none certs 
   4.122 +    then Cache_IO.run' (make_cmd (choose cmd) args) problem_path
   4.123 +    else if Config.get ctxt record
   4.124 +    then Cache_IO.cached' (the certs) (make_cmd (choose cmd) args) problem_path
   4.125 +    else
   4.126 +     (tracing ("Using cached certificate from " ^
   4.127 +        File.shell_path (Cache_IO.cache_path_of (the certs)) ^ " ...");
   4.128 +      Cache_IO.cached' (the certs) no_cmd problem_path)
   4.129    end
   4.130  
   4.131  in
   4.132  
   4.133  fun run_solver ctxt cmd args output =
   4.134 -  with_files ctxt (invoke ctxt output (run ctxt cmd args))
   4.135 +  Cache_IO.with_tmp_file "smt-" (invoke ctxt output (run ctxt cmd args))
   4.136  
   4.137  end
   4.138  
   4.139 @@ -278,7 +281,10 @@
   4.140    setup_timeout #>
   4.141    setup_trace #>
   4.142    setup_record #>
   4.143 -  setup_certificates #>
   4.144 +  Attrib.setup (Binding.name "smt_certificates")
   4.145 +    (Scan.lift (OuterParse.$$$ "=" |-- Args.name) >>
   4.146 +      (Thm.declaration_attribute o K o select_certificates))
   4.147 +    "SMT certificates" #>
   4.148    Method.setup (Binding.name "smt") smt_method
   4.149      "Applies an SMT solver to the current goal."
   4.150  
     5.1 --- a/src/HOL/SMT/lib/scripts/run_smt_solver	Tue Feb 16 15:16:33 2010 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,93 +0,0 @@
     5.4 -#!/usr/bin/env perl
     5.5 -#
     5.6 -# Author: Sascha Boehme, TU Muenchen
     5.7 -#
     5.8 -# Cache for prover results, based on discriminating problems using MD5.
     5.9 -
    5.10 -use strict;
    5.11 -use warnings;
    5.12 -use Digest::MD5;
    5.13 -
    5.14 -
    5.15 -# arguments
    5.16 -
    5.17 -my $certs_file = shift @ARGV;
    5.18 -my $location = shift @ARGV;
    5.19 -my $result_file = pop @ARGV;
    5.20 -my $problem_file = $ARGV[-1];
    5.21 -
    5.22 -my $use_certs = not ($certs_file eq "-");
    5.23 -
    5.24 -
    5.25 -# create MD5 problem digest
    5.26 -
    5.27 -my $problem_digest = "";
    5.28 -if ($use_certs) {
    5.29 -  my $md5 = Digest::MD5->new;
    5.30 -  open FILE, "<$problem_file" or
    5.31 -    die "ERROR: Failed to open '$problem_file' ($!)";
    5.32 -  $md5->addfile(*FILE);
    5.33 -  close FILE;
    5.34 -  $problem_digest = $md5->b64digest;
    5.35 -}
    5.36 -
    5.37 -
    5.38 -# lookup problem digest among existing certificates and
    5.39 -# return a cached result (if there is a certificate for the problem)
    5.40 -
    5.41 -if ($use_certs and -e $certs_file) {
    5.42 -  my $cached = 0;
    5.43 -  open CERTS, "<$certs_file" or die "ERROR: Failed to open '$certs_file' ($!)";
    5.44 -  while (<CERTS>) {
    5.45 -    if (m/(\S+) (\d+)/) {
    5.46 -      if ($1 eq $problem_digest) {
    5.47 -        my $start = tell CERTS;
    5.48 -        open FILE, ">$result_file" or
    5.49 -          die "ERROR: Failed to open '$result_file ($!)";
    5.50 -        while ((tell CERTS) - $start < $2) {
    5.51 -          my $line = <CERTS>;
    5.52 -          print FILE $line;
    5.53 -        }
    5.54 -        close FILE;
    5.55 -        $cached = 1;
    5.56 -        last;
    5.57 -      }
    5.58 -      else { seek CERTS, $2, 1; }
    5.59 -    }
    5.60 -    else { die "ERROR: Invalid file format in '$certs_file'"; }
    5.61 -  }
    5.62 -  close CERTS;
    5.63 -  if ($cached) { exit 0; }
    5.64 -}
    5.65 -
    5.66 -
    5.67 -# invoke (remote or local) prover
    5.68 -
    5.69 -my $result;
    5.70 -
    5.71 -if ($location eq "remote") {
    5.72 -  $result = system "$ENV{'REMOTE_SMT'} @ARGV >$result_file 2>&1";
    5.73 -}
    5.74 -elsif ($location eq "local") {
    5.75 -  $result = system "@ARGV >$result_file 2>&1";
    5.76 -}
    5.77 -else { die "ERROR: No SMT solver invoked"; }
    5.78 -
    5.79 -
    5.80 -# cache result
    5.81 -
    5.82 -if ($use_certs) {
    5.83 -  open CERTS, ">>$certs_file" or
    5.84 -    die "ERROR: Failed to open '$certs_file' ($!)";
    5.85 -  print CERTS
    5.86 -    ("$problem_digest " . ((-s $result_file) + (length "\n")) . "\n");
    5.87 -
    5.88 -  open FILE, "<$result_file" or
    5.89 -    die "ERROR: Failed to open '$result_file' ($!)";
    5.90 -  foreach (<FILE>) { print CERTS $_; }
    5.91 -  close FILE; 
    5.92 -
    5.93 -  print CERTS "\n";
    5.94 -  close CERTS;
    5.95 -}
    5.96 -
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Tools/Cache_IO/cache_io.ML	Tue Feb 16 15:25:36 2010 +0100
     6.3 @@ -0,0 +1,121 @@
     6.4 +(*  Title:      Tools/Cache_IO/cache_io.ML
     6.5 +    Author:     Sascha Boehme, TU Muenchen
     6.6 +
     6.7 +Cache for output of external processes.
     6.8 +*)
     6.9 +
    6.10 +signature CACHE_IO =
    6.11 +sig
    6.12 +  val with_tmp_file: string -> (Path.T -> 'a) -> 'a
    6.13 +  val run: (Path.T -> string) -> Path.T -> string list
    6.14 +  val run': (Path.T -> Path.T -> string) -> Path.T -> string list * string list
    6.15 +
    6.16 +  type cache
    6.17 +  val make: Path.T -> cache
    6.18 +  val cache_path_of: cache -> Path.T
    6.19 +  val cached: cache -> (Path.T -> string) -> Path.T -> string list
    6.20 +  val cached': cache -> (Path.T -> Path.T -> string) -> Path.T ->
    6.21 +    string list * string list
    6.22 +end
    6.23 +
    6.24 +structure Cache_IO : CACHE_IO =
    6.25 +struct
    6.26 +
    6.27 +fun with_tmp_file name f =
    6.28 +  let
    6.29 +    val path = File.tmp_path (Path.explode (name ^ serial_string ()))
    6.30 +    val x = Exn.capture f path
    6.31 +    val _ = try File.rm path
    6.32 +  in Exn.release x end
    6.33 +
    6.34 +fun run' make_cmd in_path =
    6.35 +  with_tmp_file "cache-io-" (fn out_path =>
    6.36 +    let
    6.37 +      val (out2, _) = bash_output (make_cmd in_path out_path)
    6.38 +      val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
    6.39 +    in (out1, split_lines out2) end)
    6.40 +
    6.41 +fun run make_cmd = snd o run' (fn in_path => fn _ => make_cmd in_path)
    6.42 +
    6.43 +
    6.44 +
    6.45 +abstype cache = Cache of {
    6.46 +  path: Path.T,
    6.47 +  table: (int * (int * int * int) Symtab.table) Synchronized.var }
    6.48 +with
    6.49 +
    6.50 +
    6.51 +fun cache_path_of (Cache {path, ...}) = path
    6.52 +
    6.53 +
    6.54 +fun load cache_path =
    6.55 +  let
    6.56 +    fun err () = error ("Cache IO: corrupted cache file: " ^
    6.57 +      File.shell_path cache_path)
    6.58 +
    6.59 +    fun int_of_string s =
    6.60 +      (case read_int (explode s) of
    6.61 +        (i, []) => i
    6.62 +      | _ => err ())    
    6.63 +
    6.64 +    fun split line =
    6.65 +      (case space_explode " " line of
    6.66 +        [key, len1, len2] => (key, int_of_string len1, int_of_string len2)
    6.67 +      | _ => err ())
    6.68 +
    6.69 +    fun parse line ((i, l), tab) =
    6.70 +      if i = l
    6.71 +      then
    6.72 +        let val (key, l1, l2) = split line
    6.73 +        in ((i+1, l+l1+l2+1), Symtab.update (key, (i+1, l1, l2)) tab) end
    6.74 +      else ((i+1, l), tab)
    6.75 +  in apfst fst (File.fold_lines parse cache_path ((1, 1), Symtab.empty)) end 
    6.76 +
    6.77 +fun make path =
    6.78 +  let val table = if File.exists path then load path else (1, Symtab.empty)
    6.79 +  in Cache {path=path, table=Synchronized.var (Path.implode path) table} end
    6.80 +
    6.81 +
    6.82 +fun get_hash_key path =
    6.83 +  let
    6.84 +    val arg = File.shell_path path
    6.85 +    val (out, res) = bash_output (getenv "COMPUTE_HASH_KEY" ^ " " ^ arg)
    6.86 +  in
    6.87 +    if res = 0 then hd (split_lines out)
    6.88 +    else error ("Cache IO: failed to generate hash key for file " ^ arg)
    6.89 +  end
    6.90 +
    6.91 +fun load_cached_result cache_path (p, len1, len2) =
    6.92 +  let
    6.93 +    fun load line (i, xsp) =
    6.94 +      if i < p then (i+1, xsp)
    6.95 +      else if i < p + len1 then (i+1, apfst (cons line) xsp)
    6.96 +      else if i < p + len2 then (i+1, apsnd (cons line) xsp)
    6.97 +      else (i, xsp)
    6.98 +  in pairself rev (snd (File.fold_lines load cache_path (1, ([], [])))) end
    6.99 +
   6.100 +fun cached' (Cache {path=cache_path, table}) make_cmd in_path =
   6.101 +  let val key = get_hash_key in_path
   6.102 +  in
   6.103 +    (case Symtab.lookup (snd (Synchronized.value table)) key of
   6.104 +      SOME pos => load_cached_result cache_path pos
   6.105 +    | NONE =>
   6.106 +        let
   6.107 +          val res as (out, err) = run' make_cmd in_path
   6.108 +          val (l1, l2) = pairself length res
   6.109 +          val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
   6.110 +          val lines = map (suffix "\n") (header :: out @ err)
   6.111 +
   6.112 +          val _ = Synchronized.change table (fn (p, tab) =>
   6.113 +            if Symtab.defined tab key then (p, tab)
   6.114 +            else
   6.115 +              let val _ = File.append_list cache_path lines
   6.116 +              in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
   6.117 +        in res end)
   6.118 +  end
   6.119 +
   6.120 +fun cached cache make_cmd =
   6.121 +  snd o cached' cache (fn in_path => fn _ => make_cmd in_path)
   6.122 +
   6.123 +end
   6.124 +end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Tools/Cache_IO/etc/settings	Tue Feb 16 15:25:36 2010 +0100
     7.3 @@ -0,0 +1,4 @@
     7.4 +ISABELLE_CACHE_IO="$COMPONENT"
     7.5 +
     7.6 +COMPUTE_HASH_KEY="$ISABELLE_CACHE_IO/lib/scripts/compute_hash_key"
     7.7 +
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Tools/Cache_IO/lib/scripts/compute_hash_key	Tue Feb 16 15:25:36 2010 +0100
     8.3 @@ -0,0 +1,24 @@
     8.4 +#!/usr/bin/env perl
     8.5 +#
     8.6 +# Author: Sascha Boehme, TU Muenchen
     8.7 +#
     8.8 +# Compute MD5 hash key.
     8.9 +
    8.10 +use strict;
    8.11 +use warnings;
    8.12 +use Digest::MD5;
    8.13 +
    8.14 +
    8.15 +# argument
    8.16 +
    8.17 +my $file = $ARGV[0];
    8.18 +
    8.19 +
    8.20 +# compute MD5 hash key
    8.21 +
    8.22 +my $md5 = Digest::MD5->new;
    8.23 +open FILE, "<$file" or die "ERROR: Failed to open '$file' ($!)";
    8.24 +$md5->addfile(*FILE);
    8.25 +close FILE;
    8.26 +print $md5->b64digest . "\n";
    8.27 +