Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Update PowerPC modules #54

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Update PowerPC modules #54

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 4 additions & 12 deletions fstar/code/arch/ppc64le/PPC64LE.Vale.Decls.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,13 +45,9 @@ unfold let va_state = state
val va_fuel : Type0
unfold let reg_opr = reg
unfold let va_operand_reg_opr = reg
unfold let va_operand_dst_reg_opr = reg
unfold let dst_reg_opr = reg
unfold let va_operand_Mem64 = maddr
unfold let vec_opr = vec
unfold let dst_vec_opr = vec
unfold let va_operand_vec_opr = vec
unfold let va_operand_dst_vec_opr = vec

val va_pbool : Type0
val va_ttrue (_:unit) : va_pbool
Expand All @@ -68,11 +64,9 @@ val mul_nat_helper (x y:nat) : Lemma (x * y >= 0)
// Constructors
val va_fuel_default : unit -> va_fuel
[@va_qattr] unfold let va_op_reg_opr_reg (r:reg) : reg_opr = r
[@va_qattr] unfold let va_op_dst_reg_opr_reg (r:reg) : dst_reg_opr = r
[@va_qattr] unfold let va_op_cmp_reg (r:reg) : cmp_opr = CReg r
[@va_qattr] unfold let va_const_cmp (n:imm16) : cmp_opr = CImm n
[@va_qattr] unfold let va_op_vec_opr_vec (v:vec) : vec_opr = v
[@va_qattr] unfold let va_op_dst_vec_opr_vec (v:vec) : dst_vec_opr = v

[@va_qattr]
unfold let va_opr_code_Mem64 (r:reg) (n:int) : maddr =
Expand All @@ -82,18 +76,16 @@ unfold let va_opr_code_Mem64 (r:reg) (n:int) : maddr =
[@va_qattr] unfold let va_eval_reg (s:va_state) (r:reg) : GTot nat64 = eval_reg r s
[@va_qattr] unfold let va_eval_Mem64 (s:va_state) (m:maddr) : GTot nat64 = eval_mem64 (eval_maddr m s) s
[@va_qattr] unfold let va_eval_reg_opr (s:va_state) (r:reg_opr) : GTot nat64 = eval_reg r s
[@va_qattr] unfold let va_eval_dst_reg_opr (s:va_state) (r:dst_reg_opr) : GTot nat64 = eval_reg r s
[@va_qattr] unfold let va_eval_cmp_opr (s:va_state) (o:cmp_opr) : GTot nat64 = eval_cmp_opr o s
[@va_qattr] unfold let va_eval_vec_opr (s:va_state) (v:vec_opr) : GTot quad32 = eval_vec v s
[@va_qattr] unfold let va_eval_dst_vec_opr (s:va_state) (v:dst_vec_opr) : GTot quad32 = eval_vec v s

// Predicates
[@va_qattr] unfold let va_is_src_reg_opr (r:reg_opr) (s:va_state) = True
[@va_qattr] unfold let va_is_dst_dst_reg_opr (r:dst_reg_opr) (s:va_state) = True
[@va_qattr] unfold let va_is_dst_reg_opr (r:reg_opr) (s:va_state) = True
[@va_qattr] unfold let va_is_src_Mem64 (m:maddr) (s:va_state) = valid_maddr64 m s
[@va_qattr] unfold let va_is_dst_Mem64 (m:maddr) (s:va_state) = valid_maddr64 m s
[@va_qattr] unfold let va_is_src_vec_opr (v:vec_opr) (s:va_state) = True
[@va_qattr] unfold let va_is_dst_dst_vec_opr (v:dst_vec_opr) (s:va_state) = True
[@va_qattr] unfold let va_is_dst_vec_opr (v:vec_opr) (s:va_state) = True

// Getters
[@va_qattr] unfold let va_get_ok (s:va_state) : bool = s.ok
Expand Down Expand Up @@ -123,15 +115,15 @@ unfold let va_opr_code_Mem64 (r:reg) (n:int) : maddr =
va_upd_vec x (eval_vec x sM) sK

[@va_qattr] unfold
let va_update_operand_dst_reg_opr (r:reg) (sM:va_state) (sK:va_state) : va_state =
let va_update_operand_reg_opr (r:reg) (sM:va_state) (sK:va_state) : va_state =
va_update_reg r sM sK

[@va_qattr] unfold
let va_update_operand_Mem64 (m:maddr) (sM:va_state) (sK:va_state) : va_state =
va_update_maddr m sM sK

[@va_qattr] unfold
let va_update_operand_dst_vec_opr (x:vec) (sM:va_state) (sK:va_state) : va_state =
let va_update_operand_vec_opr (x:vec) (sM:va_state) (sK:va_state) : va_state =
va_update_vec x sM sK

// Constructors for va_codes
Expand Down
72 changes: 31 additions & 41 deletions fstar/code/arch/ppc64le/PPC64LE.Vale.InsBasic.vaf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,34 +58,24 @@ var cr0:cr0_t {:state cr0()};
var xer:xer_t {:state xer()};
var mem:memory {:state mem()};

// Input operands of general-purpose registers
// Operands of general-purpose registers
operand_type reg_opr:nat64 :=
| in r0 | in r1 | in r2 | in r3
| in r4 | in r5 | in r6 | in r7
| in r8 | in r9 | in r10 | in r11
| in r12 | in r13 | in r14 | in r15
| in r16 | in r17 | in r18 | in r19
| in r20 | in r21 | in r22 | in r23
| in r24 | in r25 | in r26 | in r27
| in r28 | in r29 | in r30 | in r31
;
// Output operands of general-purpose registers
operand_type dst_reg_opr:nat64 :=
| out r0 | out r1 | out r2 | out r3
| out r4 | out r5 | out r6 | out r7
| out r8 | out r9 | out r10 | out r11
| out r12 | out r13 | out r14 | out r15
| out r16 | out r17 | out r18 | out r19
| out r20 | out r21 | out r22 | out r23
| out r24 | out r25 | out r26 | out r27
| out r28 | out r29 | out r30 | out r31
| inout r0 | inout r1 | inout r2 | inout r3
| inout r4 | inout r5 | inout r6 | inout r7
| inout r8 | inout r9 | inout r10 | inout r11
| inout r12 | inout r13 | inout r14 | inout r15
| inout r16 | inout r17 | inout r18 | inout r19
| inout r20 | inout r21 | inout r22 | inout r23
| inout r24 | inout r25 | inout r26 | inout r27
| inout r28 | inout r29 | inout r30 | inout r31
;

// 64-bit Memory operand
operand_type Mem64(in address:reg_opr, inline offset:int):nat64;
type simm16:Type(0) := int_range((-32768), 32767);
type nsimm16:Type(0) := int_range((-32767), 32768);

procedure Move(out dst:dst_reg_opr, in src:reg_opr)
procedure Move(out dst:reg_opr, in src:reg_opr)
{:public}
{:instruction Ins(S.Move(dst, src))}
ensures
Expand All @@ -94,7 +84,7 @@ procedure Move(out dst:dst_reg_opr, in src:reg_opr)
}

// Load from 64-bit memory to general-purpose register
procedure Load64(out dst:dst_reg_opr, in src:Mem64)
procedure Load64(out dst:reg_opr, in src:Mem64)
{:public}
{:instruction Ins(S.Load64(dst, src))}
ensures
Expand All @@ -112,7 +102,7 @@ procedure Store64(in src:reg_opr, out dst:Mem64)
}

// Load Immediate to general-purpose register
procedure LoadImm64(out dst:dst_reg_opr, inline src:simm16)
procedure LoadImm64(out dst:reg_opr, inline src:simm16)
{:public}
{:instruction Ins(S.LoadImm64(dst, src))}
ensures
Expand All @@ -121,7 +111,7 @@ procedure LoadImm64(out dst:dst_reg_opr, inline src:simm16)
}

// Load address
procedure AddLa(out dst:dst_reg_opr, in src1:reg_opr, inline src2:simm16)
procedure AddLa(out dst:reg_opr, in src1:reg_opr, inline src2:simm16)
{:public}
{:instruction Ins(S.AddLa(dst, src1, src2))}
requires
Expand All @@ -132,7 +122,7 @@ procedure AddLa(out dst:dst_reg_opr, in src1:reg_opr, inline src2:simm16)
}

// Add two general-purpose registers. Assuming the result has no carry
procedure Add(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr)
procedure Add(out dst:reg_opr, in src1:reg_opr, in src2:reg_opr)
{:public}
{:instruction Ins(S.Add(dst, src1, src2))}
requires
Expand All @@ -143,7 +133,7 @@ procedure Add(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr)
}

// Add two general-purpose registers with wrapping
procedure AddWrap(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr)
procedure AddWrap(out dst:reg_opr, in src1:reg_opr, in src2:reg_opr)
{:public}
{:instruction Ins(S.Add(dst, src1, src2))}
ensures
Expand All @@ -152,7 +142,7 @@ procedure AddWrap(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr)
}

// Add general-purpose register amd immediate. Assuming the result has no carry
procedure AddImm(out dst:dst_reg_opr, in src1:reg_opr, inline src2:simm16)
procedure AddImm(out dst:reg_opr, in src1:reg_opr, inline src2:simm16)
{:public}
{:instruction Ins(S.AddImm(dst, src1, src2))}
requires
Expand All @@ -163,7 +153,7 @@ procedure AddImm(out dst:dst_reg_opr, in src1:reg_opr, inline src2:simm16)
}

// Add general-purpose register amd immediate with wrapping
procedure AddImmWrap(out dst:dst_reg_opr, in src1:reg_opr, inline src2:simm16)
procedure AddImmWrap(out dst:reg_opr, in src1:reg_opr, inline src2:simm16)
{:public}
{:instruction Ins(S.AddImm(dst, src1, src2))}
ensures
Expand All @@ -172,7 +162,7 @@ procedure AddImmWrap(out dst:dst_reg_opr, in src1:reg_opr, inline src2:simm16)
}

// Add two general-purpose registers plus carry with wrapping and store status of carry occurrence in XER register
procedure AddExtended(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr)
procedure AddExtended(out dst:reg_opr, in src1:reg_opr, in src2:reg_opr)
{:public}
{:instruction Ins(S.AddExtended(dst, src1, src2))}
modifies
Expand All @@ -184,7 +174,7 @@ procedure AddExtended(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr)
}

// Add two general-purpose registers plus overflow with wrapping and store status of overflow occurrence in XER register
procedure AddExtendedOV(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr)
procedure AddExtendedOV(out dst:reg_opr, in src1:reg_opr, in src2:reg_opr)
{:public}
{:instruction Ins(S.AddExtendedOV(dst, src1, src2))}
modifies
Expand All @@ -196,7 +186,7 @@ procedure AddExtendedOV(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr)
}

// Subtract two general-purpose registers. Assuming the result has no borrow
procedure Sub(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr)
procedure Sub(out dst:reg_opr, in src1:reg_opr, in src2:reg_opr)
{:public}
{:instruction Ins(S.Sub(dst, src1, src2))}
requires
Expand All @@ -207,7 +197,7 @@ procedure Sub(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr)
}

// Subtract two general-purpose registers with wrapping
procedure SubWrap(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr)
procedure SubWrap(out dst:reg_opr, in src1:reg_opr, in src2:reg_opr)
{:public}
{:instruction Ins(S.Sub(dst, src1, src2))}
ensures
Expand All @@ -216,7 +206,7 @@ procedure SubWrap(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr)
}

// Subtract general-purpose register amd immediate. Assuming the result has no borrow
procedure SubImm(out dst:dst_reg_opr, in src1:reg_opr, inline src2:nsimm16)
procedure SubImm(out dst:reg_opr, in src1:reg_opr, inline src2:nsimm16)
{:public}
{:instruction Ins(S.SubImm(dst, src1, src2))}
requires
Expand All @@ -227,7 +217,7 @@ procedure SubImm(out dst:dst_reg_opr, in src1:reg_opr, inline src2:nsimm16)
}

// Subtract general-purpose register amd immediate with wrapping
procedure SubImmWrap(out dst:dst_reg_opr, in src1:reg_opr, inline src2:nsimm16)
procedure SubImmWrap(out dst:reg_opr, in src1:reg_opr, inline src2:nsimm16)
{:public}
{:instruction Ins(S.SubImm(dst, src1, src2))}
ensures
Expand All @@ -236,7 +226,7 @@ procedure SubImmWrap(out dst:dst_reg_opr, in src1:reg_opr, inline src2:nsimm16)
}

// Mutiply two general-purpose registers. Assuming the product fits in 64-bit
procedure MulLow64(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr)
procedure MulLow64(out dst:reg_opr, in src1:reg_opr, in src2:reg_opr)
{:public}
{:instruction Ins(S.MulLow64(dst, src1, src2))}
requires
Expand All @@ -247,7 +237,7 @@ procedure MulLow64(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr)
}

// Mutiply two general-purpose registers ans store the low 64-bit of product in the destination register
procedure MulLow64Wrap(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr)
procedure MulLow64Wrap(out dst:reg_opr, in src1:reg_opr, in src2:reg_opr)
{:public}
{:instruction Ins(S.MulLow64(dst, src1, src2))}
ensures
Expand All @@ -256,7 +246,7 @@ procedure MulLow64Wrap(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr)
}

// Mutiply two general-purpose registers ans store the high 64-bit of product in the destination register
procedure MulHigh64U(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr)
procedure MulHigh64U(out dst:reg_opr, in src1:reg_opr, in src2:reg_opr)
{:public}
{:instruction Ins(S.MulHigh64U(dst, src1, src2))}
ensures
Expand All @@ -265,7 +255,7 @@ procedure MulHigh64U(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr)
}

// XOR operation of two general-purpose registers
procedure Xor(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr)
procedure Xor(out dst:reg_opr, in src1:reg_opr, in src2:reg_opr)
{:public}
{:instruction Ins(S.Xor(dst, src1, src2))}
ensures
Expand All @@ -274,7 +264,7 @@ procedure Xor(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr)
}

// AND operation of two general-purpose registers
procedure And(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr)
procedure And(out dst:reg_opr, in src1:reg_opr, in src2:reg_opr)
{:public}
{:instruction Ins(S.And(dst, src1, src2))}
ensures
Expand All @@ -283,7 +273,7 @@ procedure And(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr)
}

// Shift right general-purpose register with immediate bit value
procedure Sr64Imm(out dst:dst_reg_opr, in src1:reg_opr, inline src2:bits64)
procedure Sr64Imm(out dst:reg_opr, in src1:reg_opr, inline src2:bits64)
{:public}
{:instruction Ins(S.Sr64Imm(dst, src1, src2))}
ensures
Expand All @@ -292,7 +282,7 @@ procedure Sr64Imm(out dst:dst_reg_opr, in src1:reg_opr, inline src2:bits64)
}

// Shift left general-purpose register with immediate bit value
procedure Sl64Imm(out dst:dst_reg_opr, in src1:reg_opr, inline src2:bits64)
procedure Sl64Imm(out dst:reg_opr, in src1:reg_opr, inline src2:bits64)
{:public}
{:instruction Ins(S.Sl64Imm(dst, src1, src2))}
ensures
Expand Down
2 changes: 1 addition & 1 deletion fstar/code/arch/ppc64le/PPC64LE.Vale.InsMem.vaf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ procedure Mem64_lemma(ghost address:reg_opr, ghost offset:int)
}

// Load from 64-bit memory to general-purpose register
procedure MemLoad64(out dst:dst_reg_opr, in src:reg_opr, inline offset:int)
procedure MemLoad64(out dst:reg_opr, in src:reg_opr, inline offset:int)
{:public}
reads
mem;
Expand Down
Loading