diff options
| -rw-r--r-- | risc-v/Makefile | 9 | ||||
| -rw-r--r-- | risc-v/riscv.sail | 311 | ||||
| -rw-r--r-- | risc-v/riscv_types.sail | 165 | ||||
| -rw-r--r-- | x86/x64.sail | 73 |
4 files changed, 354 insertions, 204 deletions
diff --git a/risc-v/Makefile b/risc-v/Makefile index 856a48eb..8449c7c4 100644 --- a/risc-v/Makefile +++ b/risc-v/Makefile @@ -1,13 +1,14 @@ SAIL:=../src/sail.native -SOURCES:=riscv.sail ../etc/regfp.sail riscv_regfp.sail +SOURCES:=riscv_types.sail riscv.sail ../etc/regfp.sail riscv_regfp.sail all: lem_ast shallow lem_ast: $(SOURCES) $(SAIL) - $(SAIL) -lem_ast $(SOURCES) + $(SAIL) -lem_ast $(SOURCES) -o riscv shallow: $(SOURCES) $(SAIL) - $(SAIL) -lem_lib Riscv_extras_embed -lem $(SOURCES) + $(SAIL) -lem_lib Riscv_extras_embed -lem $(SOURCES) -o riscv clean: - rm -f riscv.lem riscv_embed*.lem + rm -f riscv.lem riscv_embed*.lem riscv_toFromInterp.lem + rm -f riscv_type*.lem diff --git a/risc-v/riscv.sail b/risc-v/riscv.sail index ea885d90..8658ae96 100644 --- a/risc-v/riscv.sail +++ b/risc-v/riscv.sail @@ -1,177 +1,11 @@ -default Order dec - -typedef regval = bit[64] -typedef regno = bit[5] - -register (regval) x0 -register (regval) x1 -register (regval) x2 -register (regval) x3 -register (regval) x4 -register (regval) x5 -register (regval) x6 -register (regval) x7 -register (regval) x8 -register (regval) x9 -register (regval) x10 -register (regval) x11 -register (regval) x12 -register (regval) x13 -register (regval) x14 -register (regval) x15 -register (regval) x16 -register (regval) x17 -register (regval) x18 -register (regval) x19 -register (regval) x20 -register (regval) x21 -register (regval) x22 -register (regval) x23 -register (regval) x24 -register (regval) x25 -register (regval) x26 -register (regval) x27 -register (regval) x28 -register (regval) x29 -register (regval) x30 -register (regval) x31 - -register (bit[64]) PC -register (bit[64]) nextPC - -let (vector <0, 32, inc, (register<(regval)>)>) GPRs = - [ x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, - x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, - x28, x29, x30, x31 - ] - -function (regval) rGPR ((regno) r) = - if (r == 0) then - 0 - else - GPRs[r] - -function unit wGPR((regno) r, (regval) v) = - if (r != 0) then - GPRs[r] := v - -function forall 'a. 'a effect { escape } not_implemented((string) message) = -{ - exit message; -} - -function unit effect { escape } check_alignment( (bit[64]) addr, (nat) width) = -{ - if (unsigned(addr) mod width != 0) then - exit "misaligned memory access"; -} - - -val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr -val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_acquire -val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_strong_acquire -val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserved -val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserved_acquire -val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserved_strong_acquire -function forall Nat 'n. (bit[8 * 'n]) effect { rmem, escape } mem_read( (bit[64]) addr, ([|'n|]) width, (bool) aq, (bool) rl, (bool) res) = -{ - if (aq | res) then - check_alignment(addr, width); - - switch (aq, rl, res) { - case (false, false, false) -> MEMr(addr, width) - case (true, false, false) -> MEMr_acquire(addr, width) - case (false, false, true) -> MEMr_reserved(addr, width) - case (true, false, true) -> MEMr_reserved_acquire(addr, width) - case (false, true, false) -> not_implemented("load.rl is not implemented") - case (true, true, false) -> MEMr_strong_acquire(addr, width) - case (false, true, true) -> not_implemented("lr.rl is not implemented") - case (true, true, true) -> MEMr_reserved_strong_acquire(addr, width) - } -} - -val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea -val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_release -val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_strong_release -val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional -val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional_release -val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional_strong_release -function forall Nat 'n. unit effect { eamem, escape } mem_write_ea( (bit[64]) addr , ([|'n|]) width, (bool) aq, (bool) rl, (bool) con) = -{ - if (rl | con) then - check_alignment(addr, width); - - switch (aq, rl, con) { - case (false, false, false) -> MEMea(addr, width) - case (false, true, false) -> MEMea_release(addr, width) - case (false, false, true) -> MEMea_conditional(addr, width) - case (false, true , true) -> MEMea_conditional_release(addr, width) - case (true, false, false) -> not_implemented("store.aq is not implemented") - case (true, true, false) -> MEMea_strong_release(addr, width) - case (true, false, true) -> not_implemented("sc.aq is not implemented") - case (true, true , true) -> MEMea_conditional_strong_release(addr, width) - } -} - -val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval -val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_release -val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_strong_release -val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_conditional -val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_conditional_release -val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_conditional_strong_release -function forall Nat 'n. unit effect { wmv, escape } mem_write_value( (bit[64]) addr , ([|'n|]) width , (bit[8*'n]) value, (bool) aq, (bool) rl, (bool) con) = -{ - if (rl | con) then - check_alignment(addr, width); - - switch (aq, rl, con) { - case (false, false, false) -> MEMval(addr, width, value) - case (false, true, false) -> MEMval_release(addr, width, value) - case (false, false, true) -> MEMval_conditional(addr, width, value) - case (false, true, true) -> MEMval_conditional_release(addr, width, value) - case (true, false, false) -> not_implemented("store.aq is not implemented") - case (true, true, false) -> MEMval_strong_release(addr, width, value) - case (true, false, true) -> not_implemented("sc.aq is not implemented") - case (true, true, true) -> MEMval_conditional_strong_release(addr, width, value) - } -} - -val extern unit -> bool effect {exmem} speculate_conditional_success - -val extern unit -> unit effect { barr } MEM_fence_rw_rw -val extern unit -> unit effect { barr } MEM_fence_r_rw -val extern unit -> unit effect { barr } MEM_fence_rw_w -val extern unit -> unit effect { barr } MEM_fence_w_w -val extern unit -> unit effect { barr } MEM_fence_i - -(* Ideally these would be sail builtin *) -function (bit[64]) shift_right_arith64 ((bit[64]) v, (bit[6]) shift) = - let (bit[128]) v128 = EXTS(v) in - (v128 >> shift)[63..0] - -function (bit[32]) shift_right_arith32 ((bit[32]) v, (bit[5]) shift) = - let (bit[64]) v64 = EXTS(v) in - (v64 >> shift)[31..0] - -typedef uop = enumerate {LUI; AUIPC} (* upper immediate ops *) -typedef bop = enumerate {BEQ; BNE; BLT; BGE; BLTU; BGEU} (* branch ops *) -typedef iop = enumerate {ADDI; SLTI; SLTIU; XORI; ORI; ANDI} (* immediate ops *) -typedef sop = enumerate {SLLI; SRLI; SRAI} (* shift ops *) -typedef rop = enumerate {ADD; SUB; SLL; SLT; SLTU; XOR; SRL; SRA; OR; AND} (* reg-reg ops *) -typedef ropw = enumerate {ADDW; SUBW; SLLW; SRLW; SRAW} (* reg-reg 32-bit ops *) -typedef amoop = enumerate {AMOSWAP; AMOADD; AMOXOR; AMOAND; AMOOR; - AMOMIN; AMOMAX; AMOMINU; AMOMAXU} (* AMO ops *) - - -typedef word_width = enumerate {BYTE; HALF; WORD; DOUBLE} - -scattered function unit execute scattered typedef ast = const union val bit[32] -> option<ast> effect pure decode - scattered function option<ast> decode +scattered function unit execute + +(********************************************************************) union ast member ((bit[20]), regno, uop) UTYPE function clause decode ((bit[20]) imm : (regno) rd : 0b0110111) = Some(UTYPE(imm, rd, LUI)) @@ -185,30 +19,44 @@ function clause execute (UTYPE(imm, rd, op)) = } in wGPR(rd, ret) +(********************************************************************) union ast member ((bit[21]), regno) JAL + function clause decode ((bit[20]) imm : (regno) rd : 0b1101111) = Some (JAL(imm[19] : imm[7..0] : imm[8] : imm[18..13] : imm[12..9] : 0b0, rd)) + function clause execute (JAL(imm, rd)) = let (bit[64]) offset = EXTS(imm) in { nextPC := PC + offset; wGPR(rd, PC + 4); } +(********************************************************************) union ast member((bit[12]), regno, regno) JALR + function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b1100111) = Some(JALR(imm, rs1, rd)) + function clause execute (JALR(imm, rs1, rd)) = let (bit[64]) newPC = rGPR(rs1) + EXTS(imm) in { nextPC := newPC[63..1] : 0b0; wGPR(rd, PC + 4); } +(********************************************************************) union ast member ((bit[13]), regno, regno, bop) BTYPE -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BEQ)) -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BNE)) -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b100 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BLT)) -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b101 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BGE)) -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b110 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BLTU)) -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b111 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BGEU)) + +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b1100011) = + Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BEQ)) +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b1100011) = + Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BNE)) +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b100 : (bit[5]) imm5 : 0b1100011) = + Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BLT)) +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b101 : (bit[5]) imm5 : 0b1100011) = + Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BGE)) +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b110 : (bit[5]) imm5 : 0b1100011) = + Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BLTU)) +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b111 : (bit[5]) imm5 : 0b1100011) = + Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BGEU)) function clause execute (BTYPE(imm, rs2, rs1, op)) = let rs1_val = rGPR(rs1) in @@ -224,13 +72,16 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) = if (taken) then nextPC := PC + EXTS(imm) +(********************************************************************) union ast member ((bit[12]), regno, regno, iop) ITYPE + function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, ADDI)) function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, SLTI)) function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, SLTIU)) function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, XORI)) function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, ORI)) function clause decode ((bit[12]) imm : (regno) rs1 : 0b111 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, ANDI)) + function clause execute (ITYPE (imm, rs1, rd, op)) = let rs1_val = rGPR(rs1) in let imm64 = (bit[64]) (EXTS(imm)) in @@ -244,10 +95,13 @@ function clause execute (ITYPE (imm, rs1, rd, op)) = } in wGPR(rd, result) +(********************************************************************) union ast member ((bit[6]), regno, regno, sop) SHIFTIOP + function clause decode (0b000000 : (bit[6]) shamt : (regno) rs1 : 0b001 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, SLLI)) function clause decode (0b000000 : (bit[6]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, SRLI)) function clause decode (0b010000 : (bit[6]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, SRAI)) + function clause execute (SHIFTIOP(shamt, rs1, rd, op)) = let rs1_val = rGPR(rs1) in let result = switch(op) { @@ -257,7 +111,9 @@ function clause execute (SHIFTIOP(shamt, rs1, rd, op)) = } in wGPR(rd, result) +(********************************************************************) union ast member (regno, regno, regno, rop) RTYPE + function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, ADD)) function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SUB)) function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b001 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SLL)) @@ -268,6 +124,7 @@ function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SRA)) function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b110 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, OR)) function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b111 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, AND)) + function clause execute (RTYPE(rs2, rs1, rd, op)) = let rs1_val = rGPR(rs1) in let rs2_val = rGPR(rs2) in @@ -285,7 +142,9 @@ function clause execute (RTYPE(rs2, rs1, rd, op)) = } in wGPR(rd, result) +(********************************************************************) union ast member ((bit[12]), regno, regno, bool, word_width, bool, bool) LOAD + function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, BYTE, false, false)) function clause decode ((bit[12]) imm : (regno) rs1 : 0b001 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, HALF, false, false)) function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, WORD, false, false)) @@ -293,6 +152,7 @@ function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b000 function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true, BYTE, false, false)) function clause decode ((bit[12]) imm : (regno) rs1 : 0b101 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true, HALF, false, false)) function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true, WORD, false, false)) + function clause execute(LOAD(imm, rs1, rd, unsigned, width, aq, rl)) = let (bit[64]) addr = rGPR(rs1) + EXTS(imm) in let (bit[64]) result = if unsigned then @@ -311,11 +171,18 @@ function clause execute(LOAD(imm, rs1, rd, unsigned, width, aq, rl)) = } in wGPR(rd, result) +(********************************************************************) union ast member ((bit[12]), regno, regno, word_width, bool, bool) STORE -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, BYTE, false, false)) -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, HALF, false, false)) -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b010 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, WORD, false, false)) -function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b011 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, DOUBLE, false, false)) + +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b0100011) = + Some(STORE(imm7 : imm5, rs2, rs1, BYTE, false, false)) +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b0100011) = + Some(STORE(imm7 : imm5, rs2, rs1, HALF, false, false)) +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b010 : (bit[5]) imm5 : 0b0100011) = + Some(STORE(imm7 : imm5, rs2, rs1, WORD, false, false)) +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b011 : (bit[5]) imm5 : 0b0100011) = + Some(STORE(imm7 : imm5, rs2, rs1, DOUBLE, false, false)) + function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = let (bit[64]) addr = rGPR(rs1) + EXTS(imm) in { switch (width) { @@ -333,18 +200,25 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = } } +(********************************************************************) union ast member ((bit[12]), regno, regno) ADDIW -function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0011011) = Some(ADDIW(imm, rs1, rd)) + +function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0011011) = + Some(ADDIW(imm, rs1, rd)) + function clause execute (ADDIW(imm, rs1, rd)) = let (bit[64]) imm64 = EXTS(imm) in let (bit[64]) result64 = imm64 + rGPR(rs1) in let (bit[64]) result32 = EXTS(result64[31..0]) in wGPR(rd, result32) +(********************************************************************) union ast member ((bit[5]), regno, regno, sop) SHIFTW + function clause decode (0b0000000 : (bit[5]) shamt : (regno) rs1 : 0b001 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, SLLI)) function clause decode (0b0000000 : (bit[5]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, SRLI)) function clause decode (0b0100000 : (bit[5]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, SRAI)) + function clause execute (SHIFTW(shamt, rs1, rd, op)) = let rs1_val = (rGPR(rs1))[31..0] in let result = switch(op) { @@ -354,12 +228,15 @@ function clause execute (SHIFTW(shamt, rs1, rd, op)) = } in wGPR(rd, EXTS(result)) +(********************************************************************) union ast member (regno, regno, regno, ropw) RTYPEW + function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, ADDW)) function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SUBW)) function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b001 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SLLW)) function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SRLW)) function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SRAW)) + function clause execute (RTYPEW(rs2, rs1, rd, op)) = let rs1_val = (rGPR(rs1))[31..0] in let rs2_val = (rGPR(rs2))[31..0] in @@ -372,8 +249,11 @@ function clause execute (RTYPEW(rs2, rs1, rd, op)) = } in wGPR(rd, EXTS(result)) +(********************************************************************) union ast member (bit[4], bit[4]) FENCE + function clause decode (0b0000 : (bit[4]) pred : (bit[4]) succ : 0b00000 : 0b000 : 0b00000 : 0b0001111) = Some(FENCE (pred, succ)) + function clause execute (FENCE(pred, succ)) = { switch(pred, succ) { case (0b0011, 0b0011) -> MEM_fence_rw_rw() @@ -384,19 +264,24 @@ function clause execute (FENCE(pred, succ)) = { } } +(********************************************************************) union ast member unit FENCEI function clause decode (0b000000000000 : 0b00000 : 0b001 : 0b00000 : 0b0001111) = Some(FENCEI) function clause execute FENCEI = MEM_fence_i() +(********************************************************************) union ast member unit ECALL function clause decode (0b000000000000 : 0b00000 : 0b000 : 0b00000 : 0b1110011) = Some(ECALL ()) function clause execute ECALL = not_implemented("ECALL is not implemented") +(********************************************************************) union ast member unit EBREAK function clause decode (0b000000000001 : 0b00000 : 0b000 : 0b00000 : 0b1110011) = Some(EBREAK ()) function clause execute EBREAK = { exit () } +(********************************************************************) union ast member (bool, bool, regno, word_width, regno) LOADRES + function clause decode (0b00010 : [aq] : [rl] : 0b00000 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(LOADRES(aq, rl, rs1, WORD, rd)) function clause decode (0b00010 : [aq] : [rl] : 0b00000 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(LOADRES(aq, rl, rs1, DOUBLE, rd)) function clause execute(LOADRES(aq, rl, rs1, width, rd)) = @@ -408,9 +293,14 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = } in wGPR(rd, result) +(********************************************************************) union ast member (bool, bool, regno, regno, word_width, regno) STORECON -function clause decode (0b00011 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(STORECON(aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b00011 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(STORECON(aq, rl, rs2, rs1, DOUBLE, rd)) + +function clause decode (0b00011 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = + Some(STORECON(aq, rl, rs2, rs1, WORD, rd)) +function clause decode (0b00011 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = + Some(STORECON(aq, rl, rs2, rs1, DOUBLE, rd)) + function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { (*(bit)*) status := if speculate_conditional_success() then 0 else 1; wGPR(rd) := (bit[64]) (EXTZ([status])); @@ -429,26 +319,45 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { }; } +(********************************************************************) union ast member (amoop, bool, bool, regno, regno, word_width, regno) AMO -function clause decode (0b00001 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOSWAP, aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b00001 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOSWAP, aq, rl, rs2, rs1, DOUBLE, rd)) -function clause decode (0b00000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOADD , aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b00000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOADD , aq, rl, rs2, rs1, DOUBLE, rd)) -function clause decode (0b00100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOXOR , aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b00100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOXOR , aq, rl, rs2, rs1, DOUBLE, rd)) -function clause decode (0b01100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOAND , aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b01100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOAND , aq, rl, rs2, rs1, DOUBLE, rd)) -function clause decode (0b01000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOOR , aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b01000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOOR , aq, rl, rs2, rs1, DOUBLE, rd)) -function clause decode (0b10000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOMIN , aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b10000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOMIN , aq, rl, rs2, rs1, DOUBLE, rd)) -function clause decode (0b10100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOMAX , aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b10100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOMAX , aq, rl, rs2, rs1, DOUBLE, rd)) -function clause decode (0b11000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOMINU, aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b11000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOMINU, aq, rl, rs2, rs1, DOUBLE, rd)) -function clause decode (0b11100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOMAXU, aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b11100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOMAXU, aq, rl, rs2, rs1, DOUBLE, rd)) +function clause decode (0b00001 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = + Some(AMO(AMOSWAP, aq, rl, rs2, rs1, WORD, rd)) +function clause decode (0b00001 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = + Some(AMO(AMOSWAP, aq, rl, rs2, rs1, DOUBLE, rd)) +function clause decode (0b00000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = + Some(AMO(AMOADD , aq, rl, rs2, rs1, WORD, rd)) +function clause decode (0b00000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = + Some(AMO(AMOADD , aq, rl, rs2, rs1, DOUBLE, rd)) +function clause decode (0b00100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = + Some(AMO(AMOXOR , aq, rl, rs2, rs1, WORD, rd)) +function clause decode (0b00100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = + Some(AMO(AMOXOR , aq, rl, rs2, rs1, DOUBLE, rd)) +function clause decode (0b01100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = + Some(AMO(AMOAND , aq, rl, rs2, rs1, WORD, rd)) +function clause decode (0b01100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = + Some(AMO(AMOAND , aq, rl, rs2, rs1, DOUBLE, rd)) +function clause decode (0b01000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = + Some(AMO(AMOOR , aq, rl, rs2, rs1, WORD, rd)) +function clause decode (0b01000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = + Some(AMO(AMOOR , aq, rl, rs2, rs1, DOUBLE, rd)) +function clause decode (0b10000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = + Some(AMO(AMOMIN , aq, rl, rs2, rs1, WORD, rd)) +function clause decode (0b10000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = + Some(AMO(AMOMIN , aq, rl, rs2, rs1, DOUBLE, rd)) +function clause decode (0b10100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = + Some(AMO(AMOMAX , aq, rl, rs2, rs1, WORD, rd)) +function clause decode (0b10100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = + Some(AMO(AMOMAX , aq, rl, rs2, rs1, DOUBLE, rd)) +function clause decode (0b11000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = + Some(AMO(AMOMINU, aq, rl, rs2, rs1, WORD, rd)) +function clause decode (0b11000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = + Some(AMO(AMOMINU, aq, rl, rs2, rs1, DOUBLE, rd)) +function clause decode (0b11100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = + Some(AMO(AMOMAXU, aq, rl, rs2, rs1, WORD, rd)) +function clause decode (0b11100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = + Some(AMO(AMOMAXU, aq, rl, rs2, rs1, DOUBLE, rd)) function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { (bit[64]) addr := rGPR(rs1); @@ -486,6 +395,8 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { }; } +(********************************************************************) + function clause decode _ = None end ast diff --git a/risc-v/riscv_types.sail b/risc-v/riscv_types.sail new file mode 100644 index 00000000..a11d5561 --- /dev/null +++ b/risc-v/riscv_types.sail @@ -0,0 +1,165 @@ +default Order dec + +function forall 'a. 'a effect { escape } not_implemented((string) message) = + exit message + +typedef regval = bit[64] +typedef regno = bit[5] + +(* register (regval) x0 is hard-wired zero *) +register (regval) x1 +register (regval) x2 +register (regval) x3 +register (regval) x4 +register (regval) x5 +register (regval) x6 +register (regval) x7 +register (regval) x8 +register (regval) x9 +register (regval) x10 +register (regval) x11 +register (regval) x12 +register (regval) x13 +register (regval) x14 +register (regval) x15 +register (regval) x16 +register (regval) x17 +register (regval) x18 +register (regval) x19 +register (regval) x20 +register (regval) x21 +register (regval) x22 +register (regval) x23 +register (regval) x24 +register (regval) x25 +register (regval) x26 +register (regval) x27 +register (regval) x28 +register (regval) x29 +register (regval) x30 +register (regval) x31 + +register (bit[64]) PC +register (bit[64]) nextPC + +let (vector <1, 31, inc, (register<(regval)>)>) GPRs = + [ (* x0, *) x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, + x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, + x28, x29, x30, x31 + ] + +function (regval) rGPR ((regno) r) = + if (r == 0) then + 0 + else + GPRs[r] + +function unit wGPR((regno) r, (regval) v) = + if (r != 0) then + GPRs[r] := v + +function unit effect { escape } check_alignment( (bit[64]) addr, (nat) width) = + if (unsigned(addr) mod width != 0) then + exit "misaligned memory access" + +val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr +val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_acquire +val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_strong_acquire +val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserved +val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserved_acquire +val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserved_strong_acquire + +function forall Nat 'n. (bit[8 * 'n]) effect { rmem, escape } mem_read( (bit[64]) addr, ([|'n|]) width, (bool) aq, (bool) rl, (bool) res) = +{ + if (aq | res) then + check_alignment(addr, width); + + switch (aq, rl, res) { + case (false, false, false) -> MEMr(addr, width) + case (true, false, false) -> MEMr_acquire(addr, width) + case (false, false, true) -> MEMr_reserved(addr, width) + case (true, false, true) -> MEMr_reserved_acquire(addr, width) + case (false, true, false) -> not_implemented("load.rl is not implemented") + case (true, true, false) -> MEMr_strong_acquire(addr, width) + case (false, true, true) -> not_implemented("lr.rl is not implemented") + case (true, true, true) -> MEMr_reserved_strong_acquire(addr, width) + } +} + +val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea +val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_release +val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_strong_release +val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional +val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional_release +val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional_strong_release + +function forall Nat 'n. unit effect { eamem, escape } mem_write_ea( (bit[64]) addr , ([|'n|]) width, (bool) aq, (bool) rl, (bool) con) = +{ + if (rl | con) then + check_alignment(addr, width); + + switch (aq, rl, con) { + case (false, false, false) -> MEMea(addr, width) + case (false, true, false) -> MEMea_release(addr, width) + case (false, false, true) -> MEMea_conditional(addr, width) + case (false, true , true) -> MEMea_conditional_release(addr, width) + case (true, false, false) -> not_implemented("store.aq is not implemented") + case (true, true, false) -> MEMea_strong_release(addr, width) + case (true, false, true) -> not_implemented("sc.aq is not implemented") + case (true, true , true) -> MEMea_conditional_strong_release(addr, width) + } +} + +val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval +val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_release +val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_strong_release +val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_conditional +val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_conditional_release +val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_conditional_strong_release + +function forall Nat 'n. unit effect { wmv, escape } mem_write_value( (bit[64]) addr , ([|'n|]) width , (bit[8*'n]) value, (bool) aq, (bool) rl, (bool) con) = +{ + if (rl | con) then + check_alignment(addr, width); + + switch (aq, rl, con) { + case (false, false, false) -> MEMval(addr, width, value) + case (false, true, false) -> MEMval_release(addr, width, value) + case (false, false, true) -> MEMval_conditional(addr, width, value) + case (false, true, true) -> MEMval_conditional_release(addr, width, value) + case (true, false, false) -> not_implemented("store.aq is not implemented") + case (true, true, false) -> MEMval_strong_release(addr, width, value) + case (true, false, true) -> not_implemented("sc.aq is not implemented") + case (true, true, true) -> MEMval_conditional_strong_release(addr, width, value) + } +} + +val extern unit -> bool effect {exmem} speculate_conditional_success + +val extern unit -> unit effect { barr } MEM_fence_rw_rw +val extern unit -> unit effect { barr } MEM_fence_r_rw +val extern unit -> unit effect { barr } MEM_fence_rw_w +val extern unit -> unit effect { barr } MEM_fence_w_w +val extern unit -> unit effect { barr } MEM_fence_i + +typedef uop = enumerate {LUI; AUIPC} (* upper immediate ops *) +typedef bop = enumerate {BEQ; BNE; BLT; BGE; BLTU; BGEU} (* branch ops *) +typedef iop = enumerate {ADDI; SLTI; SLTIU; XORI; ORI; ANDI} (* immediate ops *) +typedef sop = enumerate {SLLI; SRLI; SRAI} (* shift ops *) +typedef rop = enumerate {ADD; SUB; SLL; SLT; SLTU; XOR; SRL; SRA; OR; AND} (* reg-reg ops *) +typedef ropw = enumerate {ADDW; SUBW; SLLW; SRLW; SRAW} (* reg-reg 32-bit ops *) +typedef amoop = enumerate {AMOSWAP; AMOADD; AMOXOR; AMOAND; AMOOR; + AMOMIN; AMOMAX; AMOMINU; AMOMAXU} (* AMO ops *) + +typedef word_width = enumerate {BYTE; HALF; WORD; DOUBLE} + +(********************************************************************) + +(* Ideally these would be sail builtin *) +function (bit[64]) shift_right_arith64 ((bit[64]) v, (bit[6]) shift) = + let (bit[128]) v128 = EXTS(v) in + (v128 >> shift)[63..0] + +function (bit[32]) shift_right_arith32 ((bit[32]) v, (bit[5]) shift) = + let (bit[64]) v64 = EXTS(v) in + (v64 >> shift)[31..0] diff --git a/x86/x64.sail b/x86/x64.sail index dfa92fd3..ae867747 100644 --- a/x86/x64.sail +++ b/x86/x64.sail @@ -130,6 +130,14 @@ typedef wsize = const union { unit Sz64; } +function ([|8:64|]) size_to_int((wsize) s) = + switch(s) { + case (Sz8(_)) -> 8 + case Sz16 -> 16 + case Sz32 -> 32 + case Sz64 -> 64 + } + typedef base = const union { unit NoBase; unit RipBase; @@ -154,12 +162,19 @@ typedef imm_rm = const union { qword Imm; } +typedef bit_offset = const union { + (rm, qword) Bit_rm_imm; + (rm, regn) Bit_rm_r; +} + typedef monop_name = enumerate { Dec; Inc; Not; Neg } typedef binop_name = enumerate { Add; Or; Adc; Sbb; And; Sub; Xor; Cmp; Rol; Ror; Rcl; Rcr; Shl; Shr; Test; Sar } +typedef bitop_name = enumerate { Bts; Btc; Btr } + function binop_name opc_to_binop_name ((bit[4]) opc) = switch opc { @@ -319,6 +334,24 @@ function qword get_ea_address ((ea) e) = function unit jump_to_ea ((ea) e) = RIP := call_dest_from_ea(e) +function (ea, nat) bit_offset_ea ((wsize) sz, (bit_offset) bo) = + let s = size_to_int (sz) in + switch bo { + case (Bit_rm_imm (r_m, imm)) -> + let base_ea = ea_rm (sz, r_m) in + switch (base_ea) { + case (Ea_r(_, r)) -> (Ea_r(sz, r), imm mod s) + case (Ea_m(_, a)) -> (Ea_m(sz, a), imm mod s) + } + case (Bit_rm_r (r_m, r)) -> + let base_ea = ea_rm (sz, r_m) in + let offset = REG[r] in + switch (base_ea) { + case (Ea_r(_, r)) -> (Ea_r(sz, r), offset mod s) + case (Ea_m(_, a)) -> (Ea_m(Sz64, a + (offset div 8)), offset mod 64) + } + } + (* EFLAG updates *) function bit byte_parity ((byte) b) = @@ -585,6 +618,25 @@ function clause execute (Binop (locked,bop,sz,ds)) = write_binop (locked, sz, bop, val_dst, val_src, e) (* ========================================================================== + Bitop + ========================================================================== *) + +union ast member (bool,bitop_name,wsize,bit_offset) Bitop + +function clause execute (Bitop (locked,bop,sz,boffset)) = + let (base_ea, offset) = bit_offset_ea (sz, boffset) in { + word := EA(locked, base_ea); + bitval := word[offset]; + word[offset] := switch(bop) { + case Bts -> bitone + case Btc -> (~ (bitval)) + case Btr -> bitzero + }; + CF := bitval; + wEA(locked, base_ea) := word; + } + +(* ========================================================================== CALL ========================================================================== *) @@ -1376,6 +1428,27 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ( aR := append(aRs, aR); } } + case(Bitop (locked, bitop, sz, bitoff)) -> { + let rk = if locked then Read_X86_locked else Read_plain in + let wk = if locked then Write_X86_locked else Write_plain in + let (ik', iRs, oRs, aRs) = switch(bitoff) { + case (Bit_rm_imm (r_m, imm)) -> + let (m, rs, ars) = regfp_rm(r_m) in + (if m then IK_mem_rmw(rk, wk) else IK_simple, + append(rs, ars), rs, ars) + case (Bit_rm_r (r_m, r)) -> + let rfp = RFull(GPRstr[r]) in + let (m, rs, ars) = regfp_rm(r_m) in + (if m then IK_mem_rmw(rk, wk) else IK_simple, + rfp::append(rs, ars), rs, + if m then (rfp::ars) else ars) (* in memory case r is a third input to address! *) + } in { + ik := ik'; + iR := append(iRs, iR); + oR := RFull("CF")::append(oRs, oR); + aR := append(aRs, aR); + } + } case(CALL (irm) ) -> let (m, rs, ars) = regfp_imm_rm (irm) in { iK := if m then IK_mem_rmw(Read_plain, Write_plain) else IK_mem_write(Write_plain); |