aboutsummaryrefslogtreecommitdiffstats
path: root/kvx
diff options
context:
space:
mode:
Diffstat (limited to 'kvx')
-rw-r--r--kvx/Asmblockdeps.v10
-rw-r--r--kvx/Asmblockgenproof1.v8
-rw-r--r--kvx/Asmblockprops.v4
-rw-r--r--kvx/Asmvliw.v18
-rw-r--r--kvx/Machregsaux.ml2
-rw-r--r--kvx/Machregsaux.mli3
-rw-r--r--kvx/PostpassSchedulingOracle.ml10
7 files changed, 35 insertions, 20 deletions
diff --git a/kvx/Asmblockdeps.v b/kvx/Asmblockdeps.v
index b6d18c3e..a9786e0a 100644
--- a/kvx/Asmblockdeps.v
+++ b/kvx/Asmblockdeps.v
@@ -164,17 +164,17 @@ Definition arith_eval (ao: arith_op) (l: list value) :=
| _, _ => None
end.
-Definition exec_incorrect_load trap chunk :=
+Definition exec_incorrect_load trap :=
match trap with
| TRAP => None
- | NOTRAP => Some (Val (concrete_default_notrap_load_value chunk))
+ | NOTRAP => Some (Val Vundef)
end.
Definition exec_load_deps_offset (trap: trapping_mode) (chunk: memory_chunk) (m: mem) (v: val) (ofs: offset) :=
let (ge, fn) := Ge in
match (eval_offset ofs) with
| OK ptr => match Mem.loadv chunk m (Val.offset_ptr v ptr) with
- | None => exec_incorrect_load trap chunk
+ | None => exec_incorrect_load trap
| Some vl => Some (Val vl)
end
| _ => None
@@ -182,13 +182,13 @@ Definition exec_load_deps_offset (trap: trapping_mode) (chunk: memory_chunk) (m:
Definition exec_load_deps_reg (trap: trapping_mode) (chunk: memory_chunk) (m: mem) (v vo: val) :=
match Mem.loadv chunk m (Val.addl v vo) with
- | None => exec_incorrect_load trap chunk
+ | None => exec_incorrect_load trap
| Some vl => Some (Val vl)
end.
Definition exec_load_deps_regxs (trap: trapping_mode) (chunk: memory_chunk) (m: mem) (v vo: val) :=
match Mem.loadv chunk m (Val.addl v (Val.shll vo (scale_of_chunk chunk))) with
- | None => exec_incorrect_load trap chunk
+ | None => exec_incorrect_load trap
| Some vl => Some (Val vl)
end.
diff --git a/kvx/Asmblockgenproof1.v b/kvx/Asmblockgenproof1.v
index a65bd5bc..259c4f9c 100644
--- a/kvx/Asmblockgenproof1.v
+++ b/kvx/Asmblockgenproof1.v
@@ -1914,7 +1914,7 @@ Lemma transl_load_access2_correct_notrap2:
Mem.loadv chunk m v = None ->
exists rs',
exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
- /\ rs'#rd = concrete_default_notrap_load_value chunk
+ /\ rs'#rd = Vundef
/\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r.
Proof.
intros until ro; intros ARGS IREGE INSTR TR EV LOAD.
@@ -1963,7 +1963,7 @@ Lemma transl_load_access2XS_correct_notrap2:
Mem.loadv chunk m v = None ->
exists rs',
exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
- /\ rs'#rd = concrete_default_notrap_load_value chunk
+ /\ rs'#rd = Vundef
/\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r.
Proof.
intros until ro; intros ARGS IREGE INSTR TR EV LOAD.
@@ -2008,7 +2008,7 @@ Lemma transl_load_access_correct_notrap2:
Mem.loadv chunk m v = None ->
exists rs',
exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
- /\ rs'#rd = concrete_default_notrap_load_value chunk
+ /\ rs'#rd = Vundef
/\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r.
Proof.
intros until v; intros INSTR TR EV LOAD.
@@ -2185,7 +2185,7 @@ Lemma transl_load_correct_notrap2:
Mem.loadv chunk m a = None ->
exists rs',
exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
- /\ rs'#(preg_of dst) = (concrete_default_notrap_load_value chunk)
+ /\ rs'#(preg_of dst) = Vundef
/\ forall r, r <> PC -> r <> RTMP -> r <> preg_of dst -> rs'#r = rs#r.
Proof.
intros until a; intros TR EV LOAD. destruct addr.
diff --git a/kvx/Asmblockprops.v b/kvx/Asmblockprops.v
index c3929be5..a732d29b 100644
--- a/kvx/Asmblockprops.v
+++ b/kvx/Asmblockprops.v
@@ -96,9 +96,9 @@ Theorem exec_basic_instr_pc:
Proof.
intros. destruct b; try destruct i; try destruct i.
all: try (inv H; Simpl).
- 1-10: unfold parexec_load_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail.
+ 1-10: unfold parexec_load_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; inv H1; Simpl; fail.
- 1-20: unfold parexec_load_reg, parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail.
+ 1-20: unfold parexec_load_reg, parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; inv H1; Simpl; fail.
{ (* PLoadQRRO *)
unfold parexec_load_q_offset in H1.
diff --git a/kvx/Asmvliw.v b/kvx/Asmvliw.v
index aa2e0885..45b230e6 100644
--- a/kvx/Asmvliw.v
+++ b/kvx/Asmvliw.v
@@ -313,7 +313,11 @@ Inductive cf_instruction : Type :=
.
(** *** Loads *)
-Definition concrete_default_notrap_load_value (chunk : memory_chunk) :=
+
+(* What follows was the original spec, but is subtly incorrect.
+ Our definition of the assembly-level memory model is already an abstraction of the real world.
+ In particular, we consider that a load is incorrect when it points outside of CompCert's visible memory, whereas this memory could be correct at the assembly level.
+ This means that CompCert would believe an incorrect load would yield 0 whereas it would yield another value.
match chunk with
| Mint8signed | Mint8unsigned | Mint16signed | Mint16unsigned
| Mint32 => Vint Int.zero
@@ -321,7 +325,7 @@ Definition concrete_default_notrap_load_value (chunk : memory_chunk) :=
| Many32 | Many64 => Vundef
| Mfloat32 => Vsingle Float32.zero
| Mfloat64 => Vfloat Float.zero
- end.
+ end. *)
Inductive load_name : Type :=
| Plb (**r load byte *)
@@ -1169,16 +1173,16 @@ Definition eval_offset (ofs: offset) : res ptrofs := OK ofs.
(** *** load/store instructions *)
-Definition parexec_incorrect_load trap chunk d rsw mw :=
+Definition parexec_incorrect_load trap d rsw mw :=
match trap with
| TRAP => Stuck
- | NOTRAP => Next (rsw#d <- (concrete_default_notrap_load_value chunk)) mw
+ | NOTRAP => Next (rsw#d <- Vundef) mw
end.
Definition parexec_load_offset (trap: trapping_mode) (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a: ireg) (ofs: offset) :=
match (eval_offset ofs) with
| OK ptr => match Mem.loadv chunk mr (Val.offset_ptr (rsr a) ptr) with
- | None => parexec_incorrect_load trap chunk d rsw mw
+ | None => parexec_incorrect_load trap d rsw mw
| Some v => Next (rsw#d <- v) mw
end
| _ => Stuck
@@ -1225,13 +1229,13 @@ Definition parexec_load_o_offset (rsr rsw: regset) (mr mw: mem) (d : gpreg_o) (a
Definition parexec_load_reg (trap: trapping_mode) (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a ro: ireg) :=
match Mem.loadv chunk mr (Val.addl (rsr a) (rsr ro)) with
- | None => parexec_incorrect_load trap chunk d rsw mw
+ | None => parexec_incorrect_load trap d rsw mw
| Some v => Next (rsw#d <- v) mw
end.
Definition parexec_load_regxs (trap: trapping_mode) (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a ro: ireg) :=
match Mem.loadv chunk mr (Val.addl (rsr a) (Val.shll (rsr ro) (scale_of_chunk chunk))) with
- | None => parexec_incorrect_load trap chunk d rsw mw
+ | None => parexec_incorrect_load trap d rsw mw
| Some v => Next (rsw#d <- v) mw
end.
diff --git a/kvx/Machregsaux.ml b/kvx/Machregsaux.ml
index e3b18181..dbb89727 100644
--- a/kvx/Machregsaux.ml
+++ b/kvx/Machregsaux.ml
@@ -31,3 +31,5 @@ let class_of_type = function
| AST.Tint | AST.Tlong
| AST.Tfloat | AST.Tsingle -> 0
| AST.Tany32 | AST.Tany64 -> assert false
+
+let nr_regs = [| 59 |]
diff --git a/kvx/Machregsaux.mli b/kvx/Machregsaux.mli
index 01b0f9fd..23ac1c9a 100644
--- a/kvx/Machregsaux.mli
+++ b/kvx/Machregsaux.mli
@@ -15,3 +15,6 @@
val is_scratch_register: string -> bool
val class_of_type: AST.typ -> int
+
+(* Number of registers in each class *)
+val nr_regs : int array
diff --git a/kvx/PostpassSchedulingOracle.ml b/kvx/PostpassSchedulingOracle.ml
index 2107ce22..5ebad421 100644
--- a/kvx/PostpassSchedulingOracle.ml
+++ b/kvx/PostpassSchedulingOracle.ml
@@ -787,8 +787,14 @@ let latency_constraints bb =
*)
let build_problem bb =
- { max_latency = -1; resource_bounds = resource_bounds;
- instruction_usages = instruction_usages bb; latency_constraints = latency_constraints bb }
+{ max_latency = -1;
+ resource_bounds = resource_bounds;
+ instruction_usages = instruction_usages bb;
+ latency_constraints = latency_constraints bb;
+ live_regs_entry = Registers.Regset.empty; (* unused here *)
+ typing = (fun x -> AST.Tint); (* unused here *)
+ reference_counting = None
+}
let rec find_min_opt (l: int option list) =
match l with
generated by cgit (git 2.34.1) at 2024-07-04 01:26:41 +0000