Skeleton of Asmblock

1 files changed, 136 insertions, 82 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 89df1d31..71c0dba3 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -37,6 +37,7 @@ Require Import AST Integers Floats.
 Require Import Values Memory Events Globalenvs Smallstep.
 Require Import Locations Conventions.
 Require Stacklayout.
+Require Import OptionMonad.
 
 (** * Abstract syntax *)
 
@@ -323,7 +324,7 @@ Record function : Type := mkfunction { fn_sig: signature; fn_blocks: bblocks }.
 Definition fundef := AST.fundef function.
 Definition program := AST.program fundef unit.
 
-(* TODO: ORIGINAL INSTRUCTIONS THAT NEEDS TO BE ADAPTED !
+(* TODO: ORIGINAL ABSTRACT SYNTAX OF INSTRUCTIONS THAT NEEDS TO BE ADAPTED !
 
 Inductive instruction: Type :=
   (** Branches *)
@@ -573,7 +574,7 @@ Record state: Type := State { _rs: regset; _m: mem }.
 Definition outcome := option state.
 Definition Next rs m: outcome := Some (State rs m).
 Definition Stuck: outcome := None.
-
+Local Open Scope option_monad_scope.
 
 (* a few lemma on comparisons of unsigned (e.g. pointers) 
 
@@ -780,18 +781,14 @@ Definition eval_addressing (a: addressing) (rs: regset): val :=
 
 Definition exec_load (chunk: memory_chunk) (transf: val -> val)
                      (a: addressing) (r: preg) (rs: regset) (m: mem) :=
-  match Mem.loadv chunk m (eval_addressing a rs) with
-  | None => Stuck
-  | Some v => Next (rs#r <- (transf v)) m
-  end.
+  SOME v <- Mem.loadv chunk m (eval_addressing a rs) IN
+  Next (rs#r <- (transf v)) m.
 
 Definition exec_store (chunk: memory_chunk)
                       (a: addressing) (v: val)
                       (rs: regset) (m: mem) :=
-  match Mem.storev chunk m (eval_addressing a rs) v with
-  | None => Stuck
-  | Some m' => Next rs m'
-  end.
+  SOME m' <- Mem.storev chunk m (eval_addressing a rs) v IN
+  Next rs m'.
 
 (** Insertion of bits into an integer *)
 
@@ -882,28 +879,23 @@ Definition interp_load_rd_a (ld: load_rd_a): val -> val :=
   | _ => fun v => v
   end.
 
+
+(* basic exec *)
 Definition exec_basic (b: basic) (rs: regset) (m: mem): outcome :=
   match b with
   | PLoad ld rd a => exec_load (chunk_load_rd_a ld) (interp_load_rd_a ld) a rd rs m
   | Pallocframe sz pos =>
       let (m1, stk) := Mem.alloc m 0 sz in
       let sp := (Vptr stk Ptrofs.zero) in
-      match Mem.storev Mint64 m1 (Val.offset_ptr sp pos) rs#SP with
-      | None => Stuck
-      | Some m2 => Next (rs #X29 <- (rs#SP) #SP <- sp #X16 <- Vundef) m2
-      end
+      SOME m2 <- Mem.storev Mint64 m1 (Val.offset_ptr sp pos) rs#SP IN
+      Next (rs #X29 <- (rs#SP) #SP <- sp #X16 <- Vundef) m2
   | Pfreeframe sz pos =>
-      match Mem.loadv Mint64 m (Val.offset_ptr rs#SP pos) with
-      | None => Stuck
-      | Some v =>
-          match rs#SP with
-          | Vptr stk ofs =>
-              match Mem.free m stk 0 sz with
-              | None => Stuck
-              | Some m' => Next (rs#SP <- v #X16 <- Vundef) m'
-              end
-          | _ => Stuck
-          end
+      SOME v <- Mem.loadv Mint64 m (Val.offset_ptr rs#SP pos) IN
+      match rs#SP with
+      | Vptr stk ofs =>
+        SOME m' <- Mem.free m stk 0 sz IN
+        Next (rs#SP <- v #X16 <- Vundef) m'
+      | _ => Stuck
       end
   | Ploadsymbol rd id =>
       Next (rs#rd <- (Genv.symbol_address ge id Ptrofs.zero)) m
@@ -916,56 +908,93 @@ Definition exec_basic (b: basic) (rs: regset) (m: mem): outcome :=
   end
 .
 
+(** TODO: redundant w.r.t Machblock ?? *)
+Lemma in_dec (lbl: label) (l: list label):  { List.In lbl l } + { ~(List.In lbl l) }.
+Proof.
+  apply List.in_dec.
+  apply Pos.eq_dec.
+Qed.
+
+(** Note: copy-paste from Machblock *)
+Definition is_label (lbl: label) (bb: bblock) : bool :=
+  if in_dec lbl (header bb) then true else false.
 
-(* TODO: ORIGINAL PART THAT NEEDS TO BE ADAPTED !
+Lemma is_label_correct_true lbl bb:
+  List.In lbl (header bb) <-> is_label lbl bb = true. 
+Proof.
+  unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition.
+Qed.
 
-(** Looking up instructions in a code sequence by position. *)
+Lemma is_label_correct_false lbl bb:
+  ~(List.In lbl (header bb)) <-> is_label lbl bb = false. 
+Proof.
+  unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition.
+Qed.
 
-Fixpoint find_instr (pos: Z) (c: code) {struct c} : option instruction :=
-  match c with
+(** convert a label into a position in the code *)
+Fixpoint label_pos (lbl: label) (pos: Z) (lb: bblocks) {struct lb} : option Z :=
+  match lb with
   | nil => None
-  | i :: il => if zeq pos 0 then Some i else find_instr (pos - 1) il
+  | b :: lb' => if is_label lbl b then Some pos else label_pos lbl (pos + (size b)) lb'
   end.
 
-(** Position corresponding to a label *)
-
-Definition is_label (lbl: label) (instr: instruction) : bool :=
-  match instr with
-  | Plabel lbl' => if peq lbl lbl' then true else false
-  | _ => false
+Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) :=
+  SOME pos <- label_pos lbl 0 (fn_blocks f) IN
+  match rs#PC with
+  | Vptr b ofs => Next (rs#PC <- (Vptr b (Ptrofs.repr pos))) m
+  | _ => Stuck
   end.
 
-Lemma is_label_correct:
-  forall lbl instr,
-  if is_label lbl instr then instr = Plabel lbl else instr <> Plabel lbl.
-Proof.
-  intros.  destruct instr; simpl; try discriminate. destruct (peq lbl lbl0); congruence.
-Qed.
+(** Evaluating a branch 
 
-Fixpoint label_pos (lbl: label) (pos: Z) (c: code) {struct c} : option Z :=
-  match c with
-  | nil => None
-  | instr :: c' =>
-      if is_label lbl instr then Some (pos + 1) else label_pos lbl (pos + 1) c'
-  end.
+Warning: PC is assumed to be already pointing on the next instruction !
 
+*)
 
-(** Manipulations over the [PC] register: continuing with the next
-  instruction ([nextinstr]) or branching to a label ([goto_label]). *)
+Definition eval_branch (f: function) (lbl: label) (rs: regset) (m: mem) (ores: option bool) :=
+  SOME res <- ores IN
+  if res then goto_label f lbl rs m else Next rs m.
 
-Definition nextinstr (rs: regset) :=
-  rs#PC <- (Val.offset_ptr rs#PC Ptrofs.one).
+Definition eval_neg_branch (f: function) (lbl: label) (rs: regset) (m: mem) (ores: option bool) :=
+  SOME res <- ores IN
+  if res then Next rs m else goto_label f lbl rs m.
 
-Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) :=
-  match label_pos lbl 0 (fn_code f) with
-  | None => Stuck
-  | Some pos =>
-      match rs#PC with
-      | Vptr b ofs => Next (rs#PC <- (Vptr b (Ptrofs.repr pos))) m
+Definition exec_cfi (f: function) (cfi: cf_instruction) (rs: regset) (m: mem) : outcome :=
+  match cfi with
+  (** Branches *)
+  | Pb lbl =>
+      goto_label f lbl rs m
+  | Pbc cond lbl =>
+      eval_branch f lbl rs m (eval_testcond cond rs)
+  | Pbl id sg =>
+      Next (rs#RA <- (rs#PC) #PC <- (Genv.symbol_address ge id Ptrofs.zero)) m
+  | Pbs id sg =>
+      Next (rs#PC <- (Genv.symbol_address ge id Ptrofs.zero)) m
+  | Pblr r sg =>
+      Next (rs#RA <- (rs#PC) #PC <- (rs#r)) m
+  | Pbr r sg =>
+      Next (rs#PC <- (rs#r)) m
+  | Pret r =>
+      Next (rs#PC <- (rs#r)) m
+  | Pcbnz sz r lbl =>
+      eval_neg_branch f lbl rs m (eval_testzero sz rs#r)
+  | Pcbz sz r lbl =>
+      eval_branch f lbl rs m (eval_testzero sz rs#r)
+  | Ptbnz sz r n lbl =>
+      eval_branch f lbl rs m (eval_testbit sz rs#r n)
+  | Ptbz sz r n lbl =>
+      eval_neg_branch f lbl rs m (eval_testbit sz rs#r n)
+  (** Pseudo-instructions *)
+  | Pbtbl r tbl =>
+      match (rs#X16 <- Vundef)#r with
+      | Vint n =>
+          SOME lbl <- list_nth_z tbl (Int.unsigned n) IN
+          goto_label f lbl (rs#X16 <- Vundef #X17 <- Vundef) m
       | _ => Stuck
-    end
+      end
   end.
 
+(* TODO: ORIGINAL EXECUTION OF INSTRUCTIONS THAT NEEDS TO BE ADAPTED !
 
 (** Execution of a single instruction [i] in initial state
     [rs] and [m].  Return updated state.  For instructions
@@ -1415,6 +1444,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pcfi_rel_offset _ =>
       Stuck
   end.
+*)
 
 (** Translation of the LTL/Linear/Mach view of machine registers
   to the AArch64 view.  Note that no LTL register maps to [X16],
@@ -1482,44 +1512,70 @@ Definition extcall_arguments
 Definition loc_external_result (sg: signature) : rpair preg :=
   map_rpair preg_of (loc_result sg).
 
-(** Execution of the instruction at [rs#PC]. *)
 
-Inductive state: Type :=
-  | State: regset -> mem -> state.
+(**  execution of the body of a bblock *)
+Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome :=
+  match body with
+  | nil => Next rs m
+  | bi::body' => 
+     SOME o <- exec_basic bi rs m IN
+     exec_body body' (_rs o) (_m o)
+  end.
+
+Definition incrPC size_b (rs: regset) :=
+  rs#PC <- (Val.offset_ptr rs#PC size_b).
+
+(**  execution of the exit instruction of a bblock *)
+Inductive exec_exit (f: function) size_b (rs: regset) (m: mem): (option control) -> trace -> regset -> mem -> Prop :=
+  | none_step:
+      exec_exit f size_b rs m None E0 (incrPC size_b rs) m
+  | cfi_step (cfi: cf_instruction) rs' m':
+      exec_cfi f cfi (incrPC size_b rs) m = Next rs' m' ->
+      exec_exit f size_b rs m (Some (PCtlFlow cfi)) E0 rs' m'
+  | builtin_step ef args res vargs t vres rs' m':
+      eval_builtin_args ge rs rs#SP m args vargs ->
+      external_call ef ge vargs m t vres m' ->
+      rs' = incrPC size_b
+              (set_res res vres
+                (undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) ->
+      exec_exit f size_b rs m (Some (Pbuiltin ef args res)) t rs' m'
+      .
+
+Definition exec_bblock (f: function) (b: bblock) (rs: regset) (m: mem) (t:trace) (rs':regset) (m':mem): Prop
+  := exists rs1 m1, exec_body (body b) rs m = Next rs1 m1 /\  exec_exit f (Ptrofs.repr (size b)) rs1 m1 (exit b) t rs' m'.
+
+Fixpoint find_bblock (pos: Z) (lb: bblocks) {struct lb} : option bblock :=
+  match lb with
+  | nil => None
+  | b :: il => 
+    if zlt pos 0 then None  (* NOTE: It is impossible to branch inside a block *)
+    else if zeq pos 0 then Some b
+    else find_bblock (pos - (size b)) il
+  end.
+
+(** Execution of the instruction at [rs PC]. *)
 
 Inductive step: state -> trace -> state -> Prop :=
   | exec_step_internal:
-      forall b ofs f i rs m rs' m',
+      forall b ofs f bi rs m t rs' m',
       rs PC = Vptr b ofs ->
       Genv.find_funct_ptr ge b = Some (Internal f) ->
-      find_instr (Ptrofs.unsigned ofs) f.(fn_code) = Some i ->
-      exec_instr f i rs m = Next rs' m' ->
+      find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bi ->
+      exec_bblock f bi rs m t rs' m' ->
       step (State rs m) E0 (State rs' m')
-  | exec_step_builtin:
-      forall b ofs f ef args res rs m vargs t vres rs' m',
-      rs PC = Vptr b ofs ->
-      Genv.find_funct_ptr ge b = Some (Internal f) ->
-      find_instr (Ptrofs.unsigned ofs) f.(fn_code) = Some (Pbuiltin ef args res) ->
-      eval_builtin_args ge rs rs#SP m args vargs ->
-      external_call ef ge vargs m t vres m' ->
-      rs' = nextinstr
-              (set_res res vres
-                (undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) ->
-      step (State rs m) t (State rs' m')
   | exec_step_external:
       forall b ef args res rs m t rs' m',
       rs PC = Vptr b Ptrofs.zero ->
       Genv.find_funct_ptr ge b = Some (External ef) ->
       external_call ef ge args m t res m' ->
       extcall_arguments rs m (ef_sig ef) args ->
-      rs' = (set_pair (loc_external_result (ef_sig ef)) res (undef_caller_save_regs rs)) #PC <- (rs RA) ->
-      step (State rs m) t (State rs' m').
+      rs' = (set_pair (loc_external_result (ef_sig ef) ) res (undef_caller_save_regs rs))#PC <- (rs RA) ->
+      step (State rs m) t (State rs' m')
+  .
 
-*)
 
 End RELSEM.
 
-(* TODO: ORIGINAL PART THAT NEEDS TO BE ADAPTED !
 
 (** Execution of whole programs. *)
 
@@ -1542,5 +1598,3 @@ Inductive final_state: state -> int -> Prop :=
 
 Definition semantics (p: program) :=
   Semantics step (initial_state p) final_state (Genv.globalenv p).
-
-*)
\ No newline at end of file