From 91a07b5ef9935780942a53108ac80ef354a76248 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Sat, 19 Dec 2020 18:40:04 +0100
Subject: Cleanup

---
 aarch64/Asmblockgen.v | 46 ----------------------------------------------
 1 file changed, 46 deletions(-)

(limited to 'aarch64/Asmblockgen.v')

diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v
index 325f238c..b55a1195 100644
--- a/aarch64/Asmblockgen.v
+++ b/aarch64/Asmblockgen.v
@@ -389,9 +389,6 @@ Definition arith_extended
 Definition shrx32 (rd r1: ireg) (n: int) (k: bcode) : bcode :=
   if Int.eq n Int.zero then
     Pmov rd r1 ::bi k
-(*   else if Int.eq n Int.one then
-    Padd W (SOlsr (Int.repr 31)) X16 r1 r1 ::bi
-    Porr W (SOasr n) rd XZR X16 ::bi k *)
   else
     Porr W (SOasr (Int.repr 31)) X16 XZR r1 ::bi
     Padd W (SOlsr (Int.sub Int.iwordsize n)) X16 r1 X16 ::bi
@@ -400,9 +397,6 @@ Definition shrx32 (rd r1: ireg) (n: int) (k: bcode) : bcode :=
 Definition shrx64 (rd r1: ireg) (n: int) (k: bcode) : bcode :=
   if Int.eq n Int.zero then
     Pmov rd r1 ::bi k
-(*   else if Int.eq n Int.one then
-    Padd X (SOlsr (Int.repr 63)) X16 r1 r1 ::bi
-    Porr X (SOasr n) rd XZR X16 ::bi k *)
   else
     Porr X (SOasr (Int.repr 63)) X16 XZR r1 ::bi
     Padd X (SOlsr (Int.sub Int64.iwordsize' n)) X16 r1 X16 ::bi
@@ -1170,34 +1164,6 @@ Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_ins
       transl_instr_basic f i1 it1p k1
   end.
 
-(** Translation of a whole function.  Note that we must check
-  that the generated code contains less than [2^64] instructions,
-  otherwise the offset part of the [PC] code pointer could wrap
-  around, leading to incorrect executions. *)
-
-(* NB Sylvain: this issue with PExpand seems specific to kvx -- and not necessary here *)
-(* gen_bblocks can generate two bblocks if the ctl is a PExpand (since the PExpand must be alone in its block) *)
-(*
-Program Definition gen_bblocks (hd: list label) (c: bcode) (ctl: list instruction) :=
-  match (extract_ctl ctl) with
-  | None => 
-      (* XXX Que faire du Pnop ? *)
-      match c with
-      | nil => {| header := hd; body := Pnop::nil; exit := None |} :: nil
-      | i :: c => {| header := hd; body := ((i :: c) ++ extract_basic ctl); exit := None |} :: nil
-      end
-  (*| Some (i) =>*)
-      (*match c with*)
-      (*| nil => {| header := hd; body := nil; exit := Some (PExpand (Pbuiltin ef args res)) |} :: nil*)
-      (*| _ => {| header := hd; body := c; exit := None |} *)
-              (*:: {| header := nil; body := nil; exit := Some (PExpand (Pbuiltin ef args res)) |} :: nil*)
-      (*end*)
-  | Some ex => {| header := hd; body := (c ++ extract_basic ctl); exit := Some ex |} :: nil
-  end
-.
-*)
-
-(* XXX: the simulation proof may be complex with this pattern. We may fix this later *)
 Program Definition cons_bblocks (ll: list label) (bdy: list basic) (ex: option control): bblocks :=
   match ex with
   | None =>
@@ -1262,23 +1228,11 @@ Fixpoint transl_blocks (f: Machblock.function) (lmb: list Machblock.bblock) (ep:
   end
 .
 
-(*   match lmb with
-  | nil => OK nil
-  | mb :: lmb => 
-      do lb <- transl_blocks f lmb false;
-      transl_block f mb (if Machblock.header mb then ep else false) lb
-  end. *)
-  (* OK (make_epilogue f ((Pret X0)::c nil))*)
-
 Program Definition make_prologue (f:  Machblock.function) (k:bblocks) :=
   {| header := nil; body := Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::bi
-(*       storeptr_bc RA XSP f.(fn_retaddr_ofs) nil; *)
       ((PSt_rs_a Pstrx RA) (ADimm XSP (Ptrofs.to_int64 (f.(fn_retaddr_ofs))))) ::bi nil;
       exit := None |} :: k.
   
-(*    Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::b
-   push_bc (storeptr_bc RA XSP f.(fn_retaddr_ofs) (pop_bc k)) k. *)
-
 Definition transl_function (f: Machblock.function) : res Asmblock.function :=
   do lb <- transl_blocks f f.(Machblock.fn_code) true;
   OK (mkfunction f.(Machblock.fn_sig)
-- 
cgit