File: genParser.ml

package info (click to toggle)
herdtools7 7.58-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid
  • size: 19,732 kB
  • sloc: ml: 128,583; ansic: 3,827; makefile: 670; python: 407; sh: 212; awk: 14
file content (270 lines) | stat: -rw-r--r-- 8,971 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
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
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
(****************************************************************************)
(*                           the diy toolsuite                              *)
(*                                                                          *)
(* Jade Alglave, University College London, UK.                             *)
(* Luc Maranget, INRIA Paris-Rocquencourt, France.                          *)
(*                                                                          *)
(* Copyright 2010-present Institut National de Recherche en Informatique et *)
(* en Automatique and the authors. All rights reserved.                     *)
(*                                                                          *)
(* This software is governed by the CeCILL-B license under French law and   *)
(* abiding by the rules of distribution of free software. You can use,      *)
(* modify and/ or redistribute the software under the terms of the CeCILL-B *)
(* license as circulated by CEA, CNRS and INRIA at the following URL        *)
(* "http://www.cecill.info". We also give a copy in LICENSE.txt.            *)
(****************************************************************************)

(******************************)
(* A 'generic' parsing module *)
(******************************)

(* Configuration, to change kinds and condition *)
module type Config = sig
  val debuglexer : bool
  val verbose : int
  val check_kind : string -> ConstrGen.kind option
  val check_cond : string -> string option
end

module DefaultConfig = struct
  let debuglexer = false let verbose = 0
  let check_kind _ = None
  let check_cond _ = None
end

(* input signature, a lexer and a parser for a given architecture *)
module type LexParse = sig
  type token
  type instruction

  val lexer : Lexing.lexbuf -> token
  val parser :
        (Lexing.lexbuf -> token) -> Lexing.lexbuf ->
          MiscParser.proc list * instruction list list * MiscParser.extra_data
end

(* Output signature *)
module type S = sig
  type pseudo
  type init = MiscParser.state
  type prog = (MiscParser.proc * pseudo list) list
  type locations = MiscParser.LocSet.t

  val parse : in_channel -> Splitter.result ->  pseudo MiscParser.t
  val parse_string : string -> Splitter.result ->  pseudo MiscParser.t
end


module Make
    (O:Config)
    (A:ArchBase.S)
    (L: LexParse
    with type instruction = A.parsedPseudo) : S with type pseudo = A.pseudo =
  struct
    type pseudo = A.pseudo
    type init = MiscParser.state
    type prog = (MiscParser.proc * pseudo list) list
    type locations = MiscParser.LocSet.t

    let call_parser = GenParserUtils.call_parser
    module U = GenParserUtils

(*
  Transpose the instructions:
  a list of rows -> a list of columns (each being the program
  for a given processor
*)
    let transpose procs prog =
      try
        let prog = Misc.transpose prog in
        List.combine procs prog
      with
      |  Misc.TransposeFailure | Invalid_argument _ ->
          Warn.fatal "mismatch in instruction lines"


(************************)
(* Various basic checks *)
(************************)

    let check_procs procs =
      let rec iter_rec i xs = match xs with
        | [] -> ()
        | (p,_,MiscParser.Main)::xs ->
           if i = p then
             iter_rec (i + 1) xs
           else
             Warn.fatal "Processes must be P0, P1, ..."
        | (p,_,MiscParser.FaultHandler)::xs ->
           if i >= p then
             iter_rec i xs
           else
             Warn.fatal "Fault Handler for an undefined process"
      in iter_rec 0 procs

 let check_regs procs = U.check_regs (List.map (fun (p,_,_) -> p) procs)

(*******************)
(* Macro expansion *)
(*******************)

    let rec expn  = function
      | [] -> []
      | A.Macro (name,regs)::k ->
          let f =
            try A.get_macro name
            with Not_found -> Warn.fatal "macro not found: %s" name in
          f regs (expn k)
      | i::k -> i::expn k

    let expn_prog =
      Label.reset () ;
      List.map (fun (p,code) -> p,expn code)

(* Translation from parsed instruction to internal ones *)
    let check_and_tr p =
      let p = A.pseudo_parsed_tr p in
      if A.pseudo_exists (fun p -> not (A.is_valid p)) p then
        Warn.user_error "Illegal instruction '%s'"
          (A.pseudo_dump A.dump_instruction p)
      else p

    let parsed_tr prog =
      List.map
        (List.map check_and_tr)
        prog

(***********)
(* Parsing *)
(***********)

(* Lexers *)
    module LexConfig = struct let debug = O.debuglexer end
    module LU = LexUtils.Make (LexConfig)
    module SL = StateLexer.Make (LexConfig)


    let parse_cond lexbuf =
      let cond =  call_parser "cond" lexbuf
          SL.token StateParser.main_constr in
      cond

    module D = TestHash.Make(A)

    module Do
        (I:
           sig
             type src
             val call_parser_loc :
                 string ->
                   src -> Pos.pos2 ->
                     'a -> ('a -> Lexing.lexbuf -> 'b) -> 'b
           end) = struct

    let parse chan
        {
         Splitter.locs = (init_loc, prog_loc,constr_loc,_) ;
         name = name ;
         info = info ; _
       }  =
      let init =
        I.call_parser_loc "init"
          chan init_loc SL.token StateParser.init in
      MiscParser.check_env_for_dups init ;
      let procs,prog,extra_data =
        I.call_parser_loc "prog" chan prog_loc L.lexer L.parser in
      check_procs procs ;
      let prog = parsed_tr prog in
      let prog = transpose procs prog in
      let prog = expn_prog prog in
      let (locs,filter,final,_quantifiers) =
        I.call_parser_loc "final"
          chan constr_loc SL.token StateParser.constraints in
      check_regs procs init locs final ;
      let all_locs = U.get_visible_locs locs final in
      let parsed =
        {
         MiscParser.info; init; prog = prog;
         filter = filter;
         condition = final;
         locations = locs;
         extra_data = extra_data ;
       } in
      let name  = name.Name.name in
      let parsed =
        match O.check_cond name  with
        | None -> parsed
        | Some k ->
            let cond =
              let cond = parse_cond (Lexing.from_string k) in
              try (* Apply mapping as condition may be expressed with external
                     registers *)
                let map = List.assoc OutMapping.key info in
                let map = try LexOutMapping.parse map with _ -> assert false in
                let map = OutMapping.locmap_inverse map in
                if O.verbose > 0 then
                  MiscParser.LocMap.iter
                    (fun k v ->
                      Printf.eprintf "Loc %s -> %s\n"
                        (MiscParser.dump_location k)
                        (MiscParser.dump_location v))
                    map ;
                let map_loc loc = MiscParser.LocMap.safe_find loc loc map in
                let open ConstrGen in
                let map_rloc rloc = match rloc with
                  | Loc loc -> Loc (map_loc loc)
                  | Deref (loc,i) -> Deref (map_loc loc,i) in
                let open MiscParser in
                let map_atom = function
                  | LV (loc,v) -> LV (map_rloc loc,v)
                  | LL (loc1,loc2) ->  LL (map_loc loc1,map_loc loc2)
                  | FF (_,None,_) as a -> a
                  | FF (p,Some x,ft) ->
                      begin match map_loc (Location_global x) with
                      | Location_global x -> FF (p,Some x,ft)
                      | _ -> assert false
                      end
                in
                if O.verbose > 0 then prerr_endline "Bingo" ;
                ConstrGen.map_constr map_atom cond
              with Not_found -> cond in
            { parsed with
              MiscParser.condition = cond ;} in
      let parsed =
        match O.check_kind name  with
        | None -> parsed
        | Some k ->
            { parsed with
              MiscParser.condition =
              ConstrGen.set_kind k parsed.MiscParser.condition; } in
      let parsed =
        match MiscParser.get_hash parsed with
        | None ->
             let info = parsed.MiscParser.info in
             { parsed with
               MiscParser.info =
               ("Hash",D.digest info init prog all_locs)::info ; }
        | Some _ -> parsed in
      parsed
    end

    let parse chan x =
      let module Src = struct
        type src = in_channel
        let call_parser_loc name chan loc =
          let lexbuf = LU.from_section loc chan in
          call_parser name lexbuf
      end in
      let module P = Do(Src) in
      P.parse chan x

    let parse_string s x =
      let module Src = struct
        type src = string
        let call_parser_loc name s loc =
          let lexbuf = LU.from_section_string loc s in
          call_parser name lexbuf
      end in
      let module P = Do(Src) in
      P.parse s x
  end