From 9c03320dd809295239a9cdf71cd8726f02df0d33 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 1 Feb 2021 20:37:49 +0100
Subject: int64_of_value

---
 riscV/ExtValues.v | 77 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 77 insertions(+)

(limited to 'riscV')

diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v
index 39070e7b..d79604f7 100644
--- a/riscV/ExtValues.v
+++ b/riscV/ExtValues.v
@@ -2,7 +2,84 @@ Require Import Coqlib.
 Require Import Integers.
 Require Import Values.
 Require Import Floats.
+Require Import Memory.
+Require Import Lia.
 
+Axiom address_of_ptr : mem -> block -> ptrofs -> int64.
+Axiom ptr_of_address : mem -> int64 -> option (block*ptrofs).
+Axiom ptr_address_correct :
+  forall m b ofs, (ptr_of_address m (address_of_ptr m b ofs)) = Some (b, ofs).
+
+Definition int64_of_value m v : int64 :=
+  match v with
+  | Vint x => Int64.repr (Int.signed x)
+  | Vlong x => x
+  | Vsingle x => Int64.repr (Int.signed (Float32.to_bits x))
+  | Vfloat x => Float.to_bits x
+  | Vptr b ofs => address_of_ptr m b ofs
+  | Vundef => Int64.zero
+  end.
+
+Inductive vtype := VTint | VTlong | VTsingle | VTfloat | VTptr | VTundef.
+
+Definition vtype_of v :=
+  match v with
+  | Vint _ => VTint
+  | Vlong _ => VTlong
+  | Vfloat _ => VTfloat
+  | Vsingle _ => VTsingle
+  | Vptr _ _ => VTptr
+  | Vundef => VTundef
+  end.
+
+Definition value_of_int64 (ty : vtype) (m : mem) (l : int64) : val :=
+  match ty with
+  | VTint => Vint (Int.repr (Int64.signed l))
+  | VTlong => Vlong l
+  | VTsingle => Vsingle (Float32.of_bits (Int.repr (Int64.signed l)))
+  | VTfloat => Vfloat (Float.of_bits l)
+  | VTptr => match ptr_of_address m l with
+                | Some(b, ofs) => Vptr b ofs
+                | None => Vundef
+             end
+  | VTundef => Vundef
+  end.
+
+Remark min_signed_order: Int64.min_signed <= Int.min_signed.
+Proof.
+  cbv. discriminate.
+Qed.
+
+Remark max_signed_order: Int.max_signed <= Int64.max_signed.
+Proof.
+  cbv. discriminate.
+Qed.
+
+Lemma int64_of_value_correct :
+  forall m v,
+    value_of_int64 (vtype_of v) m (int64_of_value m v) = v.
+Proof.
+  destruct v; cbn; trivial; f_equal.
+  - rewrite Int64.signed_repr.
+    apply Int.repr_signed. 
+    pose proof (Int.signed_range i) as RANGE.
+    pose proof min_signed_order.
+    pose proof max_signed_order.
+    lia.
+  - apply Float.of_to_bits.
+  - rewrite Int64.signed_repr.
+    { rewrite Int.repr_signed.
+      apply Float32.of_to_bits. }
+    pose proof (Int.signed_range (Float32.to_bits f)) as RANGE.
+    pose proof min_signed_order.
+    pose proof max_signed_order.
+    lia.
+  - pose proof (ptr_address_correct m b i).
+    destruct (ptr_of_address m (address_of_ptr m b i)).
+    + inv H. trivial.
+    + discriminate.
+Qed.
+    
 Definition bits_of_float x :=
   match x with
   | Vfloat f => Vlong (Float.to_bits f)
-- 
cgit