[WIP] Initiate PowerPC64 little-endian support

Adding the following modules:
- Vale.PPC64LE.Machine_s
- Vale.PPC64LE.Instruction_s
- Vale.PPC64LE.Instructions_s

vale/specs/hardware/Vale.PPC64LE.Instruction_s.fst

@@ -0,0 +1,33 @@
+module Vale.PPC64LE.Instruction_s
+open FStar.Mul
+
+[@instr_attr]
+let rec instr_print_t_args (args:list instr_operand) : Type0 =
+ match args with
+ | [] -> instr_print
+ | (IOpEx i)::args -> arrow (instr_operand_t i) (instr_print_t_args args)
+ | (IOpIm _)::args -> instr_print_t_args args
+ | (IOpOpt _)::args -> instr_print_t_args args
+
+[@instr_attr]
+let rec instr_print_t (outs:list instr_operand_inout) (args:list instr_operand) : Type0 =
+ match outs with
+ | [] -> instr_print_t_args args
+ | (_, IOpEx i)::outs -> arrow (instr_operand_t i) (instr_print_t outs args)
+ | (_, IOpIm _)::outs -> instr_print_t outs args
+ | (_, IOpOpt _)::outs -> instr_print_t outs args
+
+noeq type instr_t (outs:list instr_out) (args:list instr_operand) (havoc_flags:flag_havoc) = {
+ i_eval:instr_eval_t outs args;
+ i_printer:instr_print_t outs args;
+}
+
+let make_ins
+ (#outs:list instr_out) (#args:list instr_operand) (#havoc_flags:flag_havoc)
+ (#f:normal (instr_eval_t outs args))
+ (print:normal (instr_print_t outs args))
+ : instr_dep outs args havoc_flags f =
+ {i_printer = print; i_eval = f}
+
+let print (name:string) (oprs:list instr_print_operand) : instr_print = Print name POpcode oprs
+let print_s (name:string) (oprs:list instr_print_operand) : instr_print = Print name PSuffix oprs

vale/specs/hardware/Vale.PPC64LE.Instruction_s.fsti

@@ -0,0 +1,142 @@
+module Vale.PPC64LE.Instruction_s
+open FStar.Mul
+open Vale.Def.Words_s
+open Vale.Def.Types_s
+open Vale.PPC64LE.Machine_s
+
+(*
+An generic instruction has:
+- zero or more input operands
+- zero or more output operands
+- a possible effect on the branch facility registers
+Some of the operands may be hard-coded to a particular register; some operands are optional; 
+other operands are flexible.
+*)
+type instr_operand_inout = | In | Out
+type instr_operand_explicit = // flexible operand
+ | IOpGpr : instr_operand_explicit
+ | IOpVec : instr_operand_explicit
+ | IOpVsx : instr_operand_explicit
+type instr_operand_implicit = // hard-coded operand
+ | IOpCr0 : instr_operand_implicit
+ | IOpCtr : instr_operand_implicit
+type instr_operand_optional = // optional operand
+ | IOpCr : instr_operand_optional
+type instr_operand =
+ | IOpEx : instr_operand_explicit -> instr_operand
+ | IOpIm : instr_operand_implicit -> instr_operand
+ | IOpOpt : instr_operand_optional -> instr_operand
+let instr_out = instr_operand_inout & instr_operand
+
+irreducible let instr_attr = ()
+unfold let normal (#a:Type) (x:a) : a = norm [zeta; iota; delta_attr [`%instr_attr]] x
+
+let arrow (a b:Type) = a -> b
+
+[@instr_attr] unfold let in (o:instr_operand) = (In, o)
+[@instr_attr] unfold let out (o:instr_operand) = (Out, o)
+[@instr_attr] unfold let opGpr = IOpEx IOpGpr
+[@instr_attr] unfold let opVec = IOpEx IOpVec
+[@instr_attr] unfold let opVsx = IOpEx IOpVsx
+[@instr_attr] unfold let opCr0 = IOpIm IOpCr0
+[@instr_attr] unfold let opCtr = IOpIm IOpCtr
+[@instr_attr] unfold let opCr = IOpOpt IOpCr
+
+[@instr_attr]
+let instr_val_t (o:instr_operand) : Type0 =
+ match o with
+ | IOpEx IOpGpr -> nat64
+ | IOpEx IOpVec -> nat128
+ | IOpEx IOpVsx -> nat128
+ | IOpIm IOpCr0 -> fixed_point_flag
+ | IOpIm IOpCtr -> nat64
+ | IOpIm IOpCr -> condition_register
+
+[@instr_attr]
+let rec instr_ret_t (outs:list instr_out) : Type0 =
+ match outs with
+ | [] -> unit
+ | [(_, o)] -> instr_val_t o
+ | (_, o)::outs -> instr_val_t o & instr_ret_t outs
+
+[@instr_attr]
+let rec instr_args_t (outs:list instr_out) (args:list instr_operand) : Type0 =
+ match args with
+ | [] -> option (instr_ret_t outs)
+ | i::args -> arrow (instr_val_t i) (instr_args_t outs args)
+
+[@instr_attr]
+let rec instr_inouts_t (outs inouts:list instr_out) (args:list instr_operand) : Type0 =
+ match inouts with
+ | [] -> instr_args_t outs args
+ | (Out, _)::inouts -> instr_inouts_t outs inouts args
+ | (In, i)::inouts -> arrow (instr_val_t i) (instr_inouts_t outs inouts args)
+
+(*
+An instr evaluator is a function of type:
+ in_outs1 ... -> in_outsi -> args1 -> ...> argsj -> (outs1 & (... & outsk) ...)
+where in_outs = [(b, o) in outs | b = In]
+*)
+[@instr_attr]
+let instr_eval_t (outs:list instr_out) (args:list instr_operand) : Type0 =
+ instr_inouts_t outs outs args
+
+[@instr_attr]
+let instr_operand_t (arg:instr_operand_explicit) : Type0 =
+ match arg with
+ | IOpGpr -> operand64
+ | IOpVec -> operand128
+ | IOpVsx -> operand128
+
+[@instr_attr]
+let rec instr_operands_t_args (args:list instr_operand) : Type0 =
+ match args with
+ | [] -> unit
+ | (IOpEx i)::args -> instr_operand_t i & instr_operands_t_args args
+ | (IOpIm _)::args -> instr_operands_t_args args
+ | (IOpOpt _)::args -> instr_operands_t_args args
+
+[@instr_attr]
+let rec instr_operands_t (outs:list instr_out) (args:list instr_operand) : Type0 =
+ match outs with
+ | [] -> instr_operands_t_args args
+ | (_, IOpEx i)::outs -> instr_operand_t i & instr_operands_t outs args
+ | (_, IOpIm _)::outs -> instr_operands_t outs args
+ | (_, IOpOpt _)::outs -> instr_operands_t outs args
+
+type instr_print_operand =
+ | PGpr : operand64 -> instr_print_operand
+ | PVec : operand128 -> instr_print_operand
+ | PVsx : operand128 -> instr_print_operand
+ | PImm : int16 -> instr_print_operand
+ | PShift : imm_shift -> instr_print_operand
+type instr_print =
+ | Print : string -> instr_print_kind -> list instr_print_operand -> instr_print
+
+type flag_havoc = | HavocFlags | PreserveFlags
+
+val instr_t (outs:list instr_out) (args:list instr_operand) (havoc_flags:flag_havoc) : Type0
+
+noeq type instr_t_record =
+ | InstrTypeRecord :
+ #outs:list instr_out ->
+ #args:list instr_operand ->
+ #havoc_flags:flag_havoc ->
+ i:instr_t outs args havoc_flags ->
+ instr_t_record
+
+val instr_eval
+ (#outs:list instr_out) (#args:list instr_operand) (#havoc_flags:flag_havoc)
+ (i:instr_t outs args havoc_flags)
+ : norm [zeta; iota; delta_attr [`%instr_attr]] (instr_eval_t outs args)
+
+val instr_printer
+ (#outs:list instr_out) (#args:list instr_operand) (#havoc_flags:flag_havoc)
+ (i:instr_t outs args havoc_flags) (oprs:normal (instr_operands_t outs args))
+ : instr_print
+
+let instr_dep
+ (outs:list instr_out) (args:list instr_operand) (havoc_flags:flag_havoc)
+ (f:normal (instr_eval_t outs args))
+ : Type0 =
+ i:(instr_t outs args havoc_flags){instr_eval i == f}

vale/specs/hardware/Vale.PPC64LE.Instructions_s.fst

@@ -0,0 +1,31 @@
+module Vale.PPC64LE.Instructions_s
+open FStar.Mul
+friend Vale.PPC64LE.Instruction_s
+
+let ins_Load64 = make_ins (fun rt ra -> print_s "ld" [PGpr rt; PGpr ra])
+
+let ins_LoadRev64 = make_ins (fun rt ra rb -> print_s "ldbrx" [PGpr rt; PGpr ra; PGpr rb])
+
+let ins_ByteRev64 = make_ins (fun ra rs -> print_s "brd" [PGpr ra; PGpr rs])
+
+let ins_SetRegLT = make_ins (fun rx ry rz -> print_s "isellt" [PGpr rx; PGpr ry; PGpr rz])
+
+let ins_Add = make_ins (fun rt ra rb -> print_s "add" [PGpr rt; PGpr ra; PGpr rb])
+
+let ins_AddCarry = make_ins (fun rt ra rb -> print_s "addc" [PGpr rt; PGpr ra; PGpr rb])
+
+let ins_Sub = make_ins (fun rt ra rb -> print_s "sub" [PGpr rt; PGpr ra; PGpr rb])
+
+let ins_SubCarry = make_ins (fun rt ra rb -> print_s "subc" [PGpr rt; PGpr ra; PGpr rb])
+
+let ins_And = make_ins (fun rt rs rb -> print_s "and" [PGpr rt; PGpr rs; PGpr rb])
+
+let ins_Xor = make_ins (fun rt rs rb -> print_s "xor" [PGpr rt; PGpr rs; PGpr rb])
+
+let ins_SRImm64 = make_ins (fun rx ry n -> print_s "srdi" [PGpr rx; PGpr ry; PImm n])
+
+let ins_SLImm64 = make_ins (fun rx ry n -> print_s "sldi" [PGpr rx; PGpr ry; PImm n])
+
+let MulLow32 = make_ins (fun rt ra rb -> print_s "mullw" [PGpr rt; PGpr ra; PGpr rb])
+
+let MulHigh32 = make_ins (fun rt ra rb -> print_s "mulhw" [PGpr rt; PGpr ra; PGpr rb])

vale/specs/hardware/Vale.PPC64LE.Machine_s.fst

@@ -0,0 +1,145 @@
+module Vale.PPC64LE.Machine_s
+open FStar.Mul
+
+type condition_register =
+ | Cr0 : condition_register
+ | Cr1 : condition_register
+ | Cr2 : condition_register
+ | Cr3 : condition_register
+ | Cr4 : condition_register
+ | Cr5 : condition_register
+ | Cr6 : condition_register
+ | Cr7 : condition_register
+
+type fixed_point_flag = {
+ f_lt:bool; // negative
+ f_gt:bool; // positive
+ f_eq:bool; // zero
+ f_so:bool // summary overflow
+}
+
+let int16 = Lib.IntTypes.int16
+unfold let nat64 = Vale.Def.Types_s.nat64
+unfold let nat128 = Vale.Def.Words_s.nat128
+
+let n_reg_files = 3
+let reg_file_id = rf:nat{rf < n_reg_files}
+let n_regs (rf:reg_file_id) : nat =
+ match rf with
+ | 0 -> 32
+ | 1 -> 16
+ | 1 -> 32
+let t_reg_file (rf:reg_file_id) : Type0 =
+ match rf with
+ | 0 -> nat64
+ | 1 -> nat128
+ | 2 -> nat128
+
+let reg_id (rf:reg_file_id) : Type0 = r:nat{r < n_regs rf}
+
+irreducible let va_qattr = ()
+
+[@va_qattr]
+type reg =
+ | Reg: rf:reg_file_id -> r:reg_id rf -> reg
+
+let t_reg (r:reg) : Type0 = t_reg_file r.rf
+
+type maddr:eqtype =
+ | MReg: ra:reg -> ds:int -> maddr
+ | MIndex: ra:reg -> rb:reg -> maddr
+
+let imm_shift : Type0 = i:nat{i < 64}
+
+type imm:eqtype =
+ | IValue: i:int16 -> imm
+ | IShift: i:imm_shift -> imm
+
+[@va_qattr]
+type operand (tr:eqtype) : eqtype =
+ | OImm: i:imm -> operand tr
+ | OReg: r:tr -> operand tr
+ | OMem: m:maddr -> operand tr
+
+[@va_qattr]
+let operand_rf (rf:reg_file_id) : eqtype =
+ operand (reg_id rf)
+
+[@va_qattr]
+unfold let oreg (r:reg) : operand_rf r.rf =
+ OReg r.r
+
+let reg_gp : Type0 = r:nat{r < 32}
+let reg_vec : Type0 = r:nat{r < 16}
+
+[@va_qattr] unfold let r0 : reg_gp = 0
+[@va_qattr] unfold let r1 : reg_gp = 1
+[@va_qattr] unfold let r2 : reg_gp = 2
+[@va_qattr] unfold let r3 : reg_gp = 3
+[@va_qattr] unfold let r4 : reg_gp = 4
+[@va_qattr] unfold let r5 : reg_gp = 5
+[@va_qattr] unfold let r6 : reg_gp = 6
+[@va_qattr] unfold let r7 : reg_gp = 7
+[@va_qattr] unfold let r8 : reg_gp = 8
+[@va_qattr] unfold let r9 : reg_gp = 9
+[@va_qattr] unfold let r10 : reg_gp = 10
+[@va_qattr] unfold let r11 : reg_gp = 11
+[@va_qattr] unfold let r12 : reg_gp = 12
+[@va_qattr] unfold let r13 : reg_gp = 13
+[@va_qattr] unfold let r14 : reg_gp = 14
+[@va_qattr] unfold let r15 : reg_gp = 15
+[@va_qattr] unfold let r16 : reg_gp = 16
+[@va_qattr] unfold let r17 : reg_gp = 17
+[@va_qattr] unfold let r18 : reg_gp = 18
+[@va_qattr] unfold let r19 : reg_gp = 19
+[@va_qattr] unfold let r20 : reg_gp = 20
+[@va_qattr] unfold let r21 : reg_gp = 21
+[@va_qattr] unfold let r22 : reg_gp = 22
+[@va_qattr] unfold let r23 : reg_gp = 23
+[@va_qattr] unfold let r24 : reg_gp = 24
+[@va_qattr] unfold let r25 : reg_gp = 25
+[@va_qattr] unfold let r26 : reg_gp = 26
+[@va_qattr] unfold let r27 : reg_gp = 27
+[@va_qattr] unfold let r28 : reg_gp = 28
+[@va_qattr] unfold let r29 : reg_gp = 29
+[@va_qattr] unfold let r30 : reg_gp = 30
+[@va_qattr] unfold let r31 : reg_gp = 31
+
+[@va_qattr] unfold let reg_r0 : reg = Reg 0 0
+[@va_qattr] unfold let reg_r1 : reg = Reg 0 1
+[@va_qattr] unfold let reg_r2 : reg = Reg 0 2
+[@va_qattr] unfold let reg_r3 : reg = Reg 0 3
+[@va_qattr] unfold let reg_r4 : reg = Reg 0 4
+[@va_qattr] unfold let reg_r5 : reg = Reg 0 5
+[@va_qattr] unfold let reg_r6 : reg = Reg 0 6
+[@va_qattr] unfold let reg_r7 : reg = Reg 0 7
+[@va_qattr] unfold let reg_r8 : reg = Reg 0 8
+[@va_qattr] unfold let reg_r9 : reg = Reg 0 9
+[@va_qattr] unfold let reg_r10 : reg = Reg 0 10
+[@va_qattr] unfold let reg_r11 : reg = Reg 0 11
+[@va_qattr] unfold let reg_r12 : reg = Reg 0 12
+[@va_qattr] unfold let reg_r13 : reg = Reg 0 13
+[@va_qattr] unfold let reg_r14 : reg = Reg 0 14
+[@va_qattr] unfold let reg_r15 : reg = Reg 0 15
+[@va_qattr] unfold let reg_r16 : reg = Reg 0 16
+[@va_qattr] unfold let reg_r17 : reg = Reg 0 17
+[@va_qattr] unfold let reg_r18 : reg = Reg 0 18
+[@va_qattr] unfold let reg_r19 : reg = Reg 0 19
+[@va_qattr] unfold let reg_r20 : reg = Reg 0 20
+[@va_qattr] unfold let reg_r21 : reg = Reg 0 21
+[@va_qattr] unfold let reg_r22 : reg = Reg 0 22
+[@va_qattr] unfold let reg_r23 : reg = Reg 0 23
+[@va_qattr] unfold let reg_r24 : reg = Reg 0 24
+[@va_qattr] unfold let reg_r25 : reg = Reg 0 25
+[@va_qattr] unfold let reg_r26 : reg = Reg 0 26
+[@va_qattr] unfold let reg_r27 : reg = Reg 0 27
+[@va_qattr] unfold let reg_r28 : reg = Reg 0 28
+[@va_qattr] unfold let reg_r29 : reg = Reg 0 29
+[@va_qattr] unfold let reg_r30 : reg = Reg 0 30
+[@va_qattr] unfold let reg_r31 : reg = Reg 0 31
+
+[@va_qattr]
+let operand64:eqtype = operand reg_gp
+
+[@va_qattr]
+let operand128:eqtype = operand reg_vec