← Back to branch summary

~ubuntu-branches/debian/sid/frama-c/sid

« back to all changes in this revision

Viewing changes to cil/src/frontc/patch.ml

  • Committer: Bazaar Package Importer
  • Author(s): Mehdi Dogguy
  • Date: 2009-06-03 08:19:25 UTC
  • Revision ID: james.westby@ubuntu.com-20090603081925-kihvxvt0wy3zc4ar
Tags: upstream-20081201.dfsg
Import upstream version 20081201.dfsg

Show diffs side-by-side

added added

removed removed

Lines of Context:
cil/src/frontc/patch.ml
 
1
(**************************************************************************)
 
2
(*                                                                        *)
 
3
(*  Copyright (C) 2001-2003,                                              *)
 
4
(*   George C. Necula    <necula@cs.berkeley.edu>                         *)
 
5
(*   Scott McPeak        <smcpeak@cs.berkeley.edu>                        *)
 
6
(*   Wes Weimer          <weimer@cs.berkeley.edu>                         *)
 
7
(*   Ben Liblit          <liblit@cs.berkeley.edu>                         *)
 
8
(*  All rights reserved.                                                  *)
 
9
(*                                                                        *)
 
10
(*  Redistribution and use in source and binary forms, with or without    *)
 
11
(*  modification, are permitted provided that the following conditions    *)
 
12
(*  are met:                                                              *)
 
13
(*                                                                        *)
 
14
(*  1. Redistributions of source code must retain the above copyright     *)
 
15
(*  notice, this list of conditions and the following disclaimer.         *)
 
16
(*                                                                        *)
 
17
(*  2. Redistributions in binary form must reproduce the above copyright  *)
 
18
(*  notice, this list of conditions and the following disclaimer in the   *)
 
19
(*  documentation and/or other materials provided with the distribution.  *)
 
20
(*                                                                        *)
 
21
(*  3. The names of the contributors may not be used to endorse or        *)
 
22
(*  promote products derived from this software without specific prior    *)
 
23
(*  written permission.                                                   *)
 
24
(*                                                                        *)
 
25
(*  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS   *)
 
26
(*  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT     *)
 
27
(*  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS     *)
 
28
(*  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE        *)
 
29
(*  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,   *)
 
30
(*  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,  *)
 
31
(*  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;      *)
 
32
(*  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER      *)
 
33
(*  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT    *)
 
34
(*  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN     *)
 
35
(*  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE       *)
 
36
(*  POSSIBILITY OF SUCH DAMAGE.                                           *)
 
37
(*                                                                        *)
 
38
(*  File modified by CEA (Commissariat � l'�nergie Atomique).             *)
 
39
(**************************************************************************)
 
40
 
 
41
 
 
42
(* patch.ml *)
 
43
(* CABS file patching *)
 
44
 
 
45
open Cabs
 
46
open Cabshelper
 
47
open Trace
 
48
open Pretty
 
49
open Cabsvisit
 
50
open Cil
 
51
 
 
52
(* binding of a unification variable to a syntactic construct *)
 
53
type binding =
 
54
  | BSpecifier of string * spec_elem list
 
55
  | BName of string * string
 
56
  | BExpr of string * expression
 
57
 
 
58
(* thrown when unification fails *)
 
59
exception NoMatch
 
60
 
 
61
(* thrown when an attempt to find the associated binding fails *)
 
62
exception BadBind of string
 
63
 
 
64
(* trying to isolate performance problems; will hide all the *)
 
65
(* potentially expensive debugging output behind "if verbose .." *)
 
66
let verbose : bool = true
 
67
 
 
68
 
 
69
(* raise NoMatch if x and y are not equal *)
 
70
let mustEq (x : 'a) (y : 'a) : unit =
 
71
begin
 
72
  if (x <> y) then (
 
73
    if verbose then
 
74
      (trace "patchDebug" (dprintf "mismatch by structural disequality\n"));
 
75
    raise NoMatch
 
76
  )
 
77
end
 
78
 
 
79
(* why isn't this in the core Ocaml library? *)
 
80
let identity x = x
 
81
 
 
82
 
 
83
let isPatternVar (s : string) : bool =
 
84
begin
 
85
  ((String.length s) >= 1) && ((String.get s 0) = '@')
 
86
end
 
87
 
 
88
(* 's' is actually "@name(blah)"; extract the 'blah' *)
 
89
let extractPatternVar (s : string) : string =
 
90
  (*(trace "patch" (dprintf "extractPatternVar %s\n" s));*)
 
91
  (String.sub s 6 ((String.length s) - 7))
 
92
 
 
93
 
 
94
(* a few debugging printers.. *)
 
95
let printExpr (e : expression) =
 
96
begin
 
97
  if (verbose && traceActive "patchDebug") then (
 
98
    Cprint.print_expression e; Cprint.force_new_line ();
 
99
    Cprint.flush ()
 
100
  )
 
101
end
 
102
 
 
103
let printSpec (spec: spec_elem list) =
 
104
begin
 
105
  if (verbose && traceActive "patchDebug") then (
 
106
    Cprint.print_specifiers spec;  Cprint.force_new_line ();
 
107
    Cprint.flush ()
 
108
  )
 
109
end
 
110
 
 
111
let printSpecs (pat : spec_elem list) (tgt : spec_elem list) =
 
112
begin
 
113
  (printSpec pat);
 
114
  (printSpec tgt)
 
115
end
 
116
 
 
117
let printDecl (pat : name) (tgt : name) =
 
118
begin
 
119
  if (verbose && traceActive "patchDebug") then (
 
120
    Cprint.print_name pat;  Cprint.force_new_line ();
 
121
    Cprint.print_name tgt;  Cprint.force_new_line ();
 
122
    Cprint.flush ()
 
123
  )
 
124
end
 
125
 
 
126
let printDeclType (pat : decl_type) (tgt : decl_type) =
 
127
begin
 
128
  if (verbose && traceActive "patchDebug") then (
 
129
    Cprint.print_decl "__missing_field_name" pat;  Cprint.force_new_line ();
 
130
    Cprint.print_decl "__missing_field_name" tgt;  Cprint.force_new_line ();
 
131
    Cprint.flush ()
 
132
  )
 
133
end
 
134
 
 
135
let printDefn (d : definition) =
 
136
begin
 
137
  if (verbose && traceActive "patchDebug") then (
 
138
    Cprint.print_def d;
 
139
    Cprint.flush ()
 
140
  )
 
141
end
 
142
 
 
143
 
 
144
(* class to describe how to modify the tree for subtitution *)
 
145
class substitutor (bindings : binding list) = object(self)
 
146
  inherit nopCabsVisitor as super
 
147
 
 
148
  (* look in the binding list for a given name *)
 
149
  method findBinding (name : string) : binding =
 
150
  begin
 
151
    try
 
152
      (List.find
 
153
        (fun b ->
 
154
          match b with
 
155
          | BSpecifier(n, _) -> n=name
 
156
          | BName(n, _) -> n=name
 
157
          | BExpr(n, _) -> n=name)
 
158
        bindings)
 
159
    with
 
160
      Not_found -> raise (BadBind ("name not found: " ^ name))
 
161
  end
 
162
 
 
163
  method vexpr (e:expression) : expression visitAction =
 
164
  begin
 
165
    match e with
 
166
    | EXPR_PATTERN(name) -> (
 
167
        match (self#findBinding name) with
 
168
        | BExpr(_, expr) -> ChangeTo(expr)    (* substitute bound expression *)
 
169
        | _ -> raise (BadBind ("wrong type: " ^ name))
 
170
      )
 
171
    | _ -> DoChildren
 
172
  end
 
173
 
 
174
  (* use of a name *)
 
175
  method vvar (s:string) : string =
 
176
  begin
 
177
    if (isPatternVar s) then (
 
178
      let nameString = (extractPatternVar s) in
 
179
      match (self#findBinding nameString) with
 
180
      | BName(_, str) -> str        (* substitute *)
 
181
      | _ -> raise (BadBind ("wrong type: " ^ nameString))
 
182
    )
 
183
    else
 
184
      s
 
185
  end
 
186
 
 
187
  (* binding introduction of a name *)
 
188
  method vname (_k: nameKind) (_spec: specifier) (n: name) : name visitAction =
 
189
  begin
 
190
    match n with (s (*variable name*), dtype, attrs, loc) -> (
 
191
      let replacement = (self#vvar s) in    (* use replacer from above *)
 
192
      if (s <> replacement) then
 
193
        ChangeTo(replacement, dtype, attrs, loc)
 
194
      else
 
195
        DoChildren                          (* no replacement *)
 
196
    )
 
197
  end
 
198
 
 
199
  method vspec (specList: specifier) : specifier visitAction =
 
200
  begin
 
201
    if verbose then (trace "patchDebug" (dprintf "substitutor: vspec\n"));
 
202
    (printSpec specList);
 
203
 
 
204
    (* are any of the specifiers SpecPatterns?  we have to check the entire *)
 
205
    (* list, not just the head, because e.g. "typedef @specifier(foo)" has *)
 
206
    (* "typedef" as the head of the specifier list *)
 
207
    if (List.exists (fun elt -> match elt with
 
208
                                | SpecPattern(_) -> true
 
209
                                | _ -> false)
 
210
                    specList) then begin
 
211
      (* yes, replace the existing list with one got by *)
 
212
      (* replacing all occurrences of SpecPatterns *)
 
213
      (trace "patchDebug" (dprintf "at least one spec pattern\n"));
 
214
      ChangeTo
 
215
        (List.flatten
 
216
          (List.map
 
217
            (* for each specifier element, yield the specifier list *)
 
218
            (* to which it maps; then we'll flatten the final result *)
 
219
            (fun elt ->
 
220
              match elt with
 
221
              | SpecPattern(name) -> (
 
222
                  match (self#findBinding name) with
 
223
                  | BSpecifier(_, replacement) -> (
 
224
                      (trace "patchDebug" (dprintf "replacing pattern %s\n" name));
 
225
                      replacement
 
226
                    )
 
227
                  | _ -> raise (BadBind ("wrong type: " ^ name))
 
228
                )
 
229
              | _ -> [elt]    (* leave this one alone *)
 
230
            )
 
231
            specList
 
232
          )
 
233
        )
 
234
    end
 
235
    else
 
236
      (* none of the specifiers in specList are patterns *)
 
237
      DoChildren
 
238
  end
 
239
 
 
240
  method vtypespec (tspec: typeSpecifier) : typeSpecifier visitAction =
 
241
  begin
 
242
    match tspec with
 
243
    | Tnamed(str) when (isPatternVar str) ->
 
244
        ChangeTo(Tnamed(self#vvar str))
 
245
    | Tstruct(str, fields, extraAttrs) when (isPatternVar str) -> (
 
246
        (trace "patchDebug" (dprintf "substituting %s\n" str));
 
247
        ChangeDoChildrenPost(Tstruct((self#vvar str), fields, extraAttrs), identity)
 
248
      )
 
249
    | Tunion(str, fields, extraAttrs) when (isPatternVar str) ->
 
250
        (trace "patchDebug" (dprintf "substituting %s\n" str));
 
251
        ChangeDoChildrenPost(Tunion((self#vvar str), fields, extraAttrs), identity)
 
252
    | _ -> DoChildren
 
253
  end
 
254
 
 
255
end
 
256
 
 
257
 
 
258
(* why can't I have forward declarations in the language?!! *)
 
259
let unifyExprFwd : (expression -> expression -> binding list) ref
 
260
  = ref (fun _e _e -> [])
 
261
 
 
262
 
 
263
(* substitution for expressions *)
 
264
let substExpr (bindings : binding list) (expr : expression) : expression =
 
265
begin
 
266
  if verbose then
 
267
    (trace "patchDebug" (dprintf "substExpr with %d bindings\n" (List.length bindings)));
 
268
  (printExpr expr);
 
269
 
 
270
  (* apply the transformation *)
 
271
  let result = (visitCabsExpression (new substitutor bindings :> cabsVisitor) expr) in
 
272
  (printExpr result);
 
273
 
 
274
  result
 
275
end
 
276
 
 
277
let d_loc (_:unit) (loc: cabsloc) : doc =
 
278
  text (fst loc).Lexing.pos_fname ++ chr ':' ++ num (fst loc).Lexing.pos_lnum
 
279
 
 
280
 
 
281
(* class to describe how to modify the tree when looking for places *)
 
282
(* to apply expression transformers *)
 
283
class exprTransformer (srcpattern : expression) (destpattern : expression)
 
284
                      (patchline : int) (srcloc : cabsloc) = object
 
285
  inherit nopCabsVisitor as super
 
286
 
 
287
  method vexpr (e:expression) : expression visitAction =
 
288
  begin
 
289
    (* see if the source pattern matches this subexpression *)
 
290
    try (
 
291
      let bindings = (!unifyExprFwd srcpattern e) in
 
292
 
 
293
      (* match! *)
 
294
      (trace "patch" (dprintf "expr match: patch line %d, src %a\n"
 
295
                              patchline d_loc srcloc));
 
296
      ChangeTo(substExpr bindings destpattern)
 
297
    )
 
298
 
 
299
    with NoMatch -> (
 
300
      (* doesn't apply *)
 
301
      DoChildren
 
302
    )
 
303
  end
 
304
 
 
305
  (* other constructs left unchanged *)
 
306
end
 
307
 
 
308
 
 
309
let unifyList (pat : 'a list) (tgt : 'a list)
 
310
              (unifyElement : 'a -> 'a -> binding list) : binding list =
 
311
begin
 
312
  if verbose then
 
313
    (trace "patchDebug" (dprintf "unifyList (pat len %d, tgt len %d)\n"
 
314
                                 (List.length pat) (List.length tgt)));
 
315
 
 
316
  (* walk down the lists *)
 
317
  let rec loop pat tgt : binding list =
 
318
    match pat, tgt with
 
319
    | [], [] -> []
 
320
    | (pelt :: prest), (telt :: trest) ->
 
321
         (unifyElement pelt telt) @
 
322
         (loop prest trest)
 
323
    | _,_ -> (
 
324
        (* no match *)
 
325
        if verbose then (
 
326
          (trace "patchDebug" (dprintf "mismatching list length\n"));
 
327
        );
 
328
        raise NoMatch
 
329
     )
 
330
  in
 
331
  (loop pat tgt)
 
332
end
 
333
 
 
334
 
 
335
let gettime () : float =
 
336
  (Unix.times ()).Unix.tms_utime
 
337
 
 
338
let rec applyPatch (patchFile : file) (srcFile : file) : file =
 
339
begin
 
340
  let patch : definition list = List.map snd (snd patchFile) in
 
341
  let srcFname : string = (fst srcFile) in
 
342
  let src : definition list = List.map snd (snd srcFile) in
 
343
 
 
344
  (trace "patchTime" (dprintf "applyPatch start: %f\n" (gettime ())));
 
345
  if (traceActive "patchDebug") then
 
346
    Cprint.out := stdout      (* hack *)
 
347
  else ();
 
348
 
 
349
  (* more hackery *)
 
350
  unifyExprFwd := unifyExpr;
 
351
 
 
352
  (* patch a single source definition, yield transformed *)
 
353
  let rec patchDefn (patch : definition list) (d : definition) : definition list =
 
354
  begin
 
355
    match patch with
 
356
    | TRANSFORMER(srcpattern, destpattern, loc) :: rest -> (
 
357
        if verbose then
 
358
          (trace "patchDebug"
 
359
            (dprintf "considering applying defn pattern at line %d to src at %a\n"
 
360
                     (fst loc).Lexing.pos_lnum d_loc (get_definitionloc d)));
 
361
 
 
362
        (* see if the source pattern matches the definition 'd' we have *)
 
363
        try (
 
364
          let bindings = (unifyDefn srcpattern d) in
 
365
 
 
366
          (* we have a match!  apply the substitutions *)
 
367
          (trace "patch" (dprintf "defn match: patch line %d, src %a\n"
 
368
                                  (fst loc).Lexing.pos_lnum d_loc (get_definitionloc d)));
 
369
 
 
370
          (List.map (fun destElt -> (substDefn bindings destElt)) destpattern)
 
371
        )
 
372
 
 
373
        with NoMatch -> (
 
374
          (* no match, continue down list *)
 
375
          (*(trace "patch" (dprintf "no match\n"));*)
 
376
          (patchDefn rest d)
 
377
        )
 
378
      )
 
379
 
 
380
    | EXPRTRANSFORMER(srcpattern, destpattern, loc) :: rest -> (
 
381
        if verbose then
 
382
          (trace "patchDebug"
 
383
            (dprintf "considering applying expr pattern at line %d to src at %a\n"
 
384
                     (fst loc).Lexing.pos_lnum d_loc (get_definitionloc d)));
 
385
 
 
386
        (* walk around in 'd' looking for expressions to modify *)
 
387
        let dList = (visitCabsDefinition
 
388
                      ((new exprTransformer srcpattern destpattern
 
389
                                            (fst loc).Lexing.pos_lnum (get_definitionloc d))
 
390
                       :> cabsVisitor)
 
391
                      d
 
392
                    ) in
 
393
 
 
394
        (* recursively invoke myself to try additional patches *)
 
395
        (* since visitCabsDefinition might return a list, I'll try my *)
 
396
        (* addtional patches on every yielded definition, then collapse *)
 
397
        (* all of them into a single list *)
 
398
        (List.flatten (List.map (fun d -> (patchDefn rest d)) dList))
 
399
      )
 
400
 
 
401
    | _ :: rest -> (
 
402
        (* not a transformer; just keep going *)
 
403
        (patchDefn rest d)
 
404
      )
 
405
    | [] -> (
 
406
        (* reached the end of the patch file with no match *)
 
407
        [d]     (* have to wrap it in a list ... *)
 
408
      )
 
409
  end in
 
410
 
 
411
  (* transform all the definitions *)
 
412
  let result : definition list =
 
413
    (List.flatten (List.map (fun d -> (patchDefn patch d)) src)) in
 
414
 
 
415
  (*Cprint.print_defs result;*)
 
416
 
 
417
  if (traceActive "patchDebug") then (
 
418
    (* avoid flush bug? yes *)
 
419
    Cprint.force_new_line ();
 
420
    Cprint.flush ()
 
421
  );
 
422
 
 
423
  (trace "patchTime" (dprintf "applyPatch finish: %f\n" (gettime ())));
 
424
  (srcFname, List.map (fun x -> false,x) result)
 
425
end
 
426
 
 
427
 
 
428
(* given a definition pattern 'pat', and a target concrete defintion 'tgt', *)
 
429
(* determine if they can be unified; if so, return the list of bindings of *)
 
430
(* unification variables in pat; otherwise raise NoMatch *)
 
431
and unifyDefn (pat : definition) (tgt : definition) : binding list =
 
432
begin
 
433
  match pat, tgt with
 
434
  | DECDEF(_,(pspecifiers, pdeclarators), _),
 
435
    DECDEF(_,(tspecifiers, tdeclarators), _) -> (
 
436
      if verbose then
 
437
        (trace "patchDebug" (dprintf "unifyDefn of DECDEFs\n"));
 
438
      (unifySpecifiers pspecifiers tspecifiers) @
 
439
      (unifyInitDeclarators pdeclarators tdeclarators)
 
440
    )
 
441
 
 
442
  | TYPEDEF((pspec, pdecl), _),
 
443
    TYPEDEF((tspec, tdecl), _) -> (
 
444
      if verbose then
 
445
        (trace "patchDebug" (dprintf "unifyDefn of TYPEDEFs\n"));
 
446
      (unifySpecifiers pspec tspec) @
 
447
      (unifyDeclarators pdecl tdecl)
 
448
    )
 
449
 
 
450
  | ONLYTYPEDEF(pspec, _),
 
451
    ONLYTYPEDEF(tspec, _) -> (
 
452
      if verbose then
 
453
        (trace "patchDebug" (dprintf "unifyDefn of ONLYTYPEDEFs\n"));
 
454
      (unifySpecifiers pspec tspec)
 
455
    )
 
456
 
 
457
  | _, _ -> (
 
458
      if verbose then
 
459
        (trace "patchDebug" (dprintf "mismatching definitions\n"));
 
460
      raise NoMatch
 
461
    )
 
462
end
 
463
 
 
464
and unifySpecifier (pat : spec_elem) (tgt : spec_elem) : binding list =
 
465
begin
 
466
  if verbose then
 
467
    (trace "patchDebug" (dprintf "unifySpecifier\n"));
 
468
  (printSpecs [pat] [tgt]);
 
469
 
 
470
  if (pat = tgt) then [] else
 
471
 
 
472
  match pat, tgt with
 
473
  | SpecType(tspec1), SpecType(tspec2) ->
 
474
      (unifyTypeSpecifier tspec1 tspec2)
 
475
  | SpecPattern(name), _ ->
 
476
      (* record that future occurrances of @specifier(name) will yield this specifier *)
 
477
      if verbose then
 
478
        (trace "patchDebug" (dprintf "found specifier match for %s\n" name));
 
479
      [BSpecifier(name, [tgt])]
 
480
  | _,_ -> (
 
481
      (* no match *)
 
482
      if verbose then (
 
483
        (trace "patchDebug" (dprintf "mismatching specifiers\n"));
 
484
      );
 
485
      raise NoMatch
 
486
   )
 
487
end
 
488
 
 
489
and unifySpecifiers (pat : spec_elem list) (tgt : spec_elem list) : binding list =
 
490
begin
 
491
  if verbose then
 
492
    (trace "patchDebug" (dprintf "unifySpecifiers\n"));
 
493
  (printSpecs pat tgt);
 
494
 
 
495
  (* canonicalize the specifiers by sorting them *)
 
496
  let pat' = (List.stable_sort compare pat) in
 
497
  let tgt' = (List.stable_sort compare tgt) in
 
498
 
 
499
  (* if they are equal, they match with no further checking *)
 
500
  if (pat' = tgt') then [] else
 
501
 
 
502
  (* walk down the lists; don't walk the sorted lists because the *)
 
503
  (* pattern must always be last, if it occurs *)
 
504
  let rec loop pat tgt : binding list =
 
505
    match pat, tgt with
 
506
    | [], [] -> []
 
507
    | [SpecPattern(name)], _ ->
 
508
        (* final SpecPattern matches anything which comes after *)
 
509
        (* record that future occurrences of @specifier(name) will yield this specifier *)
 
510
        if verbose then
 
511
          (trace "patchDebug" (dprintf "found specifier match for %s\n" name));
 
512
        [BSpecifier(name, tgt)]
 
513
    | (pspec :: prest), (tspec :: trest) ->
 
514
         (unifySpecifier pspec tspec) @
 
515
         (loop prest trest)
 
516
    | _,_ -> (
 
517
        (* no match *)
 
518
        if verbose then (
 
519
          (trace "patchDebug" (dprintf "mismatching specifier list length\n"));
 
520
        );
 
521
        raise NoMatch
 
522
     )
 
523
  in
 
524
  (loop pat tgt)
 
525
end
 
526
 
 
527
and unifyTypeSpecifier (pat: typeSpecifier) (tgt: typeSpecifier) : binding list =
 
528
begin
 
529
  if verbose then
 
530
    (trace "patchDebug" (dprintf "unifyTypeSpecifier\n"));
 
531
 
 
532
  if (pat = tgt) then [] else
 
533
 
 
534
  match pat, tgt with
 
535
  | Tnamed(s1), Tnamed(s2) -> (unifyString s1 s2)
 
536
  | Tstruct(name1, None, _), Tstruct(name2, None, _) ->
 
537
      (unifyString name1 name2)
 
538
  | Tstruct(name1, Some(fields1), _), Tstruct(name2, Some(fields2), _) ->
 
539
      (* ignoring extraAttrs b/c we're just trying to come up with a list
 
540
       * of substitutions, and there's no unify_attributes function, and
 
541
       * I don't care at this time about checking that they are equal .. *)
 
542
      (unifyString name1 name2) @
 
543
      (unifyList fields1 fields2 unifyField)
 
544
  | Tunion(name1, None, _), Tstruct(name2, None, _) ->
 
545
      (unifyString name1 name2)
 
546
  | Tunion(name1, Some(fields1), _), Tunion(name2, Some(fields2), _) ->
 
547
      (unifyString name1 name2) @
 
548
      (unifyList fields1 fields2 unifyField)
 
549
  | Tenum(name1, None, _), Tenum(name2, None, _) ->
 
550
      (unifyString name1 name2)
 
551
  | Tenum(name1, Some(items1), _), Tenum(name2, Some(items2), _) ->
 
552
      (mustEq items1 items2);    (* enum items *)
 
553
      (unifyString name1 name2)
 
554
  | TtypeofE(exp1), TtypeofE(exp2) ->
 
555
      (unifyExpr exp1 exp2)
 
556
  | TtypeofT(spec1, dtype1), TtypeofT(spec2, dtype2) ->
 
557
      (unifySpecifiers spec1 spec2) @
 
558
      (unifyDeclType dtype1 dtype2)
 
559
  | _ -> (
 
560
      if verbose then (trace "patchDebug" (dprintf "mismatching typeSpecifiers\n"));
 
561
      raise NoMatch
 
562
    )
 
563
end
 
564
 
 
565
and unifyField (pat : field_group) (tgt : field_group) : binding list =
 
566
begin
 
567
  match pat,tgt with FIELD (spec1, list1), FIELD (spec2, list2) -> (
 
568
    (unifySpecifiers spec1 spec2) @
 
569
      (unifyList list1 list2 unifyNameExprOpt)
 
570
  )
 
571
    | _ ->
 
572
        (* no match *)
 
573
        if verbose then (
 
574
          (trace "patchDebug" (dprintf "mismatching during type annotation\n"));
 
575
        );
 
576
        raise NoMatch
 
577
end
 
578
 
 
579
and unifyNameExprOpt (pat : name * expression option)
 
580
                     (tgt : name * expression option) : binding list =
 
581
begin
 
582
  match pat,tgt with
 
583
  | (name1, None), (name2, None) -> (unifyName name1 name2)
 
584
  | (name1, Some(exp1)), (name2, Some(exp2)) ->
 
585
      (unifyName name1 name2) @
 
586
      (unifyExpr exp1 exp2)
 
587
  | _,_ -> []
 
588
end
 
589
 
 
590
and unifyName (pat : name) (tgt : name) : binding list =
 
591
begin
 
592
  match pat,tgt with (pstr, pdtype, pattrs, _ploc), (tstr, tdtype, tattrs, _tloc) ->
 
593
    (mustEq pattrs tattrs);
 
594
    (unifyString pstr tstr) @
 
595
    (unifyDeclType pdtype tdtype)
 
596
end
 
597
 
 
598
and unifyInitDeclarators (pat : init_name list) (tgt : init_name list) : binding list =
 
599
begin
 
600
  (*
 
601
    if verbose then
 
602
      (trace "patchDebug" (dprintf "unifyInitDeclarators, pat %d, tgt %d\n"
 
603
                                   (List.length pat) (List.length tgt)));
 
604
  *)
 
605
 
 
606
  match pat, tgt with
 
607
  | ((pdecl, piexpr) :: prest),
 
608
    ((tdecl, tiexpr) :: trest) ->
 
609
      (unifyDeclarator pdecl tdecl) @
 
610
      (unifyInitExpr piexpr tiexpr) @
 
611
      (unifyInitDeclarators prest trest)
 
612
  | [], [] -> []
 
613
  | _, _ -> (
 
614
      if verbose then
 
615
        (trace "patchDebug" (dprintf "mismatching init declarators\n"));
 
616
      raise NoMatch
 
617
    )
 
618
end
 
619
 
 
620
and unifyDeclarators (pat : name list) (tgt : name list) : binding list =
 
621
  (unifyList pat tgt unifyDeclarator)
 
622
 
 
623
and unifyDeclarator (pat : name) (tgt : name) : binding list =
 
624
begin
 
625
  if verbose then
 
626
    (trace "patchDebug" (dprintf "unifyDeclarator\n"));
 
627
  (printDecl pat tgt);
 
628
 
 
629
  match pat, tgt with
 
630
  | (pname, pdtype, pattr, _ploc),
 
631
    (tname, tdtype, tattr, _tloc) ->
 
632
      (mustEq pattr tattr);
 
633
      (unifyDeclType pdtype tdtype) @
 
634
      (unifyString pname tname)
 
635
end
 
636
 
 
637
and unifyDeclType (pat : decl_type) (tgt : decl_type) : binding list =
 
638
begin
 
639
  if verbose then
 
640
    (trace "patchDebug" (dprintf "unifyDeclType\n"));
 
641
  (printDeclType pat tgt);
 
642
 
 
643
  match pat, tgt with
 
644
  | JUSTBASE, JUSTBASE -> []
 
645
  | PARENTYPE(pattr1, ptype, pattr2),
 
646
    PARENTYPE(tattr1, ttype, tattr2) ->
 
647
      (mustEq pattr1 tattr1);
 
648
      (mustEq pattr2 tattr2);
 
649
      (unifyDeclType ptype ttype)
 
650
  | ARRAY(ptype, pattr, psz),
 
651
    ARRAY(ttype, tattr, tsz) ->
 
652
      (mustEq pattr tattr);
 
653
      (unifyDeclType ptype ttype) @
 
654
      (unifyExpr psz tsz)
 
655
  | PTR(pattr, ptype),
 
656
    PTR(tattr, ttype) ->
 
657
      (mustEq pattr tattr);
 
658
      (unifyDeclType ptype ttype)
 
659
  | PROTO(ptype, pformals, pva),
 
660
    PROTO(ttype, tformals, tva) ->
 
661
      (mustEq pva tva);
 
662
      (unifyDeclType ptype ttype) @
 
663
      (unifySingleNames pformals tformals)
 
664
  | _ -> (
 
665
      if verbose then
 
666
        (trace "patchDebug" (dprintf "mismatching decl_types\n"));
 
667
      raise NoMatch
 
668
    )
 
669
end
 
670
 
 
671
and unifySingleNames (pat : single_name list) (tgt : single_name list) : binding list =
 
672
begin
 
673
  if verbose then
 
674
    (trace "patchDebug" (dprintf "unifySingleNames, pat %d, tgt %d\n"
 
675
                                 (List.length pat) (List.length tgt)));
 
676
 
 
677
  match pat, tgt with
 
678
  | [], [] -> []
 
679
  | (pspec, pdecl) :: prest,
 
680
    (tspec, tdecl) :: trest ->
 
681
      (unifySpecifiers pspec tspec) @
 
682
      (unifyDeclarator pdecl tdecl) @
 
683
      (unifySingleNames prest trest)
 
684
  | _, _ -> (
 
685
      if verbose then
 
686
        (trace "patchDebug" (dprintf "mismatching single_name lists\n"));
 
687
      raise NoMatch
 
688
    )
 
689
end
 
690
 
 
691
and unifyString (pat : string) (tgt : string) : binding list =
 
692
begin
 
693
  (* equal? match with no further ado *)
 
694
  if (pat = tgt) then [] else
 
695
 
 
696
  (* is the pattern a variable? *)
 
697
  if (isPatternVar pat) then
 
698
    (* pat is actually "@name(blah)"; extract the 'blah' *)
 
699
    let varname = (extractPatternVar pat) in
 
700
 
 
701
    (* when substituted, this name becomes 'tgt' *)
 
702
    if verbose then
 
703
      (trace "patchDebug" (dprintf "found name match for %s\n" varname));
 
704
    [BName(varname, tgt)]
 
705
 
 
706
  else (
 
707
    if verbose then
 
708
      (trace "patchDebug" (dprintf "mismatching names: %s and %s\n" pat tgt));
 
709
    raise NoMatch
 
710
  )
 
711
end
 
712
 
 
713
and unifyExpr (pat : expression) (tgt : expression) : binding list =
 
714
begin
 
715
  (* if they're equal, that's good enough *)
 
716
  if (pat = tgt) then [] else
 
717
 
 
718
  (* shorter name *)
 
719
  let ue = unifyExpr in
 
720
 
 
721
  (* because of the equality check above, I can omit some cases *)
 
722
  match pat, tgt with
 
723
  | UNARY(pop, pexpr),
 
724
    UNARY(top, texpr) ->
 
725
      (mustEq pop top);
 
726
      (ue pexpr texpr)
 
727
  | BINARY(pop, pexp1, pexp2),
 
728
    BINARY(top, texp1, texp2) ->
 
729
      (mustEq pop top);
 
730
      (ue pexp1 texp1) @
 
731
      (ue pexp2 texp2)
 
732
  | QUESTION(p1, p2, p3),
 
733
    QUESTION(t1, t2, t3) ->
 
734
      (ue p1 t1) @
 
735
      (ue p2 t2) @
 
736
      (ue p3 t3)
 
737
  | CAST((pspec, ptype), piexpr),
 
738
    CAST((tspec, ttype), tiexpr) ->
 
739
      (mustEq ptype ttype);
 
740
      (unifySpecifiers pspec tspec) @
 
741
      (unifyInitExpr piexpr tiexpr)
 
742
  | CALL(pfunc, pargs),
 
743
    CALL(tfunc, targs) ->
 
744
      (ue pfunc tfunc) @
 
745
      (unifyExprs pargs targs)
 
746
  | COMMA(pexprs),
 
747
    COMMA(texprs) ->
 
748
      (unifyExprs pexprs texprs)
 
749
  | EXPR_SIZEOF(pexpr),
 
750
    EXPR_SIZEOF(texpr) ->
 
751
      (ue pexpr texpr)
 
752
  | TYPE_SIZEOF(pspec, ptype),
 
753
    TYPE_SIZEOF(tspec, ttype) ->
 
754
      (mustEq ptype ttype);
 
755
      (unifySpecifiers pspec tspec)
 
756
  | EXPR_ALIGNOF(pexpr),
 
757
    EXPR_ALIGNOF(texpr) ->
 
758
      (ue pexpr texpr)
 
759
  | TYPE_ALIGNOF(pspec, ptype),
 
760
    TYPE_ALIGNOF(tspec, ttype) ->
 
761
      (mustEq ptype ttype);
 
762
      (unifySpecifiers pspec tspec)
 
763
  | INDEX(parr, pindex),
 
764
    INDEX(tarr, tindex) ->
 
765
      (ue parr tarr) @
 
766
      (ue pindex tindex)
 
767
  | MEMBEROF(pexpr, pfield),
 
768
    MEMBEROF(texpr, tfield) ->
 
769
      (mustEq pfield tfield);
 
770
      (ue pexpr texpr)
 
771
  | MEMBEROFPTR(pexpr, pfield),
 
772
    MEMBEROFPTR(texpr, tfield) ->
 
773
      (mustEq pfield tfield);
 
774
      (ue pexpr texpr)
 
775
  | GNU_BODY(pblock),
 
776
    GNU_BODY(tblock) ->
 
777
      (mustEq pblock tblock);
 
778
      []
 
779
  | EXPR_PATTERN(name), _ ->
 
780
      (* match, and contribute binding *)
 
781
      if verbose then
 
782
        (trace "patchDebug" (dprintf "found expr match for %s\n" name));
 
783
      [BExpr(name, tgt)]
 
784
  | a, b ->
 
785
      if (verbose && traceActive "patchDebug") then (
 
786
        (trace "patchDebug" (dprintf "mismatching expression\n"));
 
787
        (printExpr a);
 
788
        (printExpr b)
 
789
      );
 
790
      raise NoMatch
 
791
end
 
792
 
 
793
and unifyInitExpr (pat : init_expression) (tgt : init_expression) : binding list =
 
794
begin
 
795
  (*
 
796
    Cprint.print_init_expression pat;  Cprint.force_new_line ();
 
797
    Cprint.print_init_expression tgt;  Cprint.force_new_line ();
 
798
    Cprint.flush ();
 
799
  *)
 
800
 
 
801
  match pat, tgt with
 
802
  | NO_INIT, NO_INIT -> []
 
803
  | SINGLE_INIT(pe), SINGLE_INIT(te) ->
 
804
      (unifyExpr pe te)
 
805
  | COMPOUND_INIT(plist),
 
806
    COMPOUND_INIT(tlist) -> (
 
807
      let rec loop plist tlist =
 
808
        match plist, tlist with
 
809
        | ((pwhat, piexpr) :: prest),
 
810
          ((twhat, tiexpr) :: trest) ->
 
811
            (mustEq pwhat twhat);
 
812
            (unifyInitExpr piexpr tiexpr) @
 
813
            (loop prest trest)
 
814
        | [], [] -> []
 
815
        | _, _ -> (
 
816
            if verbose then
 
817
              (trace "patchDebug" (dprintf "mismatching compound init exprs\n"));
 
818
            raise NoMatch
 
819
          )
 
820
      in
 
821
      (loop plist tlist)
 
822
    )
 
823
  | _,_ -> (
 
824
      if verbose then
 
825
        (trace "patchDebug" (dprintf "mismatching init exprs\n"));
 
826
      raise NoMatch
 
827
    )
 
828
end
 
829
 
 
830
and unifyExprs (pat : expression list) (tgt : expression list) : binding list =
 
831
  (unifyList pat tgt unifyExpr)
 
832
 
 
833
 
 
834
(* given the list of bindings 'b', substitute them into 'd' to yield a new definition *)
 
835
and substDefn (bindings : binding list) (defn : definition) : definition =
 
836
begin
 
837
  if verbose then
 
838
    (trace "patchDebug" (dprintf "substDefn with %d bindings\n" (List.length bindings)));
 
839
  (printDefn defn);
 
840
 
 
841
  (* apply the transformation *)
 
842
  match (visitCabsDefinition (new substitutor bindings :> cabsVisitor) defn) with
 
843
  | [d] -> d    (* expect a singleton list *)
 
844
  | _ -> (failwith "didn't get a singleton list where I expected one")
 
845
end
 
846
 
 
847
 
 
848
(* end of file *)