--- a/src/Pure/General/sha1.ML Fri Mar 18 16:38:40 2016 +0100
+++ b/src/Pure/General/sha1.ML Fri Mar 18 17:11:30 2016 +0100
@@ -1,8 +1,8 @@
(* Title: Pure/General/sha1.ML
Author: Makarius
+ Author: Sascha Boehme, TU Muenchen
-Digesting strings according to SHA-1 (see RFC 3174) -- relatively slow
-version in pure ML.
+Digesting strings according to SHA-1 (see RFC 3174).
*)
signature SHA1 =
@@ -11,11 +11,16 @@
val digest: string -> digest
val rep: digest -> string
val fake: string -> digest
+ val test_samples: unit -> unit
end;
structure SHA1: SHA1 =
struct
+(** internal implementation in ML -- relatively slow **)
+
+local
+
(* 32bit words *)
infix 4 << >>;
@@ -45,7 +50,7 @@
(* padding *)
-fun pack_bytes 0 n = ""
+fun pack_bytes 0 _ = ""
| pack_bytes k n = pack_bytes (k - 1) (n div 256) ^ chr (n mod 256);
fun padded_text str =
@@ -61,7 +66,7 @@
in ((len + size padding) div 4, word) end;
-(* digest_string *)
+(* digest_string_internal *)
fun digest_word (i, w, {a, b, c, d, e}) =
let
@@ -87,7 +92,9 @@
e = d}
end;
-fun digest_string str =
+in
+
+fun digest_string_internal str =
let
val (text_len, text) = padded_text str;
@@ -129,16 +136,89 @@
val hex = hex_word o hash;
in hex 0 ^ hex 1 ^ hex 2 ^ hex 3 ^ hex 4 end;
+end;
-(* type digest *)
+
+(** external implementation in C **)
+
+local
+
+(* digesting *)
+
+fun hex_digit i = if i < 10 then chr (ord "0" + i) else chr (ord "a" + i - 10);
+
+fun hex_string arr i =
+ let val c = CInterface.fromCchar (CInterface.offset i CInterface.Cchar arr)
+ in (op ^) (apply2 hex_digit (Integer.div_mod (Char.ord c) 16)) end
+
+val lib_path =
+ ("$ML_HOME/" ^ (if ML_System.platform_is_windows then "sha1.dll" else "libsha1.so"))
+ |> Path.explode;
+
+val STRING_INPUT_BYTES =
+ CInterface.mkConversion undefined (CInterface.toCbytes o Byte.stringToBytes)
+ (CInterface.Cpointer CInterface.Cchar);
+
+in
+
+fun digest_string_external str =
+ let
+ val digest = CInterface.alloc 20 CInterface.Cchar;
+ val _ =
+ CInterface.call3
+ (CInterface.get_sym (File.platform_path lib_path) "sha1_buffer")
+ (STRING_INPUT_BYTES, CInterface.LONG, CInterface.POINTER)
+ CInterface.POINTER (str, size str, CInterface.address digest);
+ in fold (suffix o hex_string digest) (0 upto 19) "" end;
+
+end;
+
+
+
+(** type digest **)
datatype digest = Digest of string;
-val digest = Digest o digest_string;
fun rep (Digest s) = s;
-
val fake = Digest;
val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Pretty.str o quote o rep);
+fun digest_string str = digest_string_external str
+ handle CInterface.Foreign msg =>
+ (warning (msg ^ "\nUsing slow ML implementation of SHA1.digest"); digest_string_internal str);
+
+val digest = Digest o digest_string;
+
+
+
+(** SHA1 samples found in the wild **)
+
+local
+
+fun check (msg, key) =
+ let val key' = rep (digest msg) in
+ if key = key' then ()
+ else
+ raise Fail ("SHA1 library integrity test failed on " ^ quote msg ^ ":\n" ^
+ key ^ " expected, but\n" ^ key' ^ " was found")
+ end;
+
+in
+
+fun test_samples () =
+ List.app check
+ [("", "da39a3ee5e6b4b0d3255bfef95601890afd80709"),
+ ("a", "86f7e437faa5a7fce15d1ddcb9eaeaea377667b8"),
+ ("abc", "a9993e364706816aba3e25717850c26c9cd0d89d"),
+ ("abcdefghijklmnopqrstuvwxyz", "32d10c7b8cf96570ca04ce37f2a19d84240d3a89"),
+ ("The quick brown fox jumps over the lazy dog", "2fd4e1c67a2d28fced849ee1bb76e7391b93eb12"),
+ (replicate_string 100 "\000", "ed4a77d1b56a118938788fc53037759b6c501e3d"),
+ ("a\000b", "4a3dec2d1f8245280855c42db0ee4239f917fdb8"),
+ ("\000\001", "3f29546453678b855931c174a97d6c0894b8f546")];
+
end;
+
+val _ = test_samples ();
+
+end;
--- a/src/Pure/General/sha1_polyml.ML Fri Mar 18 16:38:40 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-(* Title: Pure/General/sha1_polyml.ML
- Author: Sascha Boehme, TU Muenchen
-
-Digesting strings according to SHA-1 (see RFC 3174) -- based on an
-external implementation in C with a fallback to an internal
-implementation.
-*)
-
-structure SHA1: SHA1 =
-struct
-
-(* digesting *)
-
-fun hex_digit i = if i < 10 then chr (ord "0" + i) else chr (ord "a" + i - 10);
-
-fun hex_string arr i =
- let val c = CInterface.fromCchar (CInterface.offset i CInterface.Cchar arr)
- in (op ^) (apply2 hex_digit (Integer.div_mod (Char.ord c) 16)) end
-
-val lib_path =
- ("$ML_HOME/" ^ (if ML_System.platform_is_windows then "sha1.dll" else "libsha1.so"))
- |> Path.explode;
-
-val STRING_INPUT_BYTES =
- CInterface.mkConversion undefined (CInterface.toCbytes o Byte.stringToBytes)
- (CInterface.Cpointer CInterface.Cchar);
-
-fun digest_external str =
- let
- val digest = CInterface.alloc 20 CInterface.Cchar;
- val _ =
- CInterface.call3
- (CInterface.get_sym (File.platform_path lib_path) "sha1_buffer")
- (STRING_INPUT_BYTES, CInterface.LONG, CInterface.POINTER)
- CInterface.POINTER (str, size str, CInterface.address digest);
- in fold (suffix o hex_string digest) (0 upto 19) "" end;
-
-fun digest_string str = digest_external str
- handle CInterface.Foreign msg =>
- (warning (msg ^ "\nUsing slow ML implementation of SHA1.digest"); SHA1.rep (SHA1.digest str));
-
-
-(* type digest *)
-
-datatype digest = Digest of string;
-
-val digest = Digest o digest_string;
-fun rep (Digest s) = s;
-
-val fake = Digest;
-
-end;
--- a/src/Pure/General/sha1_samples.ML Fri Mar 18 16:38:40 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-(* Title: Pure/General/sha1_samples.ML
- Author: Makarius
-
-Some SHA1 samples found in the wild.
-*)
-
-signature SHA1_SAMPLES =
-sig
- val test: unit -> unit
-end;
-
-structure SHA1_Samples: SHA1_SAMPLES =
-struct
-
-fun check (msg, key) =
- let val key' = SHA1.rep (SHA1.digest msg) in
- if key = key' then ()
- else
- raise Fail ("SHA1 library integrity test failed on " ^ quote msg ^ ":\n" ^
- key ^ " expected, but\n" ^ key' ^ " was found")
- end;
-
-fun test () =
- List.app check
- [("", "da39a3ee5e6b4b0d3255bfef95601890afd80709"),
- ("a", "86f7e437faa5a7fce15d1ddcb9eaeaea377667b8"),
- ("abc", "a9993e364706816aba3e25717850c26c9cd0d89d"),
- ("abcdefghijklmnopqrstuvwxyz", "32d10c7b8cf96570ca04ce37f2a19d84240d3a89"),
- ("The quick brown fox jumps over the lazy dog", "2fd4e1c67a2d28fced849ee1bb76e7391b93eb12"),
- (replicate_string 100 "\000", "ed4a77d1b56a118938788fc53037759b6c501e3d"),
- ("a\000b", "4a3dec2d1f8245280855c42db0ee4239f917fdb8"),
- ("\000\001", "3f29546453678b855931c174a97d6c0894b8f546")];
-
-val _ = test ();
-
-end;
--- a/src/Pure/ROOT Fri Mar 18 16:38:40 2016 +0100
+++ b/src/Pure/ROOT Fri Mar 18 17:11:30 2016 +0100
@@ -50,8 +50,6 @@
"General/secure.ML"
"General/seq.ML"
"General/sha1.ML"
- "General/sha1_polyml.ML"
- "General/sha1_samples.ML"
"General/socket_io.ML"
"General/source.ML"
"General/stack.ML"
--- a/src/Pure/ROOT.ML Fri Mar 18 16:38:40 2016 +0100
+++ b/src/Pure/ROOT.ML Fri Mar 18 17:11:30 2016 +0100
@@ -143,10 +143,7 @@
use "General/socket_io.ML";
use "General/seq.ML";
use "General/timing.ML";
-
use "General/sha1.ML";
-use "General/sha1_polyml.ML";
-use "General/sha1_samples.ML";
val _ = List.app ML_Name_Space.forget_structure ML_Name_Space.critical_structures;
--- a/src/Pure/System/isabelle_process.ML Fri Mar 18 16:38:40 2016 +0100
+++ b/src/Pure/System/isabelle_process.ML Fri Mar 18 17:11:30 2016 +0100
@@ -190,7 +190,7 @@
val init_protocol = uninterruptible (fn _ => fn socket =>
let
- val _ = SHA1_Samples.test ()
+ val _ = SHA1.test_samples ()
handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn);
val _ = Output.physical_stderr Symbol.STX;
--- a/src/Pure/Tools/build.ML Fri Mar 18 16:38:40 2016 +0100
+++ b/src/Pure/Tools/build.ML Fri Mar 18 17:11:30 2016 +0100
@@ -122,7 +122,7 @@
fun build args_file =
let
- val _ = SHA1_Samples.test ();
+ val _ = SHA1.test_samples ();
val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
(document_files, (graph_file, (parent_name, (chapter, (name, theories)))))))))) =