source: src/common/AST.ma @ 882

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

Fix up fragile proofs for current version of matita.

File size: 20.6 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
174definition typ_of_memory_chunk : memory_chunk → typ ≝
175λc. match c with
176[ Mint8signed ⇒ ASTint I8 Signed
177| Mint8unsigned ⇒ ASTint I8 Unsigned
178| Mint16signed ⇒ ASTint I16 Signed
179| Mint16unsigned ⇒ ASTint I16 Unsigned
180| Mint32 ⇒ ASTint I32 Unsigned (* XXX signed? *)
181| Mfloat32 ⇒ ASTfloat F32
182| Mfloat64 ⇒ ASTfloat F64
183| Mpointer r ⇒ ASTptr r
184].
185
186(* * Initialization data for global variables. *)
187
188inductive init_data: Type[0] ≝
189  | Init_int8: int → init_data
190  | Init_int16: int → init_data
191  | Init_int32: int → init_data
192  | Init_float32: float → init_data
193  | Init_float64: float → init_data
194  | Init_space: nat → init_data
195  | Init_null: region → init_data
196  | Init_addrof: region → ident → int → init_data.   (*r address of symbol + offset *)
197
198(* * Whole programs consist of:
199- a collection of function definitions (name and description);
200- the name of the ``main'' function that serves as entry point in the program;
201- a collection of global variable declarations, consisting of
202  a name, initialization data, and additional information.
203
204The type of function descriptions and that of additional information
205for variables vary among the various intermediate languages and are
206taken as parameters to the [program] type.  The other parts of whole
207programs are common to all languages. *)
208
209record program (F,V: Type[0]) : Type[0] := {
210  prog_funct: list (ident × F);
211  prog_main: ident;
212  prog_vars: list (ident × (list init_data) × region × V)
213}.
214
215
216definition prog_funct_names ≝ λF,V: Type[0]. λp: program F V.
217  map ?? (fst ident F) (prog_funct ?? p).
218
219definition prog_var_names ≝ λF,V: Type[0]. λp: program F V.
220  map ?? (λx: ident × (list init_data) × region × V. fst ?? (fst ?? (fst ?? x))) (prog_vars ?? p).
221
222(* * * Generic transformations over programs *)
223
224(* * We now define a general iterator over programs that applies a given
225  code transformation function to all function descriptions and leaves
226  the other parts of the program unchanged. *)
227(*
228Section TRANSF_PROGRAM.
229
230Variable A B V: Type.
231Variable transf: A -> B.
232*)
233
234definition transf_program : ∀A,B. (A → B) → list (ident × A) → list (ident × B) ≝
235λA,B,transf,l.
236  map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l.
237
238definition transform_program : ∀A,B,V. (A → B) → program A V → program B V ≝
239λA,B,V,transf,p.
240  mk_program B V
241    (transf_program ?? transf (prog_funct A V p))
242    (prog_main A V p)
243    (prog_vars A V p).
244(*
245lemma transform_program_function:
246  ∀A,B,V,transf,p,i,tf.
247  in_list ? 〈i, tf〉 (prog_funct ?? (transform_program A B V transf p)) →
248  ∃f. in_list ? 〈i, f〉 (prog_funct ?? p) ∧ transf f = tf.
249normalize; #A #B #V #transf #p #i #tf #H elim (list_in_map_inv ????? H);
250#x elim x; #i' #tf' *; #e #H destruct; %{tf'} /2/;
251qed.
252*)
253(*
254End TRANSF_PROGRAM.
255
256(** The following is a variant of [transform_program] where the
257  code transformation function can fail and therefore returns an
258  option type. *)
259
260Open Local Scope error_monad_scope.
261Open Local Scope string_scope.
262
263Section MAP_PARTIAL.
264
265Variable A B C: Type.
266Variable prefix_errmsg: A -> errmsg.
267Variable f: B -> res C.
268*)
269definition map_partial : ∀A,B,C:Type[0]. (B → res C) →
270                         list (A × B) → res (list (A × C)) ≝
271λA,B,C,f. mmap ?? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉).
272(*
273Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
274  match l with
275  | nil => OK nil
276  | (a, b) :: rem =>
277      match f b with
278      | Error msg => Error (prefix_errmsg a ++ msg)%list
279      | OK c =>
280          do rem' <- map_partial rem;
281          OK ((a, c) :: rem')
282      end
283  end.
284
285Remark In_map_partial:
286  forall l l' a c,
287  map_partial l = OK l' ->
288  In (a, c) l' ->
289  exists b, In (a, b) l /\ f b = OK c.
290Proof.
291  induction l; simpl.
292  intros. inv H. elim H0.
293  intros until c. destruct a as [a1 b1].
294  caseEq (f b1); try congruence.
295  intro c1; intros. monadInv H0.
296  elim H1; intro. inv H0. exists b1; auto.
297  exploit IHl; eauto. intros [b [P Q]]. exists b; auto.
298Qed.
299
300Remark map_partial_forall2:
301  forall l l',
302  map_partial l = OK l' ->
303  list_forall2
304    (fun (a_b: A * B) (a_c: A * C) =>
305       fst a_b = fst a_c /\ f (snd a_b) = OK (snd a_c))
306    l l'.
307Proof.
308  induction l; simpl.
309  intros. inv H. constructor.
310  intro l'. destruct a as [a b].
311  caseEq (f b). 2: congruence. intro c; intros. monadInv H0. 
312  constructor. simpl. auto. auto.
313Qed.
314
315End MAP_PARTIAL.
316
317Remark map_partial_total:
318  forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)),
319  map_partial prefix (fun b => OK (f b)) l =
320  OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l).
321Proof.
322  induction l; simpl.
323  auto.
324  destruct a as [a1 b1]. rewrite IHl. reflexivity.
325Qed.
326
327Remark map_partial_identity:
328  forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)),
329  map_partial prefix (fun b => OK b) l = OK l.
330Proof.
331  induction l; simpl.
332  auto.
333  destruct a as [a1 b1]. rewrite IHl. reflexivity.
334Qed.
335
336Section TRANSF_PARTIAL_PROGRAM.
337
338Variable A B V: Type.
339Variable transf_partial: A -> res B.
340
341Definition prefix_funct_name (id: ident) : errmsg :=
342  MSG "In function " :: CTX id :: MSG ": " :: nil.
343*)
344definition transform_partial_program : ∀A,B,V. (A → res B) → program A V → res (program B V) ≝
345λA,B,V,transf_partial,p.
346  do fl ← map_partial … (*prefix_funct_name*) transf_partial (prog_funct ?? p);
347  OK ? (mk_program … fl (prog_main ?? p) (prog_vars ?? p)).
348(*
349Lemma transform_partial_program_function:
350  forall p tp i tf,
351  transform_partial_program p = OK tp ->
352  In (i, tf) tp.(prog_funct) ->
353  exists f, In (i, f) p.(prog_funct) /\ transf_partial f = OK tf.
354Proof.
355  intros. monadInv H. simpl in H0. 
356  eapply In_map_partial; eauto.
357Qed.
358
359Lemma transform_partial_program_main:
360  forall p tp,
361  transform_partial_program p = OK tp ->
362  tp.(prog_main) = p.(prog_main).
363Proof.
364  intros. monadInv H. reflexivity.
365Qed.
366
367Lemma transform_partial_program_vars:
368  forall p tp,
369  transform_partial_program p = OK tp ->
370  tp.(prog_vars) = p.(prog_vars).
371Proof.
372  intros. monadInv H. reflexivity.
373Qed.
374
375End TRANSF_PARTIAL_PROGRAM.
376
377(** The following is a variant of [transform_program_partial] where
378  both the program functions and the additional variable information
379  are transformed by functions that can fail. *)
380
381Section TRANSF_PARTIAL_PROGRAM2.
382
383Variable A B V W: Type.
384Variable transf_partial_function: A -> res B.
385Variable transf_partial_variable: V -> res W.
386
387Definition prefix_var_name (id_init: ident * list init_data) : errmsg :=
388  MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil.
389*)
390definition transform_partial_program2 : ∀A,B,V,W. (A → res B) → (V → res W) →
391                                        program A V → res (program B W) ≝
392λA,B,V,W, transf_partial_function, transf_partial_variable, p.
393  do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p);
394  do vl ← map_partial … (*prefix_var_name*) transf_partial_variable (prog_vars ?? p);
395  OK ? (mk_program … fl (prog_main ?? p) vl).
396(*
397Lemma transform_partial_program2_function:
398  forall p tp i tf,
399  transform_partial_program2 p = OK tp ->
400  In (i, tf) tp.(prog_funct) ->
401  exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf.
402Proof.
403  intros. monadInv H. 
404  eapply In_map_partial; eauto.
405Qed.
406
407Lemma transform_partial_program2_variable:
408  forall p tp i tv,
409  transform_partial_program2 p = OK tp ->
410  In (i, tv) tp.(prog_vars) ->
411  exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = OK tv.
412Proof.
413  intros. monadInv H.
414  eapply In_map_partial; eauto.
415Qed.
416
417Lemma transform_partial_program2_main:
418  forall p tp,
419  transform_partial_program2 p = OK tp ->
420  tp.(prog_main) = p.(prog_main).
421Proof.
422  intros. monadInv H. reflexivity.
423Qed.
424
425End TRANSF_PARTIAL_PROGRAM2.
426
427(** The following is a relational presentation of
428  [transform_program_partial2].  Given relations between function
429  definitions and between variable information, it defines a relation
430  between programs stating that the two programs have the same shape
431  (same global names, etc) and that identically-named function definitions
432  are variable information are related. *)
433
434Section MATCH_PROGRAM.
435
436Variable A B V W: Type.
437Variable match_fundef: A -> B -> Prop.
438Variable match_varinfo: V -> W -> Prop.
439
440Definition match_funct_entry (x1: ident * A) (x2: ident * B) :=
441  match x1, x2 with
442  | (id1, fn1), (id2, fn2) => id1 = id2 /\ match_fundef fn1 fn2
443  end.
444
445Definition match_var_entry (x1: ident * list init_data * V) (x2: ident * list init_data * W) :=
446  match x1, x2 with
447  | (id1, init1, info1), (id2, init2, info2) => id1 = id2 /\ init1 = init2 /\ match_varinfo info1 info2
448  end.
449
450Definition match_program (p1: program A V) (p2: program B W) : Prop :=
451  list_forall2 match_funct_entry p1.(prog_funct) p2.(prog_funct)
452  /\ p1.(prog_main) = p2.(prog_main)
453  /\ list_forall2 match_var_entry p1.(prog_vars) p2.(prog_vars).
454
455End MATCH_PROGRAM.
456
457Remark transform_partial_program2_match:
458  forall (A B V W: Type)
459         (transf_partial_function: A -> res B)
460         (transf_partial_variable: V -> res W)
461         (p: program A V) (tp: program B W),
462  transform_partial_program2 transf_partial_function transf_partial_variable p = OK tp ->
463  match_program
464    (fun fd tfd => transf_partial_function fd = OK tfd)
465    (fun info tinfo => transf_partial_variable info = OK tinfo)
466    p tp.
467Proof.
468  intros. monadInv H. split.
469  apply list_forall2_imply with
470    (fun (ab: ident * A) (ac: ident * B) =>
471       fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)).
472  eapply map_partial_forall2. eauto.
473  intros. destruct v1; destruct v2; simpl in *. auto.
474  split. auto.
475  apply list_forall2_imply with
476    (fun (ab: ident * list init_data * V) (ac: ident * list init_data * W) =>
477       fst ab = fst ac /\ transf_partial_variable (snd ab) = OK (snd ac)).
478  eapply map_partial_forall2. eauto.
479  intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence.
480Qed.
481*)
482(* * * External functions *)
483
484(* * For most languages, the functions composing the program are either
485  internal functions, defined within the language, or external functions
486  (a.k.a. system calls) that emit an event when applied.  We define
487  a type for such functions and some generic transformation functions. *)
488
489record external_function : Type[0] ≝ {
490  ef_id: ident;
491  ef_sig: signature
492}.
493
494definition ExternalFunction ≝ external_function.
495definition external_function_tag ≝ ef_id.
496definition external_function_sig ≝ ef_sig.
497
498inductive fundef (F: Type[0]): Type[0] ≝
499  | Internal: F → fundef F
500  | External: external_function → fundef F.
501
502(* Implicit Arguments External [F]. *)
503(*
504Section TRANSF_FUNDEF.
505
506Variable A B: Type.
507Variable transf: A -> B.
508*)
509definition transf_fundef : ∀A,B. (A→B) → fundef A → fundef B ≝
510λA,B,transf,fd.
511  match fd with
512  [ Internal f ⇒ Internal ? (transf f)
513  | External ef ⇒ External ? ef
514  ].
515
516(*
517End TRANSF_FUNDEF.
518
519Section TRANSF_PARTIAL_FUNDEF.
520
521Variable A B: Type.
522Variable transf_partial: A -> res B.
523*)
524
525definition transf_partial_fundef : ∀A,B. (A → res B) → fundef A → res (fundef B) ≝
526λA,B,transf_partial,fd.
527  match fd with
528  [ Internal f ⇒ do f' ← transf_partial f; OK ? (Internal ? f')
529  | External ef ⇒ OK ? (External ? ef)
530  ].
531(*
532End TRANSF_PARTIAL_FUNDEF.
533*)
534
535
536
537
538(* Partially merged stuff derived from the prototype cerco compiler. *)
539
540definition bool_to_Prop ≝
541 λb. match b with [ true ⇒ True | false ⇒ False ].
542
543(* dpm: should go to standard library *)
544let rec member (i: ident) (eq_i: ident → ident → bool)
545               (g: list ident) on g: Prop ≝
546  match g with
547  [ nil ⇒ False
548  | cons hd tl ⇒
549      bool_to_Prop (eq_i hd i) ∨ member i eq_i tl
550  ].
551
552(* TODO: merge in comparison definitions from Integers.ma. *)
553inductive Compare: Type[0] ≝
554  Compare_Equal: Compare
555| Compare_NotEqual: Compare
556| Compare_Less: Compare
557| Compare_Greater: Compare
558| Compare_LessEqual: Compare
559| Compare_GreaterEqual: Compare.
560
561(* XXX unused definitions
562inductive Cast: Type[0] ≝
563  Cast_Int: Byte → Cast
564| Cast_AddrSymbol: Identifier → Cast
565| Cast_StackOffset: Immediate → Cast.
566
567inductive Data: Type[0] ≝
568  Data_Reserve: nat → Data
569| Data_Int8: Byte → Data
570| Data_Int16: Word → Data.
571
572inductive DataSize: Type[0] ≝
573  DataSize_Byte: DataSize
574| DataSize_HalfWord: DataSize
575| DataSize_Word: DataSize.
576*)
577
578definition Trace ≝ list Identifier.
579
580(* dpm: how are floats represented? *)
581inductive cast: Type[0] ≝
582  | cast_int: Byte → cast                    (* integer constant *)
583  | cast_float: Byte → cast                  (* float constant *)
584  | cast_addr_symbol: ident → cast      (* address of a global symbol *)
585  | cast_stack_offset: Byte → cast.
586
587inductive op1: Type[0] ≝
588  | op_cast8_unsigned: op1   (**r 8-bit zero extension  *)
589  | op_cast8_signed: op1     (**r 8-bit sign extension  *)
590  | op_cast16_unsigned: op1  (**r 16-bit zero extension  *)
591  | op_cast16_signed: op1    (**r 16-bit sign extension *)
592  | op_neg_int: op1          (**r integer opposite *)
593  | op_not_bool: op1         (**r boolean negation  *)
594  | op_not_int: op1          (**r bitwise complement  *)
595  | op_negf: op1             (**r float opposite *)
596  | op_absf: op1             (**r float absolute value *)
597  | op_single_of_float: op1  (**r float truncation *)
598  | op_int_of_float: op1     (**r signed integer to float *)
599  | op_intu_of_float: op1    (**r unsigned integer to float *)
600  | op_float_of_int: op1     (**r float to signed integer *)
601  | op_float_of_intu: op1    (**r float to unsigned integer *)
602  | op_id: op1               (**r identity *)
603  | op_ptr_of_int: op1       (**r int to pointer *)
604  | op_int_of_ptr: op1.      (**r pointer to int *)
605
606inductive op2: Type[0] ≝
607  | op_add: op2         (**r integer addition *)
608  | op_sub: op2         (**r integer subtraction *)
609  | op_mul: op2         (**r integer multiplication *)
610  | op_div: op2         (**r integer signed division *)
611  | op_divu: op2        (**r integer unsigned division *)
612  | op_mod: op2         (**r integer signed modulus *)
613  | op_modu: op2        (**r integer unsigned modulus *)
614  | op_and: op2         (**r bitwise ``and'' *)
615  | op_or: op2          (**r bitwise ``or'' *)
616  | op_xor: op2         (**r bitwise ``xor'' *)
617  | op_shl: op2         (**r left shift *)
618  | op_shr: op2         (**r right signed shift *)
619  | op_shru: op2        (**r right unsigned shift *)
620  | op_addf: op2        (**r float addition *)
621  | op_subf: op2        (**r float subtraction *)
622  | op_mulf: op2        (**r float multiplication *)
623  | op_divf: op2        (**r float division *)
624  | op_cmp: Compare → op2   (**r integer signed comparison *)
625  | op_cmpu: Compare → op2  (**r integer unsigned comparison *)
626  | op_cmpf: Compare → op2  (**r float comparison *)
627  | op_addp: op2        (**r addition for a pointer and an integer *)
628  | op_subp: op2        (**r substraction for a pointer and a integer *)
629  | op_cmpp: Compare → op2. (**r pointer comparaison *)
Note: See TracBrowser for help on using the repository browser.