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