fix the semantics ?

2 files changed, 11 insertions, 3 deletions

diff --git a/aarch64/Asm.v b/aarch64/Asm.v
index 5dafb01f..618341a3 100644
--- a/aarch64/Asm.v
+++ b/aarch64/Asm.v
@@ -1093,9 +1093,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pfmov rd r1 =>
       Next (nextinstr (rs#rd <- (rs#r1))) m
   | Pfmovimms rd f =>
-      Next (nextinstr (rs#rd <- (Vsingle f))) m
+      Next (nextinstr ((rs#rd <- (Vsingle f))#X16 <- Vundef)) m
   | Pfmovimmd rd f =>
-      Next (nextinstr (rs#rd <- (Vfloat f))) m
+      Next (nextinstr ((rs#rd <- (Vfloat f))#X16 <- Vundef)) m
   | Pfmovi S rd r1 =>
       Next (nextinstr (rs#rd <- (float32_of_bits rs##r1))) m
   | Pfmovi D rd r1 =>
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 5da7e20a..3973abc0 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -754,6 +754,12 @@ Definition arith_eval_p (i : arith_p) : val :=
   | Pfmovimmd f => Vfloat f
   end.
 
+Definition destroy_X16 (i : arith_p) : bool :=
+  match i with
+  | Pfmovimms _ | Pfmovimmd _ => true (* TODO: we may refine this condition, according to the value of the immediate like in TargetPrinter *)
+  | _ => false
+  end.
+
 Definition if_opt_bool_val (c: option bool) v1 v2: val :=
    match c with
    | Some true => v1
@@ -948,7 +954,9 @@ Definition arith_comparison_p_compare i :=
 
 Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   match ai with
-  | PArithP i d => rs#d <- (arith_eval_p i)
+  | PArithP i d =>
+     let rs' := rs#d <- (arith_eval_p i) in
+     if destroy_X16 i then rs'#X16 <- Vundef else rs'
   | PArithPP i d s => rs#d <- (arith_eval_pp i rs#s)
   | PArithPPP i d s1 s2 => rs#d <- (arith_eval_ppp i rs#s1 rs#s2)