src/Tools/cache_io.ML
author blanchet
Mon, 15 Sep 2014 10:49:07 +0200
changeset 58335 a5a3b576fcfb
parent 50317 4d1590544b91
child 59058 a78612c67ec0
permissions -rw-r--r--
generate 'code' attribute only if 'code' plugin is enabled
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35942
667fd8553cd5 use internal SHA1 digest implementation for generating hash keys
boehmes
parents: 35941
diff changeset
     1
(*  Title:      Tools/cache_io.ML
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
     3
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
     4
Cache for output of external processes.
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
     5
*)
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
     6
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
     7
signature CACHE_IO =
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
     8
sig
40425
c9b5e0fcee31 return the process return code along with the process outputs
boehmes
parents: 37740
diff changeset
     9
  (*IO wrapper*)
40538
b8482ff0bc92 check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents: 40425
diff changeset
    10
  type result = {
b8482ff0bc92 check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents: 40425
diff changeset
    11
    output: string list,
b8482ff0bc92 check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents: 40425
diff changeset
    12
    redirected_output: string list,
b8482ff0bc92 check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents: 40425
diff changeset
    13
    return_code: int}
50316
wenzelm
parents: 43850
diff changeset
    14
  val raw_run: (Path.T -> Path.T -> string) -> string -> Path.T -> Path.T -> result
40538
b8482ff0bc92 check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents: 40425
diff changeset
    15
  val run: (Path.T -> Path.T -> string) -> string -> result
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    16
40425
c9b5e0fcee31 return the process return code along with the process outputs
boehmes
parents: 37740
diff changeset
    17
  (*cache*)
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    18
  type cache
50317
4d1590544b91 synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic);
wenzelm
parents: 50316
diff changeset
    19
  val unsynchronized_init: Path.T -> cache
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    20
  val cache_path_of: cache -> Path.T
40538
b8482ff0bc92 check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents: 40425
diff changeset
    21
  val lookup: cache -> string -> result option * string
50316
wenzelm
parents: 43850
diff changeset
    22
  val run_and_cache: cache -> string -> (Path.T -> Path.T -> string) -> string -> result
40538
b8482ff0bc92 check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents: 40425
diff changeset
    23
  val run_cached: cache -> (Path.T -> Path.T -> string) -> string -> result
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    24
end
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    25
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    26
structure Cache_IO : CACHE_IO =
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    27
struct
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    28
40425
c9b5e0fcee31 return the process return code along with the process outputs
boehmes
parents: 37740
diff changeset
    29
(* IO wrapper *)
c9b5e0fcee31 return the process return code along with the process outputs
boehmes
parents: 37740
diff changeset
    30
36086
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
    31
val cache_io_prefix = "cache-io-"
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
    32
40538
b8482ff0bc92 check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents: 40425
diff changeset
    33
type result = {
b8482ff0bc92 check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents: 40425
diff changeset
    34
  output: string list,
b8482ff0bc92 check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents: 40425
diff changeset
    35
  redirected_output: string list,
b8482ff0bc92 check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents: 40425
diff changeset
    36
  return_code: int}
b8482ff0bc92 check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents: 40425
diff changeset
    37
40578
2b098a549450 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents: 40538
diff changeset
    38
fun raw_run make_cmd str in_path out_path =
2b098a549450 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents: 40538
diff changeset
    39
  let
2b098a549450 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents: 40538
diff changeset
    40
    val _ = File.write in_path str
43850
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 42127
diff changeset
    41
    val (out2, rc) = Isabelle_System.bash_output (make_cmd in_path out_path)
40578
2b098a549450 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents: 40538
diff changeset
    42
    val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
50316
wenzelm
parents: 43850
diff changeset
    43
  in {output = split_lines out2, redirected_output = out1, return_code = rc} end
40578
2b098a549450 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents: 40538
diff changeset
    44
36086
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
    45
fun run make_cmd str =
42127
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41954
diff changeset
    46
  Isabelle_System.with_tmp_file cache_io_prefix "" (fn in_path =>
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 41954
diff changeset
    47
    Isabelle_System.with_tmp_file cache_io_prefix "" (fn out_path =>
41307
bb8468ae414e slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents: 40743
diff changeset
    48
      raw_run make_cmd str in_path out_path))
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    49
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    50
40425
c9b5e0fcee31 return the process return code along with the process outputs
boehmes
parents: 37740
diff changeset
    51
(* cache *)
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    52
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    53
abstype cache = Cache of {
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    54
  path: Path.T,
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    55
  table: (int * (int * int * int) Symtab.table) Synchronized.var }
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    56
with
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    57
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    58
fun cache_path_of (Cache {path, ...}) = path
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    59
50317
4d1590544b91 synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic);
wenzelm
parents: 50316
diff changeset
    60
fun unsynchronized_init cache_path =
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    61
  let
50316
wenzelm
parents: 43850
diff changeset
    62
    val table =
wenzelm
parents: 43850
diff changeset
    63
      if File.exists cache_path then
wenzelm
parents: 43850
diff changeset
    64
        let
wenzelm
parents: 43850
diff changeset
    65
          fun err () = error ("Cache IO: corrupted cache file: " ^ File.shell_path cache_path)
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    66
50316
wenzelm
parents: 43850
diff changeset
    67
          fun int_of_string s =
wenzelm
parents: 43850
diff changeset
    68
            (case read_int (raw_explode s) of
wenzelm
parents: 43850
diff changeset
    69
              (i, []) => i
wenzelm
parents: 43850
diff changeset
    70
            | _ => err ())
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    71
50316
wenzelm
parents: 43850
diff changeset
    72
          fun split line =
wenzelm
parents: 43850
diff changeset
    73
            (case space_explode " " line of
wenzelm
parents: 43850
diff changeset
    74
              [key, len1, len2] => (key, int_of_string len1, int_of_string len2)
wenzelm
parents: 43850
diff changeset
    75
            | _ => err ())
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    76
50316
wenzelm
parents: 43850
diff changeset
    77
          fun parse line ((i, l), tab) =
wenzelm
parents: 43850
diff changeset
    78
            if i = l
wenzelm
parents: 43850
diff changeset
    79
            then
wenzelm
parents: 43850
diff changeset
    80
              let val (key, l1, l2) = split line
wenzelm
parents: 43850
diff changeset
    81
              in ((i+1, l+l1+l2+1), Symtab.update (key, (i+1, l1, l2)) tab) end
wenzelm
parents: 43850
diff changeset
    82
            else ((i+1, l), tab)
wenzelm
parents: 43850
diff changeset
    83
        in apfst fst (File.fold_lines parse cache_path ((1, 1), Symtab.empty)) end
wenzelm
parents: 43850
diff changeset
    84
      else (1, Symtab.empty)
wenzelm
parents: 43850
diff changeset
    85
  in Cache {path = cache_path, table = Synchronized.var "Cache_IO" table} end
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    86
50316
wenzelm
parents: 43850
diff changeset
    87
fun lookup (Cache {path = cache_path, table}) str =
41954
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 41945
diff changeset
    88
  let val key = SHA1.rep (SHA1.digest str)
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    89
  in
50317
4d1590544b91 synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic);
wenzelm
parents: 50316
diff changeset
    90
    Synchronized.change_result table (fn tab =>
4d1590544b91 synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic);
wenzelm
parents: 50316
diff changeset
    91
      (case Symtab.lookup (snd tab) key of
4d1590544b91 synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic);
wenzelm
parents: 50316
diff changeset
    92
        NONE => ((NONE, key), tab)
4d1590544b91 synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic);
wenzelm
parents: 50316
diff changeset
    93
      | SOME (p, len1, len2) =>
4d1590544b91 synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic);
wenzelm
parents: 50316
diff changeset
    94
          let
4d1590544b91 synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic);
wenzelm
parents: 50316
diff changeset
    95
            fun load line (i, xsp) =
4d1590544b91 synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic);
wenzelm
parents: 50316
diff changeset
    96
              if i < p then (i+1, xsp)
4d1590544b91 synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic);
wenzelm
parents: 50316
diff changeset
    97
              else if i < p + len1 then (i+1, apfst (cons line) xsp)
4d1590544b91 synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic);
wenzelm
parents: 50316
diff changeset
    98
              else if i < p + len2 then (i+1, apsnd (cons line) xsp)
4d1590544b91 synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic);
wenzelm
parents: 50316
diff changeset
    99
              else (i, xsp)
4d1590544b91 synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic);
wenzelm
parents: 50316
diff changeset
   100
            val (out, err) =
4d1590544b91 synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic);
wenzelm
parents: 50316
diff changeset
   101
              pairself rev (snd (File.fold_lines load cache_path (1, ([], []))))
4d1590544b91 synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic);
wenzelm
parents: 50316
diff changeset
   102
          in ((SOME {output = err, redirected_output = out, return_code = 0}, key), tab) end))
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
   103
  end
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
   104
50316
wenzelm
parents: 43850
diff changeset
   105
fun run_and_cache (Cache {path = cache_path, table}) key make_cmd str =
36086
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
   106
  let
50316
wenzelm
parents: 43850
diff changeset
   107
    val {output = err, redirected_output=out, return_code} = run make_cmd str
40538
b8482ff0bc92 check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents: 40425
diff changeset
   108
    val (l1, l2) = pairself length (out, err)
36086
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
   109
    val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
   110
    val lines = map (suffix "\n") (header :: out @ err)
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
   111
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
   112
    val _ = Synchronized.change table (fn (p, tab) =>
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
   113
      if Symtab.defined tab key then (p, tab)
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
   114
      else
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
   115
        let val _ = File.append_list cache_path lines
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
   116
        in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
50316
wenzelm
parents: 43850
diff changeset
   117
  in {output = err, redirected_output = out, return_code = return_code} end
36086
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
   118
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
   119
fun run_cached cache make_cmd str =
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
   120
  (case lookup cache str of
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
   121
    (NONE, key) => run_and_cache cache key make_cmd str
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
   122
  | (SOME output, _) => output)
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
   123
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
   124
end
40425
c9b5e0fcee31 return the process return code along with the process outputs
boehmes
parents: 37740
diff changeset
   125
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
   126
end