source: src/common/AST.ma @ 879

Last change on this file since 879 was 879, checked in by campbell, 8 years ago

Refine "AST" types to include size/signedness information.

File size: 20.2 KB
Line 
1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
7(*  Copyright Institut National de Recherche en Informatique et en     *)
8(*  Automatique.  All rights reserved.  This file is distributed       *)
9(*  under the terms of the GNU General Public License as published by  *)
10(*  the Free Software Foundation, either version 2 of the License, or  *)
11(*  (at your option) any later version.  This file is also distributed *)
12(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16(* * This file defines a number of data types and operations used in
17  the abstract syntax trees of many of the intermediate languages. *)
18
19include "basics/types.ma".
20include "common/Integers.ma".
21include "common/Floats.ma".
22include "ASM/BitVector.ma".
23include "common/Identifiers.ma".
24
25
26(* * * Syntactic elements *)
27
28(* Global variables and functions are represented by identifiers with the
29   tag for symbols.  Note that Clight also uses them for locals due to
30   the ambiguous syntax. *)
31
32axiom SymbolTag : String.
33
34definition ident ≝ identifier SymbolTag.
35
36definition ident_eq : ∀x,y:ident. (x=y) + (x≠y) ≝ identifier_eq ?.
37
38definition ident_of_nat : nat → ident ≝ identifier_of_nat ?.
39
40(* XXX backend is currently using untagged words as identifiers. *)
41definition Identifier ≝ Word.
42
43definition Immediate ≝ nat. (* XXX is this the best place to put this? *)
44
45(* Memory spaces *)
46
47inductive region : Type[0] ≝
48  | Any : region
49  | Data : region
50  | IData : region
51  | PData : region
52  | XData : region
53  | Code : region.
54
55definition eq_region : region → region → bool ≝
56λr1,r2.
57  match r1 with
58  [ Any ⇒   match r2 with [ Any ⇒ true | _ ⇒ false ]
59  | Data ⇒  match r2 with [ Data ⇒ true | _ ⇒ false ]
60  | IData ⇒ match r2 with [ IData ⇒ true | _ ⇒ false ]
61  | PData ⇒ match r2 with [ PData ⇒ true | _ ⇒ false ]
62  | XData ⇒ match r2 with [ XData ⇒ true | _ ⇒ false ]
63  | Code ⇒  match r2 with [ Code ⇒ true | _ ⇒ false ]
64  ].
65
66lemma eq_region_elim : ∀P:bool → Type[0]. ∀r1,r2.
67  (r1 = r2 → P true) → (r1 ≠ r2 → P false) →
68  P (eq_region r1 r2).
69#P #r1 #r2 cases r1; cases r2; #Ptrue #Pfalse
70try ( @Ptrue // )
71@Pfalse % #E destruct;
72qed.
73
74definition eq_region_dec : ∀r1,r2:region. (r1=r2)+(r1≠r2).
75#r1 #r2 @(eq_region_elim ? r1 r2) /2/; qed.
76
77definition size_pointer : region → nat ≝
78λsp. match sp with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
79
80(* We maintain some reasonable type information through the front end of the
81   compiler. *)
82
83inductive signedness : Type[0] ≝
84  | Signed: signedness
85  | Unsigned: signedness.
86
87inductive intsize : Type[0] ≝
88  | I8: intsize
89  | I16: intsize
90  | I32: intsize.
91
92(* * Float types come in two sizes: 32 bits (single precision)
93  and 64-bit (double precision). *)
94
95inductive floatsize : Type[0] ≝
96  | F32: floatsize
97  | F64: floatsize.
98
99inductive typ : Type[0] ≝
100  | ASTint : intsize → signedness → typ
101  | ASTptr : region → typ
102  | ASTfloat : floatsize → typ.
103
104(* XXX aliases *)
105definition SigType ≝ typ.
106definition SigType_Int ≝ ASTint I32 Unsigned.
107(*
108| SigType_Float: SigType
109*)
110definition SigType_Ptr ≝ ASTptr Any.
111
112definition size_intsize : intsize → nat ≝
113λsz. match sz with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4].
114
115definition size_floatsize : floatsize → nat ≝
116λsz. match sz with [ F32 ⇒ 4 | F64 ⇒ 8 ].
117
118definition typesize : typ → nat ≝ λty.
119  match ty with
120  [ ASTint sz _ ⇒ size_intsize sz
121  | ASTptr r ⇒ size_pointer r
122  | ASTfloat sz ⇒ size_floatsize sz ].
123
124lemma typesize_pos: ∀ty. typesize ty > 0.
125* *; try * /2/ qed.
126
127lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2).
128* * * *; try *; try *; try (%1 @refl) %2 @nmk #H destruct qed.
129
130lemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2).
131#t1 #t2 cases t1 cases t2
132[ %1 @refl
133| 2,3: #ty %2 % #H destruct
134| #ty1 #ty2 elim (typ_eq ty1 ty2) #E [ %1 >E @refl | %2 % #E' destruct cases E /2/
135]
136qed.
137
138(* * Additionally, function definitions and function calls are annotated
139  by function signatures indicating the number and types of arguments,
140  as well as the type of the returned value if any.  These signatures
141  are used in particular to determine appropriate calling conventions
142  for the function. *)
143
144record signature : Type[0] ≝ {
145  sig_args: list typ;
146  sig_res: option typ
147}.
148
149(* XXX aliases *)
150definition Signature ≝ signature.
151definition signature_args ≝ sig_args.
152definition signature_return ≝ sig_res.
153
154definition proj_sig_res : signature → typ ≝ λs.
155  match sig_res s with
156  [ None ⇒ ASTint I32 Unsigned
157  | Some t ⇒ t
158  ].
159
160(* * Memory accesses (load and store instructions) are annotated by
161  a ``memory chunk'' indicating the type, size and signedness of the
162  chunk of memory being accessed. *)
163
164inductive memory_chunk : Type[0] ≝
165  | Mint8signed : memory_chunk     (*r 8-bit signed integer *)
166  | Mint8unsigned : memory_chunk   (*r 8-bit unsigned integer *)
167  | Mint16signed : memory_chunk    (*r 16-bit signed integer *)
168  | Mint16unsigned : memory_chunk  (*r 16-bit unsigned integer *)
169  | Mint32 : memory_chunk          (*r 32-bit integer, or pointer *)
170  | Mfloat32 : memory_chunk        (*r 32-bit single-precision float *)
171  | Mfloat64 : memory_chunk        (*r 64-bit double-precision float *)
172  | Mpointer : region → memory_chunk. (* pointer addressing given region *)
173
174(* * Initialization data for global variables. *)
175
176inductive init_data: Type[0] ≝
177  | Init_int8: int → init_data
178  | Init_int16: int → init_data
179  | Init_int32: int → init_data
180  | Init_float32: float → init_data
181  | Init_float64: float → init_data
182  | Init_space: nat → init_data
183  | Init_null: region → init_data
184  | Init_addrof: region → ident → int → init_data.   (*r address of symbol + offset *)
185
186(* * Whole programs consist of:
187- a collection of function definitions (name and description);
188- the name of the ``main'' function that serves as entry point in the program;
189- a collection of global variable declarations, consisting of
190  a name, initialization data, and additional information.
191
192The type of function descriptions and that of additional information
193for variables vary among the various intermediate languages and are
194taken as parameters to the [program] type.  The other parts of whole
195programs are common to all languages. *)
196
197record program (F,V: Type[0]) : Type[0] := {
198  prog_funct: list (ident × F);
199  prog_main: ident;
200  prog_vars: list (ident × (list init_data) × region × V)
201}.
202
203(*
204definition prog_funct_names ≝ λF,V: Type[0]. λp: program F V.
205  map ?? (fst ident F) (prog_funct ?? p).
206
207definition prog_var_names ≝ λF,V: Type[0]. λp: program F V.
208  map ?? (λx: ident × (list init_data) × region × V. fst ?? (fst ?? (fst ?? x))) (prog_vars ?? p).
209
210(* * * Generic transformations over programs *)
211
212(* * We now define a general iterator over programs that applies a given
213  code transformation function to all function descriptions and leaves
214  the other parts of the program unchanged. *)
215(*
216Section TRANSF_PROGRAM.
217
218Variable A B V: Type.
219Variable transf: A -> B.
220*)
221
222definition transf_program : ∀A,B. (A → B) → list (ident × A) → list (ident × B) ≝
223λA,B,transf,l.
224  map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l.
225
226definition transform_program : ∀A,B,V. (A → B) → program A V → program B V ≝
227λA,B,V,transf,p.
228  mk_program B V
229    (transf_program ?? transf (prog_funct A V p))
230    (prog_main A V p)
231    (prog_vars A V p).
232(*
233lemma transform_program_function:
234  ∀A,B,V,transf,p,i,tf.
235  in_list ? 〈i, tf〉 (prog_funct ?? (transform_program A B V transf p)) →
236  ∃f. in_list ? 〈i, f〉 (prog_funct ?? p) ∧ transf f = tf.
237normalize; #A #B #V #transf #p #i #tf #H elim (list_in_map_inv ????? H);
238#x elim x; #i' #tf' *; #e #H destruct; %{tf'} /2/;
239qed.
240*)
241(*
242End TRANSF_PROGRAM.
243
244(** The following is a variant of [transform_program] where the
245  code transformation function can fail and therefore returns an
246  option type. *)
247
248Open Local Scope error_monad_scope.
249Open Local Scope string_scope.
250
251Section MAP_PARTIAL.
252
253Variable A B C: Type.
254Variable prefix_errmsg: A -> errmsg.
255Variable f: B -> res C.
256*)
257definition map_partial : ∀A,B,C:Type[0]. (B → res C) →
258                         list (A × B) → res (list (A × C)) ≝
259λA,B,C,f. mmap ?? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉).
260(*
261Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
262  match l with
263  | nil => OK nil
264  | (a, b) :: rem =>
265      match f b with
266      | Error msg => Error (prefix_errmsg a ++ msg)%list
267      | OK c =>
268          do rem' <- map_partial rem;
269          OK ((a, c) :: rem')
270      end
271  end.
272
273Remark In_map_partial:
274  forall l l' a c,
275  map_partial l = OK l' ->
276  In (a, c) l' ->
277  exists b, In (a, b) l /\ f b = OK c.
278Proof.
279  induction l; simpl.
280  intros. inv H. elim H0.
281  intros until c. destruct a as [a1 b1].
282  caseEq (f b1); try congruence.
283  intro c1; intros. monadInv H0.
284  elim H1; intro. inv H0. exists b1; auto.
285  exploit IHl; eauto. intros [b [P Q]]. exists b; auto.
286Qed.
287
288Remark map_partial_forall2:
289  forall l l',
290  map_partial l = OK l' ->
291  list_forall2
292    (fun (a_b: A * B) (a_c: A * C) =>
293       fst a_b = fst a_c /\ f (snd a_b) = OK (snd a_c))
294    l l'.
295Proof.
296  induction l; simpl.
297  intros. inv H. constructor.
298  intro l'. destruct a as [a b].
299  caseEq (f b). 2: congruence. intro c; intros. monadInv H0. 
300  constructor. simpl. auto. auto.
301Qed.
302
303End MAP_PARTIAL.
304
305Remark map_partial_total:
306  forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)),
307  map_partial prefix (fun b => OK (f b)) l =
308  OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l).
309Proof.
310  induction l; simpl.
311  auto.
312  destruct a as [a1 b1]. rewrite IHl. reflexivity.
313Qed.
314
315Remark map_partial_identity:
316  forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)),
317  map_partial prefix (fun b => OK b) l = OK l.
318Proof.
319  induction l; simpl.
320  auto.
321  destruct a as [a1 b1]. rewrite IHl. reflexivity.
322Qed.
323
324Section TRANSF_PARTIAL_PROGRAM.
325
326Variable A B V: Type.
327Variable transf_partial: A -> res B.
328
329Definition prefix_funct_name (id: ident) : errmsg :=
330  MSG "In function " :: CTX id :: MSG ": " :: nil.
331*)
332definition transform_partial_program : ∀A,B,V. (A → res B) → program A V → res (program B V) ≝
333λA,B,V,transf_partial,p.
334  do fl ← map_partial … (*prefix_funct_name*) transf_partial (prog_funct ?? p);
335  OK ? (mk_program … fl (prog_main ?? p) (prog_vars ?? p)).
336(*
337Lemma transform_partial_program_function:
338  forall p tp i tf,
339  transform_partial_program p = OK tp ->
340  In (i, tf) tp.(prog_funct) ->
341  exists f, In (i, f) p.(prog_funct) /\ transf_partial f = OK tf.
342Proof.
343  intros. monadInv H. simpl in H0. 
344  eapply In_map_partial; eauto.
345Qed.
346
347Lemma transform_partial_program_main:
348  forall p tp,
349  transform_partial_program p = OK tp ->
350  tp.(prog_main) = p.(prog_main).
351Proof.
352  intros. monadInv H. reflexivity.
353Qed.
354
355Lemma transform_partial_program_vars:
356  forall p tp,
357  transform_partial_program p = OK tp ->
358  tp.(prog_vars) = p.(prog_vars).
359Proof.
360  intros. monadInv H. reflexivity.
361Qed.
362
363End TRANSF_PARTIAL_PROGRAM.
364
365(** The following is a variant of [transform_program_partial] where
366  both the program functions and the additional variable information
367  are transformed by functions that can fail. *)
368
369Section TRANSF_PARTIAL_PROGRAM2.
370
371Variable A B V W: Type.
372Variable transf_partial_function: A -> res B.
373Variable transf_partial_variable: V -> res W.
374
375Definition prefix_var_name (id_init: ident * list init_data) : errmsg :=
376  MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil.
377*)
378definition transform_partial_program2 : ∀A,B,V,W. (A → res B) → (V → res W) →
379                                        program A V → res (program B W) ≝
380λA,B,V,W, transf_partial_function, transf_partial_variable, p.
381  do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p);
382  do vl ← map_partial … (*prefix_var_name*) transf_partial_variable (prog_vars ?? p);
383  OK ? (mk_program … fl (prog_main ?? p) vl).
384(*
385Lemma transform_partial_program2_function:
386  forall p tp i tf,
387  transform_partial_program2 p = OK tp ->
388  In (i, tf) tp.(prog_funct) ->
389  exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf.
390Proof.
391  intros. monadInv H. 
392  eapply In_map_partial; eauto.
393Qed.
394
395Lemma transform_partial_program2_variable:
396  forall p tp i tv,
397  transform_partial_program2 p = OK tp ->
398  In (i, tv) tp.(prog_vars) ->
399  exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = OK tv.
400Proof.
401  intros. monadInv H.
402  eapply In_map_partial; eauto.
403Qed.
404
405Lemma transform_partial_program2_main:
406  forall p tp,
407  transform_partial_program2 p = OK tp ->
408  tp.(prog_main) = p.(prog_main).
409Proof.
410  intros. monadInv H. reflexivity.
411Qed.
412
413End TRANSF_PARTIAL_PROGRAM2.
414
415(** The following is a relational presentation of
416  [transform_program_partial2].  Given relations between function
417  definitions and between variable information, it defines a relation
418  between programs stating that the two programs have the same shape
419  (same global names, etc) and that identically-named function definitions
420  are variable information are related. *)
421
422Section MATCH_PROGRAM.
423
424Variable A B V W: Type.
425Variable match_fundef: A -> B -> Prop.
426Variable match_varinfo: V -> W -> Prop.
427
428Definition match_funct_entry (x1: ident * A) (x2: ident * B) :=
429  match x1, x2 with
430  | (id1, fn1), (id2, fn2) => id1 = id2 /\ match_fundef fn1 fn2
431  end.
432
433Definition match_var_entry (x1: ident * list init_data * V) (x2: ident * list init_data * W) :=
434  match x1, x2 with
435  | (id1, init1, info1), (id2, init2, info2) => id1 = id2 /\ init1 = init2 /\ match_varinfo info1 info2
436  end.
437
438Definition match_program (p1: program A V) (p2: program B W) : Prop :=
439  list_forall2 match_funct_entry p1.(prog_funct) p2.(prog_funct)
440  /\ p1.(prog_main) = p2.(prog_main)
441  /\ list_forall2 match_var_entry p1.(prog_vars) p2.(prog_vars).
442
443End MATCH_PROGRAM.
444
445Remark transform_partial_program2_match:
446  forall (A B V W: Type)
447         (transf_partial_function: A -> res B)
448         (transf_partial_variable: V -> res W)
449         (p: program A V) (tp: program B W),
450  transform_partial_program2 transf_partial_function transf_partial_variable p = OK tp ->
451  match_program
452    (fun fd tfd => transf_partial_function fd = OK tfd)
453    (fun info tinfo => transf_partial_variable info = OK tinfo)
454    p tp.
455Proof.
456  intros. monadInv H. split.
457  apply list_forall2_imply with
458    (fun (ab: ident * A) (ac: ident * B) =>
459       fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)).
460  eapply map_partial_forall2. eauto.
461  intros. destruct v1; destruct v2; simpl in *. auto.
462  split. auto.
463  apply list_forall2_imply with
464    (fun (ab: ident * list init_data * V) (ac: ident * list init_data * W) =>
465       fst ab = fst ac /\ transf_partial_variable (snd ab) = OK (snd ac)).
466  eapply map_partial_forall2. eauto.
467  intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence.
468Qed.
469*)
470(* * * External functions *)
471
472(* * For most languages, the functions composing the program are either
473  internal functions, defined within the language, or external functions
474  (a.k.a. system calls) that emit an event when applied.  We define
475  a type for such functions and some generic transformation functions. *)
476
477record external_function : Type[0] ≝ {
478  ef_id: ident;
479  ef_sig: signature
480}.
481
482definition ExternalFunction ≝ external_function.
483definition external_function_tag ≝ ef_id.
484definition external_function_sig ≝ ef_sig.
485
486inductive fundef (F: Type[0]): Type[0] ≝
487  | Internal: F → fundef F
488  | External: external_function → fundef F.
489
490(* Implicit Arguments External [F]. *)
491(*
492Section TRANSF_FUNDEF.
493
494Variable A B: Type.
495Variable transf: A -> B.
496*)
497definition transf_fundef : ∀A,B. (A→B) → fundef A → fundef B ≝
498λA,B,transf,fd.
499  match fd with
500  [ Internal f ⇒ Internal ? (transf f)
501  | External ef ⇒ External ? ef
502  ].
503
504(*
505End TRANSF_FUNDEF.
506
507Section TRANSF_PARTIAL_FUNDEF.
508
509Variable A B: Type.
510Variable transf_partial: A -> res B.
511*)
512
513definition transf_partial_fundef : ∀A,B. (A → res B) → fundef A → res (fundef B) ≝
514λA,B,transf_partial,fd.
515  match fd with
516  [ Internal f ⇒ do f' ← transf_partial f; OK ? (Internal ? f')
517  | External ef ⇒ OK ? (External ? ef)
518  ].
519(*
520End TRANSF_PARTIAL_FUNDEF.
521*)
522*)
523
524
525
526(* Partially merged stuff derived from the prototype cerco compiler. *)
527
528definition bool_to_Prop ≝
529 λb. match b with [ true ⇒ True | false ⇒ False ].
530
531(* dpm: should go to standard library *)
532let rec member (i: ident) (eq_i: ident → ident → bool)
533               (g: list ident) on g: Prop ≝
534  match g with
535  [ nil ⇒ False
536  | cons hd tl ⇒
537      bool_to_Prop (eq_i hd i) ∨ member i eq_i tl
538  ].
539
540(* TODO: merge in comparison definitions from Integers.ma. *)
541inductive Compare: Type[0] ≝
542  Compare_Equal: Compare
543| Compare_NotEqual: Compare
544| Compare_Less: Compare
545| Compare_Greater: Compare
546| Compare_LessEqual: Compare
547| Compare_GreaterEqual: Compare.
548
549(* XXX unused definitions
550inductive Cast: Type[0] ≝
551  Cast_Int: Byte → Cast
552| Cast_AddrSymbol: Identifier → Cast
553| Cast_StackOffset: Immediate → Cast.
554
555inductive Data: Type[0] ≝
556  Data_Reserve: nat → Data
557| Data_Int8: Byte → Data
558| Data_Int16: Word → Data.
559
560inductive DataSize: Type[0] ≝
561  DataSize_Byte: DataSize
562| DataSize_HalfWord: DataSize
563| DataSize_Word: DataSize.
564*)
565
566definition Trace ≝ list Identifier.
567
568(* dpm: how are floats represented? *)
569inductive cast: Type[0] ≝
570  | cast_int: Byte → cast                    (* integer constant *)
571  | cast_float: Byte → cast                  (* float constant *)
572  | cast_addr_symbol: ident → cast      (* address of a global symbol *)
573  | cast_stack_offset: Byte → cast.
574
575inductive op1: Type[0] ≝
576  | op_cast8_unsigned: op1   (**r 8-bit zero extension  *)
577  | op_cast8_signed: op1     (**r 8-bit sign extension  *)
578  | op_cast16_unsigned: op1  (**r 16-bit zero extension  *)
579  | op_cast16_signed: op1    (**r 16-bit sign extension *)
580  | op_neg_int: op1          (**r integer opposite *)
581  | op_not_bool: op1         (**r boolean negation  *)
582  | op_not_int: op1          (**r bitwise complement  *)
583  | op_negf: op1             (**r float opposite *)
584  | op_absf: op1             (**r float absolute value *)
585  | op_single_of_float: op1  (**r float truncation *)
586  | op_int_of_float: op1     (**r signed integer to float *)
587  | op_intu_of_float: op1    (**r unsigned integer to float *)
588  | op_float_of_int: op1     (**r float to signed integer *)
589  | op_float_of_intu: op1    (**r float to unsigned integer *)
590  | op_id: op1               (**r identity *)
591  | op_ptr_of_int: op1       (**r int to pointer *)
592  | op_int_of_ptr: op1.      (**r pointer to int *)
593
594inductive op2: Type[0] ≝
595  | op_add: op2         (**r integer addition *)
596  | op_sub: op2         (**r integer subtraction *)
597  | op_mul: op2         (**r integer multiplication *)
598  | op_div: op2         (**r integer signed division *)
599  | op_divu: op2        (**r integer unsigned division *)
600  | op_mod: op2         (**r integer signed modulus *)
601  | op_modu: op2        (**r integer unsigned modulus *)
602  | op_and: op2         (**r bitwise ``and'' *)
603  | op_or: op2          (**r bitwise ``or'' *)
604  | op_xor: op2         (**r bitwise ``xor'' *)
605  | op_shl: op2         (**r left shift *)
606  | op_shr: op2         (**r right signed shift *)
607  | op_shru: op2        (**r right unsigned shift *)
608  | op_addf: op2        (**r float addition *)
609  | op_subf: op2        (**r float subtraction *)
610  | op_mulf: op2        (**r float multiplication *)
611  | op_divf: op2        (**r float division *)
612  | op_cmp: Compare → op2   (**r integer signed comparison *)
613  | op_cmpu: Compare → op2  (**r integer unsigned comparison *)
614  | op_cmpf: Compare → op2  (**r float comparison *)
615  | op_addp: op2        (**r addition for a pointer and an integer *)
616  | op_subp: op2        (**r substraction for a pointer and a integer *)
617  | op_cmpp: Compare → op2. (**r pointer comparaison *)
Note: See TracBrowser for help on using the repository browser.