Changeset 1059

Timestamp:

Jul 6, 2011, 6:09:39 PM (9 years ago)

Author:

mulligan

Message:

work from today, bit of a mess at the moment

Location:

src

Files:

• ASM/Util.ma (modified) (2 diffs)
• RTLabs/RTLAbstoRTL.ma (modified) (2 diffs)
• common/AST.ma (modified) (3 diffs)
• common/IntValue.ma (modified) (1 diff)

src/ASM/Util.ma

@@ -8 +8 @@
 example daemon: False. generalize in match IMPOSSIBLE; #IMPOSSIBLE destruct(IMPOSSIBLE) qed.
 example not_implemented: False. cases daemon qed.
-  
+
+notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
+ with precedence 10
+for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
+
+let rec reduce 
+  (A: Type[0]) (left: list A) (right: list A) on left ≝
+  match left with
+  [ nil ⇒ 〈〈[ ], [ ]〉, 〈[ ], right〉〉
+  | cons hd tl ⇒
+    match right with
+    [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉
+    | cons hd' tl' ⇒
+      let 〈cleft, cright〉 ≝ reduce A tl tl' in
+      let 〈commonl, restl〉 ≝ cleft in
+      let 〈commonr, restr〉 ≝ cright in
+        〈〈hd :: commonl, restl〉, 〈hd' :: commonr, restr〉〉
+    ]
+  ].
+
+(*
+let rec reduce_strong
+  (A: Type[0]) (left: list A) (right: list A) (prf: | left | = | right |) on left ≝
+  match left return λx. |x| = |right| → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with
+  [ nil ⇒
+    match right return λy. | [ ] | = | y | → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with
+    [ nil ⇒ λnil_nil_prf. dp ? 〈〈[ ], [ ]〉, 〈[ ], [ ]〉〉 ?
+    | cons hd tl ⇒ λnil_cons_asrd_prf. ?
+    ]
+  | cons hd tl ⇒
+    match right return λy. | hd::tl | = | y | → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with
+    [ nil ⇒ λcons_nil_absrd_prf. ?
+    | cons hd' tl' ⇒ λcons_cons_prf. ?
+    ]
+  ] prf.
+*)
+
+axiom reduce_length:
+  ∀A: Type[0].
+  ∀left, right: list A.
+  ∀prf: | left | = | right |.
+    \fst (\fst (reduce A left right)) = \fst (\snd (reduce A left right)).
+    
 let rec map2_opt
   (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C)
@@ -255 +297 @@
     | S o ⇒ f (iterate A f a o)
     ].
-    
-notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
- with precedence 10
-for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
 
 (* Yeah, I probably ought to do something more general... *)

src/RTLabs/RTLAbstoRTL.ma

@@ -4 +4 @@
 include "common/Graphs.ma".
 include "common/Maps.ma".
-include "common/IntValue.ma".
+(* include "common/IntValue.ma". *)
+include "common/FrontEndOps.ma".
 
 definition add_graph ≝
@@ -280 +281 @@
     rtl_st_int r i dest_lbl.
 
-definition translate_cst ≝
-  λcst.
-  λdestrs.
-  λstart_lbl.
-  λdest_lbl.
-  λdef.
-  match cst with
-  [ cast_int i ⇒
-    match destrs with
-    [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
-    | _ ⇒
-      (* this case needs changing when Z is added to stdlib as we are using
-         nats instead of ints here! *)
-      let size ≝ length ? destrs in
-      let is ≝ map … (to_int size) (break size (of_int size (nat_of_bitvector ? i)) size) in
-      let is' ≝ map … (bitvector_of_nat ?) is in
-      let l ≝ map2 … (translate_cst_int_internal dest_lbl) destrs is' ? in
-        adds_graph l start_lbl dest_lbl def
-    ]
-  | cast_addrsymbol id ⇒
-    let 〈r1, r2〉 ≝ make_addr ? destrs ? in
-      add_graph start_lbl (rtl_st_addr r1 r2 id dest_lbl) def
-  | _ ⇒ ?
-  ].
-  | cast_addrsymbol id ⇒
-    match destrs with
-    [ nil ⇒ None ?
-    | cons hd tl ⇒
-      match tl with
-      [ nil ⇒ None ?
-      | cons hd' tl' ⇒
-        Some ? (add_graph start_lbl (rtl_st_addr hd hd' id dest_lbl) def)
-      ]
-    ]
-  | cast_offset off ⇒
-    match destrs with
-    [ nil ⇒ None ?
-    | cons hd tl ⇒
-      match tl with
-      [ nil ⇒ None ?
-      | cons hd' tl' ⇒
-        let 〈def, tmpr〉 ≝ fresh_reg def in
-        adds_graph [
-          rtl_st_stack_addr hd hd' start_lbl;
-          rtl_st_int tmpr off start_lbl;
-          rtl_st_op2 Add hd hd tmpr start_lbl;
-          rtl_st_int tmpr (bitvector_of_nat ? 0) start_lbl;
-          rtl_st_op2 Addc hd' hd' tmpr start_lbl
-        ] start_lbl dest_lbl def
-      ]
-    ]
-  | cast_stack ⇒ ?
-  | cast_sizeof size ⇒ ?
-  (* | cast_float f ⇒ None ? *) (* what are we doing with floats? *)
-  ].
-
-let rec translate_cst cst destrs start_lbl dest_lbl def = match cst with
-
-  | AST.Cst_stack ->
-    let (r1, r2) = make_addr destrs in
-    add_graph start_lbl (RTL.St_stackaddr (r1, r2, dest_lbl)) def
-
-  | AST.Cst_offset off ->
-    let i = concrete_offset off in
-    translate_cst (AST.Cst_int i) destrs start_lbl dest_lbl def
-
-  | AST.Cst_sizeof size ->
-    let i = concrete_size size in
-    translate_cst (AST.Cst_int i) destrs start_lbl dest_lbl def
+axiom translate_cst:
+  ∀cst: constant.
+  ∀destrs: list register.
+  ∀start_lbl: label.
+  ∀dest_lbl: label.
+  ∀def: rtl_internal_function.
+    rtl_internal_function.
+
+definition translate_move_internal ≝
+  λstart_lbl: label.
+  λdestr: register.
+  λsrcr: register.
+    rtl_st_move destr srcr start_lbl.
+
+definition translate_move ≝
+  λdestrs: list register.
+  λsrcrs: list register.
+  λstart_lbl: label.
+  λprf: | destrs | = | srcrs |.
+    let 〈crl, crr〉 ≝ reduce register destrs srcrs in
+    let 〈commonl, restl〉 ≝ crl in
+    let 〈commonr, restr〉 ≝ crr in
+    let f_common ≝ translate_move_internal start_lbl in
+    let translate1 ≝ adds_graph (map2 … f_common commonl commonr ?) in
+    let translate2 ≝ translate_cst (Ointconst ? (repr I8 0)) restl in (* should this be 8? *)
+      add_translates [ translate1 ; translate2 ] start_lbl.
+    
+let rec translate_move destrs srcrs start_lbl =
+  let ((common1, rest1), (common2, rest2)) = MiscPottier.reduce destrs srcrs in
+  let f_common destr srcr = RTL.St_move (destr, srcr, start_lbl) in
+  let translates1 = adds_graph (List.map2 f_common common1 common2) in
+  let translates2 = translate_cst (AST.Cst_int 0) rest1 in
+  add_translates [translates1 ; translates2] start_lbl
 
 definition filter_and_to_list_local_env_internal ≝

src/common/AST.ma

@@ -43 +43 @@
 definition Immediate ≝ nat. (* XXX is this the best place to put this? *)
 
+(* dpm: not needed
 inductive quantity: Type[0] ≝
   | q_int: Byte → quantity
@@ -53 +54 @@
   | size_sum: list abstract_size → abstract_size
   | size_array: nat → abstract_size → abstract_size.
-
-definition abstract_offset ≝ abstract_size × nat. (* nth in size *)
-
-inductive cast: Type[0] ≝
-  | cast_int: Byte → cast                     (* integer constant *)
-(*  | cast_float: float → cast                (* float constant *) *)
-  | cast_addrsymbol: ident → cast      (* address of a global symbol *)
-  | cast_stack: cast                          (* address of the stack *)
-  | cast_offset: abstract_offset → cast       (* offset *)
-  | cast_sizeof: abstract_size → cast.        (* size of a type *)
+*)
 
 (* Memory spaces *)
@@ -191 +183 @@
 definition repr : ∀sz:intsize. nat → bvint sz ≝
 λsz,x. bitvector_of_nat (bitsize_of_intsize sz) x.
-
 
 definition size_floatsize : floatsize → nat ≝

src/common/IntValue.ma

@@ -2 +2 @@
 include "arithmetics/exp.ma".
 include "basics/list.ma".
+include "common/AST.ma".
 include "common/Order.ma".
 
-definition big_int_size ≝ nat.
-axiom big_int: big_int_size → Type[0].
-axiom big_int_int_repr: Type[0].
+definition bvint ≝ λsize. BitVector (bitsize_of_intsize size).
 
-axiom compare: ∀size: big_int_size. big_int size → big_int size → order.
-axiom zero: ∀size: big_int_size. big_int size.
-axiom one: ∀size: big_int_size. big_int size.
-axiom to_signed_int_repr: ∀size: big_int_size. big_int size → big_int_int_repr.
-axiom to_unsigned_int_repr: ∀size: big_int_size. big_int size → big_int_int_repr.
-axiom succ: ∀size: big_int_size. big_int size → big_int size.
-axiom pred: ∀size: big_int_size. big_int size → big_int size.
-axiom add: ∀size: big_int_size. big_int size → big_int size → big_int size.
-axiom add_of: ∀size: big_int_size. big_int size → big_int size → bool.
-axiom sub: ∀size: big_int_size. big_int size → big_int size → big_int size.
-axiom sub_uf: ∀size: big_int_size. big_int size → big_int size → bool.
-axiom mul: ∀size: big_int_size. big_int size → big_int size → big_int size.
-axiom div: ∀size: big_int_size. big_int size → big_int size → big_int size.
-axiom divu: ∀size: big_int_size. big_int size → big_int size → big_int size.
-axiom modulo: ∀size: big_int_size. big_int size → big_int size → big_int size.
-axiom modulou: ∀size: big_int_size. big_int size → big_int size → big_int size.
-axiom eq: ∀size: big_int_size. big_int size → big_int size → bool.
-axiom neq: ∀size: big_int_size. big_int size → big_int size → bool.
-axiom lt: ∀size: big_int_size. big_int size → big_int size → bool.
-axiom ltu: ∀size: big_int_size. big_int size → big_int size → bool.
-axiom le: ∀size: big_int_size. big_int size → big_int size → bool.
-axiom leu: ∀size: big_int_size. big_int size → big_int size → bool.
-axiom gt: ∀size: big_int_size. big_int size → big_int size → bool.
-axiom gtu: ∀size: big_int_size. big_int size → big_int size → bool.
-axiom ge: ∀size: big_int_size. big_int size → big_int size → bool.
-axiom geu: ∀size: big_int_size. big_int size → big_int size → bool.
-axiom neg: ∀size: big_int_size. big_int size → big_int size.
-axiom lognot: ∀size: big_int_size. big_int size → big_int size.
-axiom logand: ∀size: big_int_size. big_int size → big_int size → big_int size.
-axiom logor: ∀size: big_int_size. big_int size → big_int size → big_int size.
-axiom logxor: ∀size: big_int_size. big_int size → big_int size → big_int size.
-axiom shl: ∀size: big_int_size. big_int size → big_int size → big_int size.
-axiom shr: ∀size: big_int_size. big_int size → big_int size → big_int size.
-axiom shrl: ∀size: big_int_size. big_int size → big_int size → big_int size.
-axiom max: ∀size: big_int_size. big_int size → big_int size → big_int size.
-axiom maxu: ∀size: big_int_size. big_int size → big_int size → big_int size.
-axiom min: ∀size: big_int_size. big_int size → big_int size → big_int size.
-axiom minu: ∀size: big_int_size. big_int size → big_int size → big_int size.
-axiom cast: ∀size: big_int_size. big_int_int_repr → big_int size.
-axiom of_int: ∀size: big_int_size. nat → big_int size. (*dpm: replace when Z is added to stdlib *)
-axiom to_int: ∀size: big_int_size. big_int size → nat. (*dpm: """" *)
-axiom zero_ext: ∀size: big_int_size. nat → big_int size → big_int size. (* nat here correct *)
-axiom sign_ext: ∀size: big_int_size. nat → big_int size → big_int size. (* nat here correct *)
-axiom break: ∀size: big_int_size. big_int size → nat → list (big_int size).
-axiom merge: ∀size: big_int_size. list (big_int size) → big_int size.
+definition bitsize_of_intsize: intsize → nat ≝
+  λsize.
+    S (match size with [ I8 ⇒ 7 | I16 ⇒ 15 | I32 ⇒ 31]).
+
+definition of_int ≝
+  λsize.
+  λn.
+    bitvector_of_nat (bitsize_of_intsize size) n.
+
+axiom compare: ∀size: intsize. bvint size → bvint size → order.
+axiom zero: ∀size: intsize. bvint size.
+axiom one: ∀size: intsize. bvint size.
+axiom to_signed_int_repr: ∀size: intsize. bvint size → bvint_int_repr.
+axiom to_unsigned_int_repr: ∀size: intsize. bvint size → bvint_int_repr.
+axiom succ: ∀size: intsize. bvint size → bvint size.
+axiom pred: ∀size: intsize. bvint size → bvint size.
+axiom add: ∀size: intsize. bvint size → bvint size → bvint size.
+axiom add_of: ∀size: intsize. bvint size → bvint size → bool.
+axiom sub: ∀size: intsize. bvint size → bvint size → bvint size.
+axiom sub_uf: ∀size: intsize. bvint size → bvint size → bool.
+axiom mul: ∀size: intsize. bvint size → bvint size → bvint size.
+axiom div: ∀size: intsize. bvint size → bvint size → bvint size.
+axiom divu: ∀size: intsize. bvint size → bvint size → bvint size.
+axiom modulo: ∀size: intsize. bvint size → bvint size → bvint size.
+axiom modulou: ∀size: intsize. bvint size → bvint size → bvint size.
+axiom eq: ∀size: intsize. bvint size → bvint size → bool.
+axiom neq: ∀size: intsize. bvint size → bvint size → bool.
+axiom lt: ∀size: intsize. bvint size → bvint size → bool.
+axiom ltu: ∀size: intsize. bvint size → bvint size → bool.
+axiom le: ∀size: intsize. bvint size → bvint size → bool.
+axiom leu: ∀size: intsize. bvint size → bvint size → bool.
+axiom gt: ∀size: intsize. bvint size → bvint size → bool.
+axiom gtu: ∀size: intsize. bvint size → bvint size → bool.
+axiom ge: ∀size: intsize. bvint size → bvint size → bool.
+axiom geu: ∀size: intsize. bvint size → bvint size → bool.
+axiom neg: ∀size: intsize. bvint size → bvint size.
+axiom lognot: ∀size: intsize. bvint size → bvint size.
+axiom logand: ∀size: intsize. bvint size → bvint size → bvint size.
+axiom logor: ∀size: intsize. bvint size → bvint size → bvint size.
+axiom logxor: ∀size: intsize. bvint size → bvint size → bvint size.
+axiom shl: ∀size: intsize. bvint size → bvint size → bvint size.
+axiom shr: ∀size: intsize. bvint size → bvint size → bvint size.
+axiom shrl: ∀size: intsize. bvint size → bvint size → bvint size.
+axiom max: ∀size: intsize. bvint size → bvint size → bvint size.
+axiom maxu: ∀size: intsize. bvint size → bvint size → bvint size.
+axiom min: ∀size: intsize. bvint size → bvint size → bvint size.
+axiom minu: ∀size: intsize. bvint size → bvint size → bvint size.
+axiom cast: ∀size: intsize. bvint_int_repr → bvint size.
+axiom to_int: ∀size: intsize. bvint size → nat. (*dpm: """" *)
+axiom zero_ext: ∀size: intsize. nat → bvint size → bvint size. (* nat here correct *)
+axiom sign_ext: ∀size: intsize. nat → bvint size → bvint size. (* nat here correct *)
+axiom break: ∀size: intsize. bvint size → nat → list (bvint size).
+axiom merge: ∀size: intsize. list (bvint size) → bvint size.