Commit 2c79f09d authored by Julian Kranz's avatar Julian Kranz

Merge branch 'experimental'

parents 199d41a5 728f3ed3
......@@ -21,7 +21,9 @@ GDSL_ASM_HL=specifications/asm/asm.ml specifications/asm/asm-pretty.ml specifica
GDSL_RREIL_HL=specifications/rreil/rreil.ml specifications/rreil/rreil-examples.ml specifications/rreil/rreil-cif.ml specifications/rreil/rreil-pretty.ml specifications/rreil/fmap.ml specifications/rreil/rreil-opt.ml specifications/rreil/rreil-translator.ml
GDSL_OPT_HL=specifications/rreil/rreil-liveness.ml specifications/rreil/rreil-forward-subst.ml specifications/rreil/forward-subst/inline.ml specifications/rreil/rreil-cleanup.ml specifications/rreil/forward-subst/substitute.ml specifications/rreil/forward-subst/substmap.ml specifications/rreil/forward-subst/simplify-expressions.ml
GDSL_MIPS_HL=specifications/mips/mips.ml specifications/mips/mips-pretty.ml specifications/mips/mips-rreil-pretty.ml specifications/mips/mips-rreil-registermapping.ml specifications/mips/mips-rreil-translator.ml specifications/mips/mips-liveness.ml specifications/mips/mips-asm.ml specifications/mips/mips-traverse.ml
GDSL_MIPS_HL_R5=specifications/mips/mips_r5.ml specifications/mips/mips-pretty_r5.ml specifications/mips/mips-rreil-translator_r5.ml specifications/mips/mips-asm_r5.ml specifications/mips/mips-traverse_r5.ml
GDSL_MIPS_HL_R6=specifications/mips/mips_r6.ml specifications/mips/mips-pretty_r6.ml specifications/mips/mips-rreil-translator_r6.ml specifications/mips/mips-asm_r6.ml specifications/mips/mips-traverse_r6.ml
GDSL_MIPS_HL=specifications/mips/mips.ml specifications/mips/mips-pretty.ml specifications/mips/mips-rreil-pretty.ml specifications/mips/mips-rreil-registermapping.ml specifications/mips/mips-rreil-translator.ml specifications/mips/mips-liveness.ml specifications/mips/mips-asm.ml specifications/mips/mips-traverse.ml $(GDSL_MIPS_HL_R6)
GDSL_MIPS_TRANS_HL=
GDSL_SOURCES=$(GDSL_BASIS_HL) $(GDSL_RREIL_HL) $(GDSL_MIPS_HL) $(GDSL_MIPS_TRANS_HL) $(GDSL_OPT_HL) $(GDSL_ASM_HL)
......
......@@ -52,6 +52,8 @@ val asm-annotated a opnd = ASM_ANNOTATED {ann=a, opnd=opnd}
val asm-sum l r = ASM_SUM {lhs=l, rhs=r}
val asm-scale f r = ASM_SCALE {factor=f, rhs=r}
val asm-bounded b o = ASM_BOUNDED {boundary=b, opnd=o}
val asm-signed o = ASM_SIGN {signedness=ASM_SIGNED, opnd=o}
val asm-unsigned o = ASM_SIGN {signedness=ASM_UNSIGNED, opnd=o}
val asm-composite c = ASM_COMPOSITE c
val asm-boundary-sz sz = ASM_BOUNDARY_SZ sz
......
......@@ -55,6 +55,7 @@ in case i of
| INSTRINDEX28 i: inner i 28
| COFUN i: inner i 25
| OP i: inner i 5
| _ : revision/generalize-immediate i
end end
val generalize-ua ua =
......
val revision/generalize-immediate i =
case i of
IMM16 x: asm-bounded (asm-boundary-sz 16) (asm-imm (zx x))
end
val revision/generalize-immediate i = let
val inner i sz = asm-bounded (asm-boundary-sz sz) (asm-imm (zx i))
in case i of
IMM21 i: inner i 21
| IMM32 i: inner i 32
| BP i: inner i 2
| SA2 i: inner i 2
| OFFSET11 i: inner i 11
| OFFSET23 i: inner i 23
| OFFSET28 i: inner i 28
| C2CONDITION i: inner i 5
end end
export pretty : (insndata) -> rope
val pretty i = show/instruction i
val -++ a b = a +++ " " +++ b
val show/lvalue opnd =
case opnd of
GPR r: show/register r
| FPR r: show/register r
end
val show/rvalue opnd =
case opnd of
LVALUE l: show/lvalue l
| IMM imm: show/immediate imm
end
val show/immediate imm =
case imm of
IMM5 x: show-int (zx x)
| IMM16 x: show-int (zx x)
| OFFSET9 x: show-int (zx x)
| OFFSET16 x: show-int (zx x)
| SEL x: show-int (zx x)
| IMPL x: show-int (zx x)
| CODE10 x: show-int (zx x)
| CODE19 x: show-int (zx x)
| CODE20 x: show-int (zx x)
| STYPE x: show-int (zx x)
| POSSIZE x: show-int (zx x)
| SIZE x: show-int (zx x)
| POS x: show-int (zx x)
| HINT x: show-int (zx x)
| INSTRINDEX x: show-int (zx x)
| COFUN x: show-int (zx x)
| CC x: show-int (zx x)
| COND x: show-int (zx x)
| OP x: show-int (zx x)
end
val show/format format =
case format of
S : "S"
| D : "D"
| W : "W"
| L : "L"
| PS : "PS"
end
val show/register r =
case r of
ZERO: "zero"
| AT: "at"
| V0: "v0"
| V1: "v1"
| A0: "a0"
| A1: "a1"
| A2: "a2"
| A3: "a3"
| T0: "t0"
| T1: "t1"
| T2: "t2"
| T3: "t3"
| T4: "t4"
| T5: "t5"
| T6: "t6"
| T7: "t7"
| S0: "s0"
| S1: "s1"
| S2: "s2"
| S3: "s3"
| S4: "s4"
| S5: "s5"
| S6: "s6"
| S7: "s7"
| T8: "t8"
| T9: "t9"
| K0: "k0"
| K1: "k1"
| GP: "gp"
| SP: "sp"
| S8: "s8"
| RA: "ra"
| HI: "hi"
| LO: "lo"
| PC: "pc"
| F0: "f0"
| F1: "f1"
| F2: "f2"
| F3: "f3"
| F4: "f4"
| F5: "f5"
| F6: "f6"
| F7: "f7"
| F8: "f8"
| F9: "f9"
| F10: "f10"
| F11: "f11"
| F12: "f12"
| F13: "f13"
| F14: "f14"
| F15: "f15"
| F16: "f16"
| F17: "f17"
| F18: "f18"
| F19: "f19"
| F20: "f20"
| F21: "f21"
| F22: "f22"
| F23: "f23"
| F24: "f24"
| F25: "f25"
| F26: "f26"
| F27: "f27"
| F28: "f28"
| F29: "f29"
| F30: "f30"
| F31: "f31"
| FIR: "fir"
| FCCR: "fccr"
| FEXR: "fexr"
| FENR: "fenr"
| FCSR: "fcsr"
end
# -> sftl
val show/unop-src x = show/rvalue x.source
val show/unop x = show/lvalue x.destination
val show/binop-src x = show/rvalue x.source1 +++ ", " +++ show/rvalue x.source2
val show/binop-fmt x = show/lvalue x.destination +++ ", " +++ show/rvalue x.source
val show/binop x = show/lvalue x.destination +++ ", " +++ show/rvalue x.source
val show/ternop-src x = show/rvalue x.source1 +++ ", " +++ show/rvalue x.source2 +++ ", " +++ show/rvalue x.source3
val show/ternop x = show/lvalue x.destination +++ ", " +++ show/rvalue x.source1 +++ ", " +++ show/rvalue x.source2
val show/ternop-fmt x = show/lvalue x.destination +++ ", " +++ show/rvalue x.source1 +++ ", " +++ show/rvalue x.source2
val show/quadop x = show/lvalue x.destination +++ ", " +++ show/rvalue x.source1 +++ ", " +++ show/rvalue x.source2 +++ ", " +++ show/rvalue x.source3
val show/quadop-fmt x = show/lvalue x.destination +++ ", " +++ show/rvalue x.source1 +++ ", " +++ show/rvalue x.source2 +++ ", " +++ show/rvalue x.source3
val show/quadop-fmt-src x = show/rvalue x.source1 +++ ", " +++ show/rvalue x.source2 +++ ", " +++ show/rvalue x.source3 +++ ", " +++ show/rvalue x.source4
val show/instruction insn = let
val show/ua mnemonic ua = case ua of
NULLOP: mnemonic
| UNOP_SRC x: mnemonic -++ show/unop-src x
| UNOP x: mnemonic -++ show/unop x
| BINOP_SRC x: mnemonic -++ show/binop-src x
| BINOP_FMT x: mnemonic +++ "." +++ show/format x.fmt -++ show/binop-fmt x
| BINOP x: mnemonic -++ show/binop x
| TERNOP_SRC x: mnemonic -++ show/ternop-src x
| TERNOP x: mnemonic -++ show/ternop x
| TERNOP_FMT x: mnemonic +++ "." +++ show/format x.fmt -++ show/ternop-fmt x
| QUADOP x: mnemonic -++ show/quadop x
| QUADOP_FMT x: mnemonic +++ "." +++ show/format x.fmt -++ show/quadop-fmt x
| QUADOP_FMT_SRC x: mnemonic +++ "." +++ show/format x.fmt -++ show/quadop-fmt-src x
end
in
traverse show/ua insn.insn
end
# <- sutl
......@@ -88,6 +88,7 @@ val show/immediate imm =
| INSTRINDEX28 x: show-int (zx x)
| COFUN x: show-int (zx x)
| OP x: show-int (zx x)
| _ : revision/show/immediate imm
end
val show/format format =
......@@ -96,27 +97,7 @@ val show/format format =
| D : "D"
| W : "W"
| L : "L"
| PS : "PS"
end
val show/condop cond =
case cond of
C_F: "F"
| C_UN: "UN"
| C_EQ: "EQ"
| C_UEQ: "UEQ"
| C_OLT: "OLT"
| C_ULT: "ULT"
| C_OLE: "OLE"
| C_ULE: "ULE"
| C_SF: "SF"
| C_NGLE: "NGLE"
| C_SEQ: "SEQ"
| C_NGL: "NGL"
| C_LT: "LT"
| C_NGE: "NGE"
| C_LE: "LE"
| C_NGT: "NGT"
| _ : revision/show/format format
end
val show/fccode fcc =
......
val show/condop cond =
case cond of
C_F: "F"
| C_UN: "UN"
| C_EQ: "EQ"
| C_UEQ: "UEQ"
| C_OLT: "OLT"
| C_ULT: "ULT"
| C_OLE: "OLE"
| C_ULE: "ULE"
| C_SF: "SF"
| C_NGLE: "NGLE"
| C_SEQ: "SEQ"
| C_NGL: "NGL"
| C_LT: "LT"
| C_NGE: "NGE"
| C_LE: "LE"
| C_NGT: "NGT"
end
val revision/show/immediate imm = "ERROR"
val revision/show/format format =
case format of
PS : "PS"
end
val show/condop cond =
case cond of
C_AF: "AF"
| C_UN: "UN"
| C_EQ: "EQ"
| C_UEQ: "UEQ"
| C_LT: "LT"
| C_ULT: "ULT"
| C_LE: "LE"
| C_ULE: "ULE"
| C_SAF: "SAF"
| C_SUN: "SUN"
| C_SEQ: "SEQ"
| C_SUEQ: "SUEQ"
| C_SLT: "SLT"
| C_SULT: "SULT"
| C_SLE: "SLE"
| C_SULE: "SULE"
| C_AT: "AT"
| C_OR: "OR"
| C_UNE: "UNE"
| C_NE: "NE"
| C_UGE: "UGE"
| C_OGE: "OGE"
| C_UGT: "UGT"
| C_OGT: "OGT"
| C_SAT: "SAT"
| C_SOR: "SOR"
| C_SUNE: "SUNE"
| C_SNE: "SNE"
| C_SUGE: "SUGE"
| C_SOGE: "SOGE"
| C_SUGT: "SUGT"
| C_SOGT: "SOGT"
end
val revision/show/immediate imm =
case imm of
IMM21 x: show-int (zx x)
| IMM32 x: show-int (zx x)
| BP x: show-int (zx x)
| SA2 x: show-int (zx x)
| OFFSET11 x: show-int (zx x)
| OFFSET23 x: show-int (zx x)
| OFFSET28 x: show-int (zx x)
| C2CONDITION x: show-int (zx x)
end
val revision/show/format format = "ERROR"
val revision/sizeof-imm imm = 0
val revision/rval-imm sn x = SEM_LIN_IMM {const=0}
val sem-addi x = do
rs <- rval Signed x.op2;
imm <- rval Signed x.op3;
size <- return (sizeof-lval x.op1);
res <- mktemp;
add size res rs imm;
overflow-add-addi size res rs imm;
write x.op1 (var res)
end
val sem-beql x = sem-b /eq x
val sem-bgezal x = sem-bz-link /ges x
val sem-bgezall x = sem-bz-link /ges x
val sem-bgezl x = sem-bz /ges x
val sem-bgtzl x = sem-bz /gts x
val sem-blezl x = sem-bz /les x
val sem-bltzal x = sem-bz-link /lts x
val sem-bltzall x = sem-bz-link /lts x
val sem-bltzl x = sem-bz /lts x
val sem-bnel x = sem-b /neq x
val sem-div-divu div_op mod_op x = do
num <- rval Signed x.op1;
denom <- rval Signed x.op2;
size <- return (sizeof-rval x.op1);
hi <- return (semantic-reg-of Sem_HI);
lo <- return (semantic-reg-of Sem_LO);
div_op size lo num denom;
mod_op size hi num denom
end
val sem-div x = sem-div-divu divs mods x
val sem-divu x = sem-div-divu div mod x
val sem-lui x = do
immediate <- rval Unsigned x.op2;
size <- return (sizeof-lval x.op1);
size_imm <- return (sizeof-rval x.op2);
res <- mktemp;
shl size res immediate (imm (32-size_imm));
write x.op1 (var res)
end
val sem-lwl x = do
off/base <- rval Signed x.op2;
base <- return (extract-tuple off/base).opnd1;
off <- return (extract-tuple off/base).opnd2;
rt <- lval Signed x.op1;
size <- return (sizeof-lval x.op1);
vaddr <- mktemp;
add size vaddr base off;
bcpu <- is-big-endian-cpu;
bcpu2 <- mktemp;
movsx 2 bcpu2 1 bcpu;
byte <- mktemp;
xorb 2 byte (var vaddr) (var bcpu2);
shl 32 byte (var byte) (imm 3);
memword <- mktemp;
load 32 memword size (var vaddr);
lshift <- mktemp;
sub size lshift (imm 24) (var byte);
high <- mktemp;
shl size high (var memword) (var lshift);
rshift <- mktemp;
add size rshift (imm 8) (var byte);
low <- mktemp;
shl size low rt (var rshift);
shr size low (var low) (var rshift);
res <- mktemp;
orb size res (var high) (var low);
write x.op1 (var res)
end
val sem-lwr x = do
off/base <- rval Signed x.op2;
base <- return (extract-tuple off/base).opnd1;
off <- return (extract-tuple off/base).opnd2;
rt <- lval Signed x.op1;
size <- return (sizeof-lval x.op1);
vaddr <- mktemp;
add size vaddr base off;
bcpu <- is-big-endian-cpu;
bcpu2 <- mktemp;
movsx 2 bcpu2 1 bcpu;
byte <- mktemp;
xorb 2 byte (var vaddr) (var bcpu2);
shl 32 byte (var byte) (imm 3);
memword <- mktemp;
load 32 memword size (var vaddr);
lshift <- mktemp;
sub size lshift (imm 32) (var byte);
high <- mktemp;
shr size high (var memword) (var lshift);
shl size high (var high) (var lshift);
rshift <- mktemp;
sub size rshift (imm 31) (var byte);
low <- mktemp;
shl size low rt (var rshift);
shr size low (var low) (var rshift);
res <- mktemp;
orb size res (var high) (var low);
write x.op1 (var res)
end
val sem-jr x = do
rs <- rval Signed x.op;
size <- return (sizeof-rval x.op);
pc <- return (semantic-reg-of Sem_SREG);
pc_true <- mktemp;
mov size pc_true rs;
pc_false <- mktemp;
mov size pc_false rs;
mov 1 pc_false (imm 0);
config1CA <- return (fCA);
cond <- /eq 1 (var config1CA) (imm 0);
isamode <- return (semantic-reg-of Sem_ISA_MODE);
_if (/neq 1 (var config1CA) (imm 0)) _then
mov isamode.size isamode rs;
cbranch cond (address pc.size (var pc_true)) (address pc.size (var pc_false))
end
val sem-jr-hb x = sem-jr x
val sem-jalx x = do
isamode <- return (semantic-reg-of Sem_ISA_MODE);
xorb 1 isamode (var isamode) (imm 1);
sem-jal x
end
val sem-madd x = sem-madd-maddu-msub-msubu movsx add x
val sem-maddu x = sem-madd-maddu-msub-msubu movzx add x
val sem-madd-maddu-msub-msubu ext_op add_sub_op x = do
rs <- rval Signed x.op1;
rt <- rval Signed x.op2;
size <- return (sizeof-rval x.op1);
rs_ext <- mktemp;
ext_op (size*2) rs_ext size rs;
rt_ext <- mktemp;
ext_op (size*2) rt_ext size rt;
res <- mktemp;
mul (size*2) res (var rs_ext) (var rt_ext);
hi <- return (semantic-reg-of Sem_HI);
lo <- return (semantic-reg-of Sem_LO);
hilo <- mktemp;
movzx (size*2) hilo size (var lo);
mov size (at-offset hilo size) (var hi);
add_sub_op (size*2) res (var res) (var hilo);
mov size lo (var res);
mov size hi (var (at-offset res size))
end
val sem-msub x = sem-madd-maddu-msub-msubu movzx sub x
val sem-msubu x = sem-madd-maddu-msub-msubu movzx sub x
val sem-mfhi x = do
hi <- return (semantic-reg-of Sem_HI);
write x.op (var hi)
end
val sem-mflo x = do
lo <- return (semantic-reg-of Sem_LO);
write x.op (var lo)
end
val sem-movn-movz cmp_op x = do
rs <- rval Signed x.op2;
rt <- rval Signed x.op3;
size <- return (sizeof-rval x.op2);
_if (cmp_op size rt (imm 0)) _then
write x.op1 rs
end
val sem-movn x = sem-movn-movz /neq x
val sem-movz x = sem-movn-movz /eq x
val sem-movf-movt x i = do
rs <- rval Signed x.op2;
cc <- (rval Signed x.op3);
_if (/eq 1 cc (imm i)) _then
write x.op1 rs
end
val sem-movf x = sem-movf-movt x 0
val sem-movt x = sem-movf-movt x 1
val sem-mthi x = do
rs <- rval Signed x.op;
hi <- return (semantic-reg-of Sem_HI);
mov hi.size hi rs
end
val sem-mtlo x = do
rs <- rval Signed x.op;
lo <- return (semantic-reg-of Sem_LO);
mov lo.size lo rs
end
val sem-mult-multu ext_op x = do
rs <- rval Signed x.op1;
rt <- rval Signed x.op2;
size <- return (sizeof-rval x.op1);
rs_ext <- mktemp;
ext_op (size*2) rs_ext size rs;
rt_ext <- mktemp;
ext_op (size*2) rt_ext size rt;
res <- mktemp;
mul (size*2) res (var rs_ext) (var rt_ext);
hi <- return (semantic-reg-of Sem_HI);
lo <- return (semantic-reg-of Sem_LO);
mov size lo (var res);
mov size hi (var (at-offset res size))
end
val sem-mult x = sem-mult-multu movsx x
val sem-multu x = sem-mult-multu movzx x
val sem-mul x = do
rs <- rval Signed x.op2;
rt <- rval Signed x.op3;
size <- return (sizeof-rval x.op2);
rs_ext <- mktemp;
movsx (size*2) rs_ext size rs;
rt_ext <- mktemp;
movsx (size*2) rt_ext size rt;
res <- mktemp;
mul (size*2) res (var rs_ext) (var rt_ext);
write x.op1 (var res)
end
val revision/semantics i =
case i of
ADDI x: sem-addi x
| ALNV-PS x: sem-default-quadop-lrrr-generic i x
| BC1F x: sem-default-binop-rr-generic i x
| BC1FL x: sem-default-binop-rr-generic i x
| BC1T x: sem-default-binop-rr-generic i x
| BC1TL x: sem-default-binop-rr-generic i x
| BC2F x: sem-default-binop-rr-generic i x
| BC2FL x: sem-default-binop-rr-generic i x
| BC2T x: sem-default-binop-rr-generic i x
| BC2TL x: sem-default-binop-rr-generic i x
| BEQL x: sem-beql x
| BGEZAL x: sem-bgezal x
| BGEZALL x: sem-bgezall x
| BGEZL x: sem-bgezl x
| BGTZL x: sem-bgtzl x
| BLEZL x: sem-blezl x
| BLTZAL x: sem-bltzal x
| BLTZALL x: sem-bltzall x
| BLTZL x: sem-bltzl x
| BNEL x: sem-bnel x
| C-cond-fmt x: sem-default-ternop-cflrr-generic i x
| CVT-PS-S x: sem-default-ternop-lrr-generic i x
| CVT-S-PL x: sem-default-binop-lr-generic i x
| CVT-S-PU x: sem-default-binop-lr-generic i x
| DIV x: sem-div x
| DIVU x: sem-divu x
| JR x: sem-jr x
| JR-HB x: sem-jr-hb x
| JALX x: sem-jalx x
| LDC2 x: sem-default-binop-rr-tuple-generic i x
| LDXC1 x: sem-default-binop-lr-tuple-generic i x
| LUI x: sem-lui x
| LUXC1 x: sem-default-binop-lr-tuple-generic i x
| LWC2 x: sem-default-binop-rr-tuple-generic i x
| LWL x: sem-lwl x
| LWLE x: sem-lwl x
| LWR x: sem-lwr x
| LWRE x: sem-lwr x
| LWXC1 x: sem-default-binop-lr-tuple-generic i x
| MADD x: sem-madd x
| MADD-fmt x: sem-default-ternop-flrr-generic i x
| MADDU x: sem-maddu x
| MFHI x: sem-mfhi x
| MFLO x: sem-mflo x
| MOVF x: sem-movf x
| MOVF-fmt x: sem-default-ternop-flrr-generic i x
| MOVN x: sem-movn x
| MOVN-fmt x: sem-default-ternop-flrr-generic i x
| MOVT x: sem-movt x
| MOVT-fmt x: sem-default-ternop-flrr-generic i x
| MOVZ x: sem-movz x
| MOVZ-fmt x: sem-default-ternop-flrr-generic i x
| MSUB x: sem-msub x
| MSUB-fmt x: sem-default-quadop-flrrr-generic i x
| MSUBU x: sem-msubu x
| MTHI x: sem-mthi x
| MTLO x: sem-mtlo x
| MUL x: sem-mul x
| MULT x: sem-mult x
| MULTU x: sem-multu x
| NMADD-fmt x: sem-default-quadop-flrrr-generic i x
| NMSUB-fmt x: sem-default-quadop-flrrr-generic i x
| PLL-PS x: sem-default-ternop-lrr-generic i x
| PLU-PS x: sem-default-ternop-lrr-generic i x
| PREFX x: sem-default-binop-rr-tuple-generic i x
| PUL-PS x: sem-default-ternop-lrr-generic i x
| PUU-PS x: sem-default-ternop-lrr-generic i x