src/Tools/Spec_Check/spec_check.ML
author wenzelm
Fri Aug 23 12:40:55 2013 +0200 (2013-08-23)
changeset 53164 beb4ee344c22
parent 52278 src/HOL/Spec_Check/spec_check.ML@39d60668f8df
child 60956 10d463883dc2
permissions -rw-r--r--
clarified position of Spec_Check for Isabelle/ML -- it is unrelated to Isabelle/HOL;
just one src/Tools/ROOT;
     1 (*  Title:      Tools/Spec_Check/spec_check.ML
     2     Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
     3     Author:     Christopher League
     4 
     5 Specification-based testing of ML programs with random values.
     6 *)
     7 
     8 signature SPEC_CHECK =
     9 sig
    10   val gen_target : int Config.T
    11   val gen_max : int Config.T
    12   val examples : int Config.T
    13   val sort_examples : bool Config.T
    14   val show_stats : bool Config.T
    15   val column_width : int Config.T
    16   val style : string Config.T
    17 
    18   type output_style = Proof.context -> string ->
    19     {status : string option * Property.result * (Property.stats  * string option list) -> unit,
    20      finish: Property.stats * string option list -> unit}
    21 
    22   val register_style : string -> output_style -> theory -> theory
    23 
    24   val checkGen : Proof.context ->
    25     'a Generator.gen * ('a -> string) option -> string * 'a Property.prop -> unit
    26 
    27   val check_property : Proof.context -> string -> unit
    28 end;
    29 
    30 structure Spec_Check : SPEC_CHECK =
    31 struct
    32 
    33 (* configurations *)
    34 
    35 val gen_target = Attrib.setup_config_int @{binding spec_check_gen_target} (K 100)
    36 val gen_max = Attrib.setup_config_int @{binding spec_check_gen_max} (K 400)
    37 val examples = Attrib.setup_config_int @{binding spec_check_examples} (K 5)
    38 
    39 val sort_examples = Attrib.setup_config_bool @{binding spec_check_sort_examples} (K true)
    40 val show_stats = Attrib.setup_config_bool @{binding spec_check_show_stats} (K true)
    41 val column_width = Attrib.setup_config_int @{binding spec_check_column_width} (K 22)
    42 val style = Attrib.setup_config_string @{binding spec_check_style} (K "Perl")
    43 
    44 type ('a, 'b) reader = 'b -> ('a * 'b) option
    45 type 'a rep = ('a -> string) option
    46 
    47 type output_style = Proof.context -> string ->
    48   {status: string option * Property.result * (Property.stats * string option list) -> unit,
    49    finish: Property.stats * string option list -> unit}
    50 
    51 fun limit ctxt gen = Generator.limit (Config.get ctxt gen_max) gen
    52 
    53 structure Style = Theory_Data
    54 (
    55   type T = output_style Symtab.table
    56   val empty = Symtab.empty
    57   val extend = I
    58   fun merge data : T = Symtab.merge (K true) data
    59 )
    60 
    61 fun get_style ctxt =
    62   let val name = Config.get ctxt style in
    63     (case Symtab.lookup (Style.get (Proof_Context.theory_of ctxt)) name of
    64       SOME style => style ctxt
    65     | NONE => error ("No style called " ^ quote name ^ " found"))
    66   end
    67 
    68 fun register_style name style = Style.map (Symtab.update (name, style))
    69 
    70 
    71 (* testing functions *)
    72 
    73 fun cpsCheck ctxt s0 shrink (next, show) (tag, prop) =
    74   let
    75     val apply_show = case show of NONE => (fn _ => NONE) | SOME f => SOME o f
    76 
    77     val {status, finish} = get_style ctxt tag
    78     fun status' (obj, result, (stats, badobjs)) =
    79       let
    80         val badobjs' = if Property.failure result then obj :: badobjs else badobjs
    81         val _ = status (apply_show obj, result, (stats, map apply_show badobjs'))
    82       in badobjs' end
    83 
    84     fun try_shrink (obj, result, stats') (stats, badobjs) =
    85       let
    86         fun is_failure s =
    87           let val (result, stats') = Property.test prop (s, stats)
    88           in if Property.failure result then SOME (s, result, stats') else NONE end
    89       in
    90         case get_first is_failure (shrink obj) of
    91           SOME (obj, result, stats') => try_shrink (obj, result, stats') (stats, badobjs)
    92         | NONE => status' (obj, result, (stats', badobjs))
    93       end
    94 
    95     fun iter (NONE, (stats, badobjs)) = finish (stats, map apply_show badobjs)
    96       | iter (SOME (obj, stream), (stats, badobjs)) =
    97         if #count stats >= Config.get ctxt gen_target then
    98           finish (stats, map apply_show badobjs)
    99         else
   100           let
   101             val (result, stats') = Property.test prop (obj, stats)
   102             val badobjs' = if Property.failure result then
   103                 try_shrink (obj, result, stats') (stats, badobjs)
   104               else
   105                 status' (obj, result, (stats', badobjs))
   106           in iter (next stream, (stats', badobjs')) end
   107   in
   108     fn stream => iter (next stream, (s0, []))
   109   end
   110 
   111 fun check' ctxt s0 = cpsCheck ctxt s0 (fn _ => [])
   112 fun check ctxt = check' ctxt Property.stats
   113 fun checks ctxt = cpsCheck ctxt Property.stats
   114 
   115 fun checkGen ctxt (gen, show) (tag, prop) =
   116   check' ctxt {count = 0, tags = [("__GEN", 0)]}
   117     (limit ctxt gen, show) (tag, prop) Generator.stream
   118 
   119 fun checkGenShrink ctxt shrink (gen, show) (tag, prop) =
   120   cpsCheck ctxt {count=0, tags=[("__GEN", 0)]} shrink
   121     (limit ctxt gen, show) (tag, prop) Generator.stream
   122 
   123 fun checkOne ctxt show (tag, prop) obj =
   124   check ctxt (List.getItem, show) (tag, prop) [obj]
   125 
   126 (*call the compiler and pass resulting type string to the parser*)
   127 fun determine_type ctxt s =
   128   let
   129     val return = Unsynchronized.ref "return"
   130     val use_context : use_context =
   131      {tune_source = #tune_source ML_Env.local_context,
   132       name_space = #name_space ML_Env.local_context,
   133       str_of_pos = #str_of_pos ML_Env.local_context,
   134       print = fn r => return := r,
   135       error = #error ML_Env.local_context}
   136     val _ =
   137       Context.setmp_thread_data (SOME (Context.Proof ctxt))
   138         (fn () => Secure.use_text use_context (0, "generated code") true s) ()
   139   in
   140     Gen_Construction.parse_pred (! return)
   141   end;
   142 
   143 (*call the compiler and run the test*)
   144 fun run_test ctxt s =
   145   Context.setmp_thread_data (SOME (Context.Proof ctxt))
   146     (fn () => Secure.use_text ML_Env.local_context (0, "generated code") false s) ();
   147 
   148 (*split input into tokens*)
   149 fun input_split s =
   150   let
   151     fun dot c = c = #"."
   152     fun space c = c = #" "
   153     val (head, code) = Substring.splitl (not o dot) (Substring.full s)
   154   in
   155    (String.tokens space (Substring.string head),
   156     Substring.string (Substring.dropl dot code))
   157   end;
   158 
   159 (*create the function from the input*)
   160 fun make_fun s =
   161   let
   162     val scan_param = Scan.one (fn s => s <> ";")
   163     fun parameters s = Scan.repeat1 scan_param s
   164     val p = $$ "ALL" |-- parameters
   165     val (split, code) = input_split s
   166     val stop = Scan.stopper (fn _ => ";") (fn s => s = ";");
   167     val (params, _) = Scan.finite stop p split
   168   in "fn (" ^ commas params ^ ") => " ^ code end;
   169 
   170 (*read input and perform the test*)
   171 fun gen_check_property check ctxt s =
   172   let
   173     val func = make_fun s
   174     val (_, ty) = determine_type ctxt func
   175   in run_test ctxt (check ctxt "Check" (ty, func)) end;
   176 
   177 val check_property = gen_check_property Gen_Construction.build_check
   178 (*val check_property_safe = gen_check_property Gen_Construction.safe_check*)
   179 
   180 (*perform test for specification function*)
   181 fun gen_check_property_f check ctxt s =
   182   let
   183     val (name, ty) = determine_type ctxt s
   184   in run_test ctxt (check ctxt name (ty, s)) end;
   185 
   186 val check_property_f = gen_check_property_f Gen_Construction.build_check
   187 (*val check_property_safe_f_ = gen_check_property_f Gen_Construction.safe_check*)
   188 
   189 end;
   190 
   191 fun check_property s = Spec_Check.check_property (ML_Context.the_local_context ()) s;
   192