clarified modules;
authorwenzelm
Fri Mar 18 17:11:30 2016 +0100 (2016-03-18)
changeset 6266600aff1da05ae
parent 62665 a78ce0c6e191
child 62667 254582abf067
clarified modules;
src/Pure/General/sha1.ML
src/Pure/General/sha1_polyml.ML
src/Pure/General/sha1_samples.ML
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/System/isabelle_process.ML
src/Pure/Tools/build.ML
     1.1 --- a/src/Pure/General/sha1.ML	Fri Mar 18 16:38:40 2016 +0100
     1.2 +++ b/src/Pure/General/sha1.ML	Fri Mar 18 17:11:30 2016 +0100
     1.3 @@ -1,8 +1,8 @@
     1.4  (*  Title:      Pure/General/sha1.ML
     1.5      Author:     Makarius
     1.6 +    Author:     Sascha Boehme, TU Muenchen
     1.7  
     1.8 -Digesting strings according to SHA-1 (see RFC 3174) -- relatively slow
     1.9 -version in pure ML.
    1.10 +Digesting strings according to SHA-1 (see RFC 3174).
    1.11  *)
    1.12  
    1.13  signature SHA1 =
    1.14 @@ -11,11 +11,16 @@
    1.15    val digest: string -> digest
    1.16    val rep: digest -> string
    1.17    val fake: string -> digest
    1.18 +  val test_samples: unit -> unit
    1.19  end;
    1.20  
    1.21  structure SHA1: SHA1 =
    1.22  struct
    1.23  
    1.24 +(** internal implementation in ML -- relatively slow **)
    1.25 +
    1.26 +local
    1.27 +
    1.28  (* 32bit words *)
    1.29  
    1.30  infix 4 << >>;
    1.31 @@ -45,7 +50,7 @@
    1.32  
    1.33  (* padding *)
    1.34  
    1.35 -fun pack_bytes 0 n = ""
    1.36 +fun pack_bytes 0 _ = ""
    1.37    | pack_bytes k n = pack_bytes (k - 1) (n div 256) ^ chr (n mod 256);
    1.38  
    1.39  fun padded_text str =
    1.40 @@ -61,7 +66,7 @@
    1.41    in ((len + size padding) div 4, word) end;
    1.42  
    1.43  
    1.44 -(* digest_string *)
    1.45 +(* digest_string_internal *)
    1.46  
    1.47  fun digest_word (i, w, {a, b, c, d, e}) =
    1.48    let
    1.49 @@ -87,7 +92,9 @@
    1.50       e = d}
    1.51    end;
    1.52  
    1.53 -fun digest_string str =
    1.54 +in
    1.55 +
    1.56 +fun digest_string_internal str =
    1.57    let
    1.58      val (text_len, text) = padded_text str;
    1.59  
    1.60 @@ -129,16 +136,89 @@
    1.61      val hex = hex_word o hash;
    1.62    in hex 0 ^ hex 1 ^ hex 2 ^ hex 3 ^ hex 4 end;
    1.63  
    1.64 +end;
    1.65  
    1.66 -(* type digest *)
    1.67 +
    1.68 +(** external implementation in C **)
    1.69 +
    1.70 +local
    1.71 +
    1.72 +(* digesting *)
    1.73 +
    1.74 +fun hex_digit i = if i < 10 then chr (ord "0" + i) else chr (ord "a" + i - 10);
    1.75 +
    1.76 +fun hex_string arr i =
    1.77 +  let val c = CInterface.fromCchar (CInterface.offset i CInterface.Cchar arr)
    1.78 +  in (op ^) (apply2 hex_digit (Integer.div_mod (Char.ord c) 16)) end
    1.79 +
    1.80 +val lib_path =
    1.81 +  ("$ML_HOME/" ^ (if ML_System.platform_is_windows then "sha1.dll" else "libsha1.so"))
    1.82 +  |> Path.explode;
    1.83 +
    1.84 +val STRING_INPUT_BYTES =
    1.85 +  CInterface.mkConversion undefined (CInterface.toCbytes o Byte.stringToBytes)
    1.86 +    (CInterface.Cpointer CInterface.Cchar);
    1.87 +
    1.88 +in
    1.89 +
    1.90 +fun digest_string_external str =
    1.91 +  let
    1.92 +    val digest = CInterface.alloc 20 CInterface.Cchar;
    1.93 +    val _ =
    1.94 +      CInterface.call3
    1.95 +        (CInterface.get_sym (File.platform_path lib_path) "sha1_buffer")
    1.96 +        (STRING_INPUT_BYTES, CInterface.LONG, CInterface.POINTER)
    1.97 +        CInterface.POINTER (str, size str, CInterface.address digest);
    1.98 +  in fold (suffix o hex_string digest) (0 upto 19) "" end;
    1.99 +
   1.100 +end;
   1.101 +
   1.102 +
   1.103 +
   1.104 +(** type digest **)
   1.105  
   1.106  datatype digest = Digest of string;
   1.107  
   1.108 -val digest = Digest o digest_string;
   1.109  fun rep (Digest s) = s;
   1.110 -
   1.111  val fake = Digest;
   1.112  
   1.113  val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Pretty.str o quote o rep);
   1.114  
   1.115 +fun digest_string str = digest_string_external str
   1.116 +  handle CInterface.Foreign msg =>
   1.117 +    (warning (msg ^ "\nUsing slow ML implementation of SHA1.digest"); digest_string_internal str);
   1.118 +
   1.119 +val digest = Digest o digest_string;
   1.120 +
   1.121 +
   1.122 +
   1.123 +(** SHA1 samples found in the wild **)
   1.124 +
   1.125 +local
   1.126 +
   1.127 +fun check (msg, key) =
   1.128 +  let val key' = rep (digest msg) in
   1.129 +    if key = key' then ()
   1.130 +    else
   1.131 +      raise Fail ("SHA1 library integrity test failed on " ^ quote msg ^ ":\n" ^
   1.132 +        key ^ " expected, but\n" ^ key' ^ " was found")
   1.133 +  end;
   1.134 +
   1.135 +in
   1.136 +
   1.137 +fun test_samples () =
   1.138 +  List.app check
   1.139 +   [("", "da39a3ee5e6b4b0d3255bfef95601890afd80709"),
   1.140 +    ("a", "86f7e437faa5a7fce15d1ddcb9eaeaea377667b8"),
   1.141 +    ("abc", "a9993e364706816aba3e25717850c26c9cd0d89d"),
   1.142 +    ("abcdefghijklmnopqrstuvwxyz", "32d10c7b8cf96570ca04ce37f2a19d84240d3a89"),
   1.143 +    ("The quick brown fox jumps over the lazy dog", "2fd4e1c67a2d28fced849ee1bb76e7391b93eb12"),
   1.144 +    (replicate_string 100 "\000", "ed4a77d1b56a118938788fc53037759b6c501e3d"),
   1.145 +    ("a\000b", "4a3dec2d1f8245280855c42db0ee4239f917fdb8"),
   1.146 +    ("\000\001", "3f29546453678b855931c174a97d6c0894b8f546")];
   1.147 +
   1.148  end;
   1.149 +
   1.150 +val _ = test_samples ();
   1.151 +
   1.152 +end;
     2.1 --- a/src/Pure/General/sha1_polyml.ML	Fri Mar 18 16:38:40 2016 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,52 +0,0 @@
     2.4 -(*  Title:      Pure/General/sha1_polyml.ML
     2.5 -    Author:     Sascha Boehme, TU Muenchen
     2.6 -
     2.7 -Digesting strings according to SHA-1 (see RFC 3174) -- based on an
     2.8 -external implementation in C with a fallback to an internal
     2.9 -implementation.
    2.10 -*)
    2.11 -
    2.12 -structure SHA1: SHA1 =
    2.13 -struct
    2.14 -
    2.15 -(* digesting *)
    2.16 -
    2.17 -fun hex_digit i = if i < 10 then chr (ord "0" + i) else chr (ord "a" + i - 10);
    2.18 -
    2.19 -fun hex_string arr i =
    2.20 -  let val c = CInterface.fromCchar (CInterface.offset i CInterface.Cchar arr)
    2.21 -  in (op ^) (apply2 hex_digit (Integer.div_mod (Char.ord c) 16)) end
    2.22 -
    2.23 -val lib_path =
    2.24 -  ("$ML_HOME/" ^ (if ML_System.platform_is_windows then "sha1.dll" else "libsha1.so"))
    2.25 -  |> Path.explode;
    2.26 -
    2.27 -val STRING_INPUT_BYTES =
    2.28 -  CInterface.mkConversion undefined (CInterface.toCbytes o Byte.stringToBytes)
    2.29 -    (CInterface.Cpointer CInterface.Cchar);
    2.30 -
    2.31 -fun digest_external str =
    2.32 -  let
    2.33 -    val digest = CInterface.alloc 20 CInterface.Cchar;
    2.34 -    val _ =
    2.35 -      CInterface.call3
    2.36 -        (CInterface.get_sym (File.platform_path lib_path) "sha1_buffer")
    2.37 -        (STRING_INPUT_BYTES, CInterface.LONG, CInterface.POINTER)
    2.38 -        CInterface.POINTER (str, size str, CInterface.address digest);
    2.39 -  in fold (suffix o hex_string digest) (0 upto 19) "" end;
    2.40 -
    2.41 -fun digest_string str = digest_external str
    2.42 -  handle CInterface.Foreign msg =>
    2.43 -    (warning (msg ^ "\nUsing slow ML implementation of SHA1.digest"); SHA1.rep (SHA1.digest str));
    2.44 -
    2.45 -
    2.46 -(* type digest *)
    2.47 -
    2.48 -datatype digest = Digest of string;
    2.49 -
    2.50 -val digest = Digest o digest_string;
    2.51 -fun rep (Digest s) = s;
    2.52 -
    2.53 -val fake = Digest;
    2.54 -
    2.55 -end;
     3.1 --- a/src/Pure/General/sha1_samples.ML	Fri Mar 18 16:38:40 2016 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,36 +0,0 @@
     3.4 -(*  Title:      Pure/General/sha1_samples.ML
     3.5 -    Author:     Makarius
     3.6 -
     3.7 -Some SHA1 samples found in the wild.
     3.8 -*)
     3.9 -
    3.10 -signature SHA1_SAMPLES =
    3.11 -sig
    3.12 -  val test: unit -> unit
    3.13 -end;
    3.14 -
    3.15 -structure SHA1_Samples: SHA1_SAMPLES =
    3.16 -struct
    3.17 -
    3.18 -fun check (msg, key) =
    3.19 -  let val key' = SHA1.rep (SHA1.digest msg) in
    3.20 -    if key = key' then ()
    3.21 -    else
    3.22 -      raise Fail ("SHA1 library integrity test failed on " ^ quote msg ^ ":\n" ^
    3.23 -        key ^ " expected, but\n" ^ key' ^ " was found")
    3.24 -  end;
    3.25 -
    3.26 -fun test () =
    3.27 -  List.app check
    3.28 -   [("", "da39a3ee5e6b4b0d3255bfef95601890afd80709"),
    3.29 -    ("a", "86f7e437faa5a7fce15d1ddcb9eaeaea377667b8"),
    3.30 -    ("abc", "a9993e364706816aba3e25717850c26c9cd0d89d"),
    3.31 -    ("abcdefghijklmnopqrstuvwxyz", "32d10c7b8cf96570ca04ce37f2a19d84240d3a89"),
    3.32 -    ("The quick brown fox jumps over the lazy dog", "2fd4e1c67a2d28fced849ee1bb76e7391b93eb12"),
    3.33 -    (replicate_string 100 "\000", "ed4a77d1b56a118938788fc53037759b6c501e3d"),
    3.34 -    ("a\000b", "4a3dec2d1f8245280855c42db0ee4239f917fdb8"),
    3.35 -    ("\000\001", "3f29546453678b855931c174a97d6c0894b8f546")];
    3.36 -
    3.37 -val _ = test ();
    3.38 -
    3.39 -end;
     4.1 --- a/src/Pure/ROOT	Fri Mar 18 16:38:40 2016 +0100
     4.2 +++ b/src/Pure/ROOT	Fri Mar 18 17:11:30 2016 +0100
     4.3 @@ -50,8 +50,6 @@
     4.4      "General/secure.ML"
     4.5      "General/seq.ML"
     4.6      "General/sha1.ML"
     4.7 -    "General/sha1_polyml.ML"
     4.8 -    "General/sha1_samples.ML"
     4.9      "General/socket_io.ML"
    4.10      "General/source.ML"
    4.11      "General/stack.ML"
     5.1 --- a/src/Pure/ROOT.ML	Fri Mar 18 16:38:40 2016 +0100
     5.2 +++ b/src/Pure/ROOT.ML	Fri Mar 18 17:11:30 2016 +0100
     5.3 @@ -143,10 +143,7 @@
     5.4  use "General/socket_io.ML";
     5.5  use "General/seq.ML";
     5.6  use "General/timing.ML";
     5.7 -
     5.8  use "General/sha1.ML";
     5.9 -use "General/sha1_polyml.ML";
    5.10 -use "General/sha1_samples.ML";
    5.11  
    5.12  val _ = List.app ML_Name_Space.forget_structure ML_Name_Space.critical_structures;
    5.13  
     6.1 --- a/src/Pure/System/isabelle_process.ML	Fri Mar 18 16:38:40 2016 +0100
     6.2 +++ b/src/Pure/System/isabelle_process.ML	Fri Mar 18 17:11:30 2016 +0100
     6.3 @@ -190,7 +190,7 @@
     6.4  
     6.5  val init_protocol = uninterruptible (fn _ => fn socket =>
     6.6    let
     6.7 -    val _ = SHA1_Samples.test ()
     6.8 +    val _ = SHA1.test_samples ()
     6.9        handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn);
    6.10      val _ = Output.physical_stderr Symbol.STX;
    6.11  
     7.1 --- a/src/Pure/Tools/build.ML	Fri Mar 18 16:38:40 2016 +0100
     7.2 +++ b/src/Pure/Tools/build.ML	Fri Mar 18 17:11:30 2016 +0100
     7.3 @@ -122,7 +122,7 @@
     7.4  
     7.5  fun build args_file =
     7.6    let
     7.7 -    val _ = SHA1_Samples.test ();
     7.8 +    val _ = SHA1.test_samples ();
     7.9  
    7.10      val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
    7.11            (document_files, (graph_file, (parent_name, (chapter, (name, theories)))))))))) =