Register-File Model
The MIPS-3k architecture features 32, 32-bit (word-sized) registers. We use the inductive type
reg_t to enumerate the identifiers (constructors of
reg_t).
type reg_t =
Zero | At | V0 | V1 | A0 | A1 | A2 | A3
| T0 | T1 | T2 | T3 | T4 | T5 | T6 | T7
| S0 | S1 | S2 | S3 | S4 | S5 | S6 | S7
| T8 | T9 | K0 | K1 | Gp | Sp | Fp | Ra
For simplicity, at this point, we model the data content by the
int type which is unbound (infinite) in the
whyML language. We store the the content in a
map reg_t int, i.e., relating (mapping) each register to an integer value.
In order to allow the register content to be mutated (updated), we define the global variable
r.
(* maps reg_t -> v : int *)
type reg_file_t = map reg_t int
(* mutable map *)
val r : ref reg_file_t
We define a set of predicates capturing the semantics of the register file. Predicates are here context free, so they take a register file
r as an argument.
In a real MIPS you may write to register Zero, however without any effect. In our model we chose to disallow writes to
Zero instead, just for simplicity.
(* register Zero = 0 *)
predicate reg_zero (r : reg_file_t) =
r[Zero] = 0
reg_content r rn v asserts that the content or register
rn is
v.
(* content of register rn = v *)
predicate reg_content (r : reg_file_t) (rn : reg_t) (v : int) =
r[rn] = v
reg_eg_preservation r r_old rn v, checks both content
reg_content r rn v and that all
other registers remain their old values.
(* content & preservation besides rn *)
predicate reg_preservation (r r_old : reg_file_t) (rn : reg_t) (v : int) =
reg_content r rn v /\
forall rn':reg_t. rn' <> rn ->
r[rn'] = r_old[rn']
We can now formulate the
read with both contract and implementation.
(* read register rn *)
let read (rn : reg_t) : int
ensures { reg_content !r rn result }
=
!r[rn]
The
write is guarded
not to write to register
Zero (
requires { rn <> Zero }). In the contract
!r refers to the state of
r after the execution of
write, while
!(old r) refers to the state
before the execution. Hence we can assert the preservation criterion (which will be needed later for verification).
(* write register rn with value v *)
let write (rn : reg_t) (v : int)
requires { rn <> Zero }
ensures { reg_preservation !r !(old r) rn v }
=
r := !r[rn <- v]
end
We can now test (assert) the behaviour of the register file model.
module RegTest
use import RegFile
(* test raw access *)
let test_raw ()
=
r := !r[T0 <- 7]; (* raw write *)
assert { !r[T0] = 7 } (* raw read *)
(* test contract, write and read *)
let test_write ()
requires { reg_zero !r } (* !r[Zero] = 0 *)
requires { !r[T0] = 1 }
requires { !r[T1] = 2 }
=
assert { !r[T0] = 1 }; (* by contract *)
assert { !r[T1] = 2 }; (* by contract *)
write T1 3;
assert { !r[T0] = 1 }; (* preservation *)
assert { !r[T1] = 3 }; (* 1) new content *)
let r = read T1 in
assert { r = 3 }; (* 2) same as 1) *)
write Zero 3; (* precondition fails *)
end
Assignment 1)
Give an implementation that adds the content fulfils the contract, i.e., computes
A0 + A1 + A2 + A3 and stores the result in
V0. (At this point you may of course cheat, by just assigning
V0, right.)
let sum1_A0_A1_A2_A3 ()
requires { reg_zero !r } (* !r[Zero] = 0 *)
requires { !r[A0] = 1 }
requires { !r[A1] = 2 }
requires { !r[A2] = 3 }
requires { !r[A3] = 4 }
ensures { !r[V0] = 10 }
=
(* your code here *)
Assignment 2) Here the contract is stronger (i.e., the precondition is weaker) and the cheating is over!
Give an implementation that fulfils the the contract. (If you did not cheat in Assignment 1), the implementation will be the same.
let sum2_A0_A1_A2_A3 ()
requires { reg_zero !r } (* !r[Zero] = 0 *)
ensures {
let v = !(old r)[A0] + !(old r)[A1] + !(old r)[A2] + !(old r)[A3] in
reg_preservation !r !(old r) V0 v
}
=
(* your code here *)
Assignment 3) Optional (well everything is optional, but this is extra optional).
Formulate a lemma (and prove) that
sum A0 A1 0 0 + sum 0 0 A2 A3 = sum A0 A1 A2 A3
To this end, you may formulate the lemma on the (logic) function:
function sum_a0_a1_a2_a3 (a0 a1 a2 a3 : int) : int =
a0 + a1 + a2 + a3
Assignment 4) Extra super optional.
Show for the same thing for
sum_A0_A1_A2_A3.
Seemingly simple a lemma approach turn out difficult (since we are dealing with stateful representations, i.e., the register file), but there is a way around it... When
why3 checks a function, (e.g.
let x (i j : int) = ....) it quantifies over all
i,
j. You may use this approach to quantify over the unknown register content, and then just prove that a program that computes
sum A0 A1 0 0 +
sum 0 0 A2 A3 renders
sum A0 A1 A2 A3.
(It is essentially more difficult to prove properties of imperative programs, this is just one example...)
/Per Lindgren, September 2015