strategy_parser.mll 4.97 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
10
(********************************************************************)
11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29

{
  open Strategy

  exception SyntaxError of string

  let error f =
    Printf.kbprintf
      (fun b ->
        let s = Buffer.contents b in Buffer.clear b; raise (SyntaxError s))
      (Buffer.create 1024)
      f

  type label = {
    mutable defined: int option;
    temporary: int;
  }

  type 'a code = {
30 31
    env: Env.env;
    whyconf: Whyconf.config;
32 33 34 35 36 37
    mutable instr: instruction array;
    mutable next: int;
    labels: (string, label) Hashtbl.t; (* label name -> label *)
    mutable temp: int;
  }

38
  let create_code env conf =
39 40 41
    let h = Hashtbl.create 17 in
    Hashtbl.add h "exit" { defined = Some (-1); temporary = 0 };
    { env = env;
42
      whyconf = conf;
43 44 45 46
      instr = Array.make 10 (Igoto 0);
      next = 0;
      temp = 1;
      labels = h; }
47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83

  let enlarge_code code =
    let old = code.instr in
    let n = Array.length old in
    code.instr <- Array.make (2 * n) (Igoto 0);
    Array.blit old 0 code.instr 0 n

  let add_instr code i =
    let n = code.next in
    if n = Array.length code.instr then enlarge_code code;
    code.instr.(n) <- i;
    code.next <- n + 1

  let temp code =
    let t = code.temp in code.temp <- t + 1; t

  let define_label code l =
    let n = code.next in
    try
      let lab = Hashtbl.find code.labels l in
      if lab.defined = None then lab.defined <- Some n
      else error "duplicate label %s" l
    with Not_found ->
      let lab =  { defined = Some n; temporary = temp code } in
      Hashtbl.add code.labels l lab

  let find_label code l =
    try
      let lab = Hashtbl.find code.labels l in lab.temporary
    with Not_found ->
      let t = temp code in
      Hashtbl.add code.labels l { defined = None; temporary = t };
      t

  let prover code p =
    try
      let fp = Whyconf.parse_filter_prover p in
84
      Whyconf.filter_one_prover code.whyconf fp
85 86 87 88 89 90 91
    with
      | Whyconf.ProverNotFound _ ->
          error "Prover %S not installed or not configured" p
      | Whyconf.ProverAmbiguity _ ->
          error "Prover description %s is ambiguous" p

  let integer msg s =
92 93 94 95 96 97 98
    try Some (int_of_string s)
    with Failure _ ->
      match s with
      | "%t" -> None
      | "%m" -> None
      | _ ->
          error "unable to parse %s argument '%s'" msg s
99 100 101

  let transform code t =
    try
102
      ignore (Trans.lookup_transform t code.env)
103 104
    with Trans.UnknownTrans _ ->
    try
105
      ignore (Trans.lookup_transform_l t code.env)
106 107 108 109 110 111 112 113 114 115 116
    with Trans.UnknownTrans _->
      error "transformation %S is unknown" t

}

let space = [' ' '\t' '\r' '\n']
let ident = [^ ' ' '\t' '\r' '\n' ':' '#']+
let integer = ['0'-'9']+
let goto = 'g' | "goto"
let call = 'c' | "call"
let transform = 't' | "transform"
117 118
let timelimit = integer | "%t"
let memlimit = integer | "%m"
119 120 121 122 123 124 125 126 127 128 129 130

rule scan code = parse
  | space+
      { scan code lexbuf }
  | '#' [^ '\n']* ('\n' | eof)
      { scan code lexbuf }
  | ident as id ':'
      { define_label code id;
        scan code lexbuf }
  | goto space+ (ident as id)
      { add_instr code (Igoto (find_label code id));
        scan code lexbuf }
131
  | call space+ (ident as p) space+ (timelimit as t) space+ (memlimit as m)
132 133
      { let p = prover code p in
        let t = integer "timelimit" t in
134 135
        if t <> None && Opt.get t <= 0 then
          error "timelimit %d is invalid" (Opt.get t);
136
        let m = integer "memlimit" m in
137 138
        if m <> None && Opt.get m <= 0 then
          error "memlimit %d is invalid" (Opt.get m);
139
        add_instr code (Icall_prover (p.Whyconf.prover, t, m));
140 141 142 143 144 145 146 147 148 149 150 151 152
        scan code lexbuf }
  | transform space+ (ident as t) space+ (ident as l)
      { transform code t;
        add_instr code (Itransform (t, find_label code l));
        scan code lexbuf }
  | _ as c
      { let i = Lexing.lexeme_start lexbuf in
        error "syntax error on character '%c' at position %d" c i }
  | eof
      { () }

{

153
  let parse env conf s =
154 155 156 157 158 159 160 161 162 163 164 165 166
    let code = create_code env conf in
    scan code (Lexing.from_string s);
    let label = Array.make code.temp 0 in
    let fill name lab = match lab.defined with
      | None -> error "label '%s' is undefined" name
      | Some n -> label.(lab.temporary) <- n in
    Hashtbl.iter fill code.labels;
    let solve = function
      | Icall_prover _ as i -> i
      | Itransform (t, n) -> Itransform (t, label.(n))
      | Igoto n -> Igoto label.(n) in
    Array.map solve (Array.sub code.instr 0 code.next)

167
}