products/sources/formale Sprachen/Isabelle/HOL/Mirabelle/Tools/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei:   Sprache: SML

Untersuchung Isabelle©
(*  Title:      HOL/Mirabelle/Tools/mirabelle.ML
    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
*)

signature MIRABELLE =
sig
  (*configuration*)
  val logfile : string Config.T
  val timeout : int Config.T
  val start_line : int Config.T
  val end_line : int Config.T

  (*core*)
  type init_action = int -> theory -> theory
  type done_args = {last: Toplevel.state, log: string -> unit}
  type done_action = int -> done_args -> unit
  type run_args = {pre: Proof.state, post: Toplevel.state option,
    timeout: Time.time, log: string -> unit, pos: Position.T, name: string}
  type run_action = int -> run_args -> unit
  type action = init_action * run_action * done_action
  val catch : (int -> string) -> run_action -> run_action
  val catch_result : (int -> string) -> 'a -> (int -> run_args -> 'a) ->
    int -> run_args -> 'a
  val register : action -> theory -> theory
  val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
    unit

  (*utility functions*)
  val can_apply : Time.time -> (Proof.context -> int -> tactic) ->
    Proof.state -> bool
  val theorems_in_proof_term : theory -> thm -> thm list
  val theorems_of_sucessful_proof : Toplevel.state option -> thm list
  val get_setting : (string * string) list -> string * string -> string
  val get_int_setting : (string * string) list -> string * int -> int
  val cpu_time : ('a -> 'b) -> 'a -> 'b * int
end



structure Mirabelle : MIRABELLE =
struct

(* Mirabelle configuration *)

val logfile = Attrib.setup_config_string \<^binding>\<open>mirabelle_logfile\<close> (K "")
val timeout = Attrib.setup_config_int \<^binding>\<open>mirabelle_timeout\<close> (K 30)
val start_line = Attrib.setup_config_int \<^binding>\<open>mirabelle_start_line\<close> (K 0)
val end_line = Attrib.setup_config_int \<^binding>\<open>mirabelle_end_line\<close> (K ~1)


(* Mirabelle core *)

type init_action = int -> theory -> theory
type done_args = {last: Toplevel.state, log: string -> unit}
type done_action = int -> done_args -> unit
type run_args = {pre: Proof.state, post: Toplevel.state option,
  timeout: Time.time, log: string -> unit, pos: Position.T, name: string}
type run_action = int -> run_args -> unit
type action = init_action * run_action * done_action

structure Actions = Theory_Data
(
  type T = (int * run_action * done_action) list
  val empty = []
  val extend = I
  fun merge data = Library.merge (K true) data  (* FIXME potential data loss because of (K true) *)
)


fun log_exn log tag id e = log (tag id ^ "exception:\n" ^ General.exnMessage e)

fun catch tag f id (st as {log, ...}: run_args) = (f id st; ())
  handle exn =>
    if Exn.is_interrupt exn then Exn.reraise exn else (log_exn log tag id exn; ())

fun catch_result tag d f id (st as {log, ...}: run_args) = f id st
  handle exn =>
    if Exn.is_interrupt exn then Exn.reraise exn else (log_exn log tag id exn; d)

fun register (init, run, done) thy =
  let val id = length (Actions.get thy) + 1
  in
    thy
    |> init id
    |> Actions.map (cons (id, run, done))
  end

local

fun log thy s =
  let fun append_to n = if n = "" then K () else File.append (Path.explode n)
  in append_to (Config.get_global thy logfile) (s ^ "\n") end
  (* FIXME: with multithreading and parallel proofs enabled, we might need to
     encapsulate this inside a critical section *)

fun log_sep thy = log thy "------------------"

fun apply_actions thy pos name info (pre, post, time) actions =
  let
    fun apply f = f {pre=pre, post=post, timeout=time, log=log thy, pos=pos, name=name}
    fun run (id, run, _) = (apply (run id); log_sep thy)
  in (log thy info; log_sep thy; List.app run actions) end

fun in_range _ _ NONE = true
  | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r))

fun only_within_range thy pos f x =
  let val l = Config.get_global thy start_line and r = Config.get_global thy end_line
  in if in_range l r (Position.line_of pos) then f x else () end

in

fun run_actions tr pre post =
  let
    val thy = Proof.theory_of pre
    val pos = Toplevel.pos_of tr
    val name = Toplevel.name_of tr
    val st = (pre, post, Time.fromSeconds (Config.get_global thy timeout))

    val str0 = string_of_int o the_default 0
    val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.offset_of pos)
    val info = "\n\nat " ^ loc ^ " (" ^ name ^ "):"
  in
    only_within_range thy pos (apply_actions thy pos name info st) (Actions.get thy)
  end

fun done_actions st =
  let
    val thy = Toplevel.theory_of st
    val _ = log thy "\n\n";
  in
    thy
    |> Actions.get
    |> List.app (fn (id, _, done) => done id {last=st, log=log thy})
  end

end

val whitelist = ["apply", "by", "proof"]

fun step_hook tr pre post =
 (* FIXME: might require wrapping into "interruptible" *)
  if can (Proof.assert_backward o Toplevel.proof_of) pre andalso
     member (op =) whitelist (Toplevel.name_of tr)
  then run_actions tr (Toplevel.proof_of pre) (SOME post)
  else if not (Toplevel.is_toplevel pre) andalso Toplevel.is_toplevel post
  then done_actions pre
  else ()   (* FIXME: add theory_hook here *)



(* Mirabelle utility functions *)

fun can_apply time tac st =
  let
    val {context = ctxt, facts, goal} = Proof.goal st
    val full_tac = HEADGOAL (Method.insert_tac ctxt facts THEN' tac ctxt)
  in
    (case try (Timeout.apply time (Seq.pull o full_tac)) goal of
      SOME (SOME _) => true
    | _ => false)
  end

local

fun fold_body_thms f =
  let
    fun app n (PBody {thms, ...}) = thms |> fold (fn (i, thm_node) =>
      fn (x, seen) =>
        if Inttab.defined seen i then (x, seen)
        else
          let
            val name = Proofterm.thm_node_name thm_node
            val prop = Proofterm.thm_node_prop thm_node
            val body = Future.join (Proofterm.thm_node_body thm_node)
            val (x', seen') = app (n + (if name = "" then 0 else 1)) body
              (x, Inttab.update (i, ()) seen)
        in (x' |> n = 0 ? f (name, prop, body), seen') end)
  in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end

in

fun theorems_in_proof_term thy thm =
  let
    val all_thms = Global_Theory.all_thms_of thy true
    fun collect (s, _, _) = if s <> "" then insert (op =) s else I
    fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE
    fun resolve_thms names = map_filter (member_of names) all_thms
  in
    resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] [])
  end

end

fun theorems_of_sucessful_proof state =
  (case state of
    NONE => []
  | SOME st =>
      if not (Toplevel.is_proof st) then []
      else
        theorems_in_proof_term (Toplevel.theory_of st) (#goal (Proof.goal (Toplevel.proof_of st))))

fun get_setting settings (key, default) =
  the_default default (AList.lookup (op =) settings key)

fun get_int_setting settings (key, default) =
  (case Option.map Int.fromString (AList.lookup (op =) settings key) of
    SOME (SOME i) => i
  | SOME NONE => error ("bad option: " ^ key)
  | NONE => default)

fun cpu_time f x =
  let val ({cpu, ...}, y) = Timing.timing f x
  in (y, Time.toMilliseconds cpu) end

end

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.66Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff