added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
authorwenzelm
Mon Aug 26 21:56:08 2013 +0200 (2013-08-26 ago)
changeset 53212387b9f7cb0ac
parent 53211 753b9fbe18be
child 53213 a11e55f667db
added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
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 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/General/sha1_samples.ML	Mon Aug 26 21:56:08 2013 +0200
     1.3 @@ -0,0 +1,35 @@
     1.4 +(*  Title:      Pure/General/sha1_samples.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Some SHA1 samples found in the wild.
     1.8 +*)
     1.9 +
    1.10 +signature SHA1_SAMPLES =
    1.11 +sig
    1.12 +  val test: unit -> unit
    1.13 +end;
    1.14 +
    1.15 +structure SHA1_Samples: SHA1_SAMPLES =
    1.16 +struct
    1.17 +
    1.18 +fun check (msg, key) =
    1.19 +  let val key' = SHA1.rep (SHA1.digest msg) in
    1.20 +    if key = key' then ()
    1.21 +    else
    1.22 +      raise Fail ("SHA1 library integrity test failed on " ^ quote msg ^ ":\n" ^
    1.23 +        key ^ " expected, but\n" ^ key' ^ " was found")
    1.24 +  end;
    1.25 +
    1.26 +fun test () =
    1.27 +  List.app check
    1.28 +   [("", "da39a3ee5e6b4b0d3255bfef95601890afd80709"),
    1.29 +    ("a", "86f7e437faa5a7fce15d1ddcb9eaeaea377667b8"),
    1.30 +    ("abc", "a9993e364706816aba3e25717850c26c9cd0d89d"),
    1.31 +    ("abcdefghijklmnopqrstuvwxyz", "32d10c7b8cf96570ca04ce37f2a19d84240d3a89"),
    1.32 +    ("The quick brown fox jumps over the lazy dog", "2fd4e1c67a2d28fced849ee1bb76e7391b93eb12"),
    1.33 +    (replicate_string 100 "\000", "ed4a77d1b56a118938788fc53037759b6c501e3d"),
    1.34 +    ("a\000b", "4a3dec2d1f8245280855c42db0ee4239f917fdb8")];
    1.35 +
    1.36 +val _ = test ();
    1.37 +
    1.38 +end;
     2.1 --- a/src/Pure/ROOT	Mon Aug 26 21:53:56 2013 +0200
     2.2 +++ b/src/Pure/ROOT	Mon Aug 26 21:56:08 2013 +0200
     2.3 @@ -91,6 +91,7 @@
     2.4      "General/seq.ML"
     2.5      "General/sha1.ML"
     2.6      "General/sha1_polyml.ML"
     2.7 +    "General/sha1_samples.ML"
     2.8      "General/socket_io.ML"
     2.9      "General/source.ML"
    2.10      "General/stack.ML"
     3.1 --- a/src/Pure/ROOT.ML	Mon Aug 26 21:53:56 2013 +0200
     3.2 +++ b/src/Pure/ROOT.ML	Mon Aug 26 21:56:08 2013 +0200
     3.3 @@ -59,6 +59,7 @@
     3.4  
     3.5  use "General/sha1.ML";
     3.6  if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();
     3.7 +use "General/sha1_samples.ML";
     3.8  
     3.9  use "PIDE/xml.ML";
    3.10  use "PIDE/yxml.ML";
     4.1 --- a/src/Pure/System/isabelle_process.ML	Mon Aug 26 21:53:56 2013 +0200
     4.2 +++ b/src/Pure/System/isabelle_process.ML	Mon Aug 26 21:56:08 2013 +0200
     4.3 @@ -187,6 +187,8 @@
     4.4  
     4.5  val init = uninterruptible (fn _ => fn rendezvous =>
     4.6    let
     4.7 +    val _ = SHA1_Samples.test ()
     4.8 +      handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); reraise exn);
     4.9      val _ = Output.physical_stderr Symbol.STX;
    4.10  
    4.11      val _ = Printer.show_markup_default := true;
     5.1 --- a/src/Pure/Tools/build.ML	Mon Aug 26 21:53:56 2013 +0200
     5.2 +++ b/src/Pure/Tools/build.ML	Mon Aug 26 21:56:08 2013 +0200
     5.3 @@ -127,6 +127,8 @@
     5.4  
     5.5  fun build args_file = Command_Line.tool (fn () =>
     5.6      let
     5.7 +      val _ = SHA1_Samples.test ();
     5.8 +
     5.9        val (command_timings, (do_output, (options, (verbose, (browser_info,
    5.10            (parent_name, (chapter, (name, theories)))))))) =
    5.11          File.read (Path.explode args_file) |> YXML.parse_body |>