diff --git a/lib_test/x86/run_x86_tests.ml b/lib_test/x86/run_x86_tests.ml index 45fd03e4f..c1cff0f7f 100644 --- a/lib_test/x86/run_x86_tests.ml +++ b/lib_test/x86/run_x86_tests.ml @@ -4,6 +4,7 @@ open Bap_plugins.Std let suite = "X86" >::: [ Test_pshufb.suite; + Test_pcmp.suite; ] let load_plugins () = diff --git a/lib_test/x86/test_pcmp.ml b/lib_test/x86/test_pcmp.ml new file mode 100644 index 000000000..ad8cb3db7 --- /dev/null +++ b/lib_test/x86/test_pcmp.ml @@ -0,0 +1,216 @@ + +(** +# rappel (don't forget -x option) + + +## pcmpeqb, pcmpgtb, pcmpeqw, pcmpgtw ... instructions + +move to xmm0 register a 128-bit value "0f 0e 0d 0c 0b 0a 09 08 07 06 05 04 03 02 01 00" +move to xmm1 register a 128-bit value "0f 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00" + + mov rax, 0x0706050403020100 + mov rbx, 0x0f0e0d0c0b0a0908 + pinsrq xmm0, rax, 0 + pinsrq xmm0, rbx, 1 + + mov rax, 0x0000000000000000 + mov rbx, 0x0f00000000000000 + pinsrq xmm1, rax, 0 + pinsrq xmm1, rbx, 1 + +Cases: + 1) pcmpeqb xmm1, xmm0 + expected: first and last bytes in xmm1 should be 0xFF + + 2) pcmpgtb xmm1, xmm0 + expected: first and last bytes in xmm1 should be 0x00, + all others bytes should be 0xFF + +## pminsb, pminub, pmaxsb, pmaxub, pminsw ... instructions + +move to xmm0 register a 128-bit value "0f 0e 0d 0c 0b 0a 09 08 07 06 05 04 03 02 01 00" +move to xmm1 register a 128-bit value "ff 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ff" + + mov rax, 0x0706050403020100 + mov rbx, 0x0f0e0d0c0b0a0908 + pinsrq xmm0, rax, 0 + pinsrq xmm0, rbx, 1 + + mov rax, 0x00000000000000ff + mov rbx, 0xff00000000000000 + pinsrq xmm1, rax, 0 + pinsrq xmm1, rbx, 1 + +Cases: + 1) pminub xmm1, xmm0 + expected: first byte in xmm1 should be 0x0f + 2) pminsb xmm1, xmm0 + expected: xmm1 stay unchanged + 3) pmaxub xmm1, xmm0 + expected: all bytes in xmm1 should be equal + to corresponded bytes in xmm0, except first and last + bytes, which stay unchanchged + 4) pmaxsb xmm1, xmm0 + expected: xmm1 = xmm0 + +*) + +open Core_kernel.Std +open Bap.Std +open OUnit2 + +module Dis = Disasm_expert.Basic +module Env = X86_env.R32 + +let arch = `x86 +let width = 32 + +let of_bytes s = + let str = String.filter ~f:(fun c -> Char.(c <> ' ')) s in + Word.of_string @@ sprintf "0x%s:256u" str + +let insn_bil x = + let bytes = Bigstring.of_string x in + let mem = Or_error.ok_exn @@ + Memory.create LittleEndian (Word.zero 32) bytes in + let mem, insn = + Or_error.ok_exn @@ + Dis.with_disasm ~backend:"llvm" (Arch.to_string arch) ~f:(fun dis -> + let dis = Dis.store_asm dis |> Dis.store_kinds in + match Dis.insn_of_mem dis mem with + | Ok (mem', Some insn, `finished) -> Ok (mem', insn) + | _ -> Error (Error.of_string "invalid insn")) in + let module T = (val (target_of_arch arch)) in + Or_error.ok_exn @@ T.lift mem insn + +let test insn_name bytes x y ~expected _ctxt = + let xmm0 = Env.ymms.(0) in + let xmm1 = Env.ymms.(1) in + let bil = Bil.[ + move xmm0 (int x); + move xmm1 (int y); + ] @ insn_bil bytes in + let c = Stmt.eval bil (new Bili.context) in + assert_bool ("got wrong result for " ^ insn_name) @@ + match c#lookup xmm1 with + | None -> false + | Some r -> + match Bil.Result.value r with + | Bil.Imm word -> + if not (Word.equal word expected) then + printf "%s: got %s, expected %s\n" + insn_name (Word.to_string word) (Word.to_string expected); + Word.equal word expected + | _ -> false + +let test_eqb = + let pcmpeqb = "\x66\x0f\x74\xc8" in (** pcmpeqb %xmm1, %xmm0 *) + let x = of_bytes "0f 0e 0d 0c 0b 0a 09 08 07 06 05 04 03 02 01 00" in + let y = of_bytes "0f 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00" in + let e = of_bytes "ff 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ff" in + test "pcmpeqb" pcmpeqb x y ~expected:e + +let test_gtb = + let pcmpgtb = "\x66\x0f\x64\xc8" in (** pcmpgtb %xmm1, %xmm0 *) + let x = of_bytes "0f 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00" in + let y = of_bytes "0f 0e 0d 0c 0b 0a 09 08 07 06 05 04 03 02 01 00" in + let e = of_bytes "00 ff ff ff ff ff ff ff ff ff ff ff ff ff ff 00" in + test "pcmpgtb" pcmpgtb x y ~expected:e + +let test_pmin_pmax name bytes expected = + let x = of_bytes "0f 0e 0d 0c 0b 0a 09 08 07 06 05 04 03 02 01 00" in + let y = of_bytes "ff 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ff" in + test name bytes x y ~expected + +let test_pminub = + let bytes = "\x66\x0f\xda\xc8" in (** pminub %xmm0, %xmm1 *) + let expected = of_bytes "0f 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00" in + test_pmin_pmax "pminub" bytes expected + +let test_pminsb = + let bytes = "\x66\x0f\x38\x38\xc8" in (** pminsb %xmm0, %xmm1 *) + let expected = of_bytes "ff 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ff" in + test_pmin_pmax "pminsb" bytes expected + +let test_pmaxub = + let bytes = "\x66\x0f\xde\xc8" in (** pmaxub %xmm0, %xmm1 *) + let expected = of_bytes "ff 0e 0d 0c 0b 0a 09 08 07 06 05 04 03 02 01 ff" in + test_pmin_pmax "pmaxub" bytes expected + +let test_pmaxsb = + let bytes = "\x66\x0f\x38\x3c\xc8" in (** pmaxsb %xmm0, %xmm1 *) + let expected = of_bytes "0f 0e 0d 0c 0b 0a 09 08 07 06 05 04 03 02 01 00" in + test_pmin_pmax "pmaxsb" bytes expected + +let test_pmaxuw = + let bytes = "\x66\x0f\x38\x3e\xc8" in (** pmaxuw %xmm0, %xmm1 *) + let x = of_bytes "8f 0e 00 00 0b 0a 09 08 05 06 05 04 03 04 01 00" in + let y = of_bytes "0f 00 0d 0c 00 00 00 00 07 06 05 05 03 02 00 00" in + let z = of_bytes "8f 0e 0d 0c 0b 0a 09 08 07 06 05 05 03 04 01 00" in + test "pmaxuw" bytes x y ~expected:z + +let test_pmaxsw = + let bytes = "\x66\x0f\xee\xc8" in (** pmaxsw %xmm0, %xmm1 *) + let x = of_bytes "8f 0e 00 00 0b 0a 09 08 05 06 05 04 03 04 01 00" in + let y = of_bytes "0f 00 0d 0c 00 00 00 00 07 06 05 05 03 02 00 00" in + let z = of_bytes "0f 00 0d 0c 0b 0a 09 08 07 06 05 05 03 04 01 00" in + test "pmaxsw" bytes x y ~expected:z + +let test_pminuw = + let bytes = "\x66\x0f\x38\x3a\xc8" in (** pminuw %xmm0, %xmm1 *) + let x = of_bytes "8f 0e 00 00 0b 0a 09 08 05 06 05 04 03 04 01 00" in + let y = of_bytes "0f 00 0d 0c 00 00 00 00 07 06 05 05 03 02 00 00" in + let z = of_bytes "0f 00 00 00 00 00 00 00 05 06 05 04 03 02 00 00" in + test "pminuw" bytes x y ~expected:z + +let test_pminsw = + let bytes = "\x66\x0f\xea\xc8" in (** pminsw %xmm0, %xmm1 *) + let x = of_bytes "8f 0e 00 00 0b 0a 09 08 05 06 05 04 03 04 01 00" in + let y = of_bytes "0f 00 0d 0c 00 00 00 00 07 06 05 05 03 02 00 00" in + let z = of_bytes "8f 0e 00 00 00 00 00 00 05 06 05 04 03 02 00 00" in + test "pminsw" bytes x y ~expected:z + +let test_pminud = + let bytes = "\x66\x0f\x38\x3b\xc8" in (** pminud %xmm0, %xmm1 *) + let x = of_bytes "8f 0e 00 00 0b 0a 09 08 05 06 05 04 03 04 01 00" in + let y = of_bytes "0f 00 0d 0c 00 00 00 00 07 06 05 05 03 02 00 00" in + let z = of_bytes "0f 00 0d 0c 00 00 00 00 05 06 05 04 03 02 00 00" in + test "pminud" bytes x y ~expected:z + +let test_pminsd = + let bytes = "\x66\x0f\x38\x39\xc8" in (** pminsd %xmm0, %xmm1 *) + let x = of_bytes "8f 0e 00 00 0b 0a 09 08 05 06 05 04 03 04 01 00" in + let y = of_bytes "0f 00 0d 0c 00 00 00 00 07 06 05 05 03 02 00 00" in + let z = of_bytes "8f 0e 00 00 00 00 00 00 05 06 05 04 03 02 00 00" in + test "pminsd" bytes x y ~expected:z + +let test_pmaxud = + let bytes = "\x66\x0f\x38\x3f\xc8" in (** pmaxud %xmm0, %xmm1 *) + let x = of_bytes "8f 0e 00 00 0b 0a 09 08 05 06 05 04 03 04 01 00" in + let y = of_bytes "0f 00 0d 0c 00 00 00 00 07 06 05 05 03 02 00 00" in + let z = of_bytes "8f 0e 00 00 0b 0a 09 08 07 06 05 05 03 04 01 00" in + test "pmaxud" bytes x y ~expected:z + +let test_pmaxsd = + let bytes = "\x66\x0f\x38\x3d\xc8" in (** pmaxsd %xmm0, %xmm1 *) + let x = of_bytes "8f 0e 00 00 0b 0a 09 08 05 06 05 04 03 04 01 00" in + let y = of_bytes "0f 00 0d 0c 00 00 00 00 07 06 05 05 03 02 00 00" in + let z = of_bytes "0f 00 0d 0c 0b 0a 09 08 07 06 05 05 03 04 01 00" in + test "pmaxsd" bytes x y ~expected:z + +let suite = "pcmp" >::: [ + "pcmpeqb" >:: test_eqb; + "pcmpgtb" >:: test_gtb; + "pminub" >:: test_pminub; + "pminsb" >:: test_pminsb; + "pmaxub" >:: test_pmaxub; + "pmaxsb" >:: test_pmaxsb; + "pminuw" >:: test_pminuw; + "pminsw" >:: test_pminsw; + "pmaxuw" >:: test_pmaxuw; + "pmaxsw" >:: test_pmaxsw; + "pminud" >:: test_pminud; + "pminsd" >:: test_pminsd; + "pmaxud" >:: test_pmaxud; + "pmaxsd" >:: test_pmaxsd; + ] diff --git a/oasis/x86 b/oasis/x86 index 9ba053498..1c07ce1c5 100644 --- a/oasis/x86 +++ b/oasis/x86 @@ -61,7 +61,7 @@ Library x86_test CompiledObject: best BuildDepends: bap, oUnit, bap-x86-cpu Install: false - Modules: Test_pshufb + Modules: Test_pshufb, Test_pcmp Executable run_x86_tests Path: lib_test/x86 diff --git a/plugins/x86/x86_disasm.ml b/plugins/x86/x86_disasm.ml index 21a222a08..21d30f78f 100644 --- a/plugins/x86/x86_disasm.ml +++ b/plugins/x86/x86_disasm.ml @@ -919,20 +919,30 @@ let parse_instr mode mem addr = | 0x37 when prefix.opsize_override -> let r, rm, rv, na = parse_modrm_vec None na in (Pcmp(prefix.mopsize, Type.imm 64, Bil.SLT, "pcmpgt", r, rm, rv), na) - | 0x38 | 0x39 when prefix.opsize_override -> + | 0x38 when prefix.opsize_override -> let r, rm, rv, na = parse_modrm_vec None na in - let et = match b3 with - | 0x38 -> Type.imm 8 | 0x39 -> Type.imm 32 - | _ -> disfailwith "invalid" - in - (Ppackedbinop(prefix.mopsize, et, min_symbolic ~is_signed:true, "pmins", r, rm, rv), na) - | 0x3a | 0x3b when prefix.opsize_override -> + Ppackedbinop(prefix.mopsize, Type.imm 8, min_symbolic ~is_signed:true, "pminsb", r, rm, rv), na + | 0x39 when prefix.opsize_override -> let r, rm, rv, na = parse_modrm_vec None na in - let et = match b3 with - | 0x3a -> Type.imm 16 | 0x3b -> Type.imm 32 - | _ -> disfailwith "invalid" - in - (Ppackedbinop(prefix.mopsize, et, min_symbolic ~is_signed:false, "pminu", r, rm, rv), na) + Ppackedbinop(prefix.mopsize, Type.imm 32, min_symbolic ~is_signed:true, "pminsd", r, rm, rv), na + | 0x3a when prefix.opsize_override -> + let r, rm, rv, na = parse_modrm_vec None na in + Ppackedbinop(prefix.mopsize, Type.imm 16, min_symbolic ~is_signed:false, "pminuw", r, rm, rv), na + | 0x3b when prefix.opsize_override -> + let r, rm, rv, na = parse_modrm_vec None na in + Ppackedbinop(prefix.mopsize, Type.imm 32, min_symbolic ~is_signed:false, "pminud", r, rm, rv), na + | 0x3c when prefix.opsize_override -> + let r, rm, rv, na = parse_modrm_vec None na in + Ppackedbinop(prefix.mopsize, Type.imm 8, max_symbolic ~is_signed:true, "pmaxsb", r, rm, rv), na + | 0x3d when prefix.opsize_override -> + let r, rm, rv, na = parse_modrm_vec None na in + Ppackedbinop(prefix.mopsize, Type.imm 32, max_symbolic ~is_signed:true, "pmaxsd", r, rm, rv), na + | 0x3e when prefix.opsize_override -> + let r, rm, rv, na = parse_modrm_vec None na in + Ppackedbinop(prefix.mopsize, Type.imm 16, max_symbolic ~is_signed:false, "pmaxuw", r, rm, rv), na + | 0x3f when prefix.opsize_override -> + let r, rm, rv, na = parse_modrm_vec None na in + Ppackedbinop(prefix.mopsize, Type.imm 32, max_symbolic ~is_signed:false, "pmaxud", r, rm, rv), na | _ -> disfailwith (Printf.sprintf "opcode unsupported: 0f 38 %02x" b3)) | 0x3a -> let b3 = Char.to_int (g na) and na = s na in @@ -1137,10 +1147,13 @@ let parse_instr mode mem addr = (Ppackedbinop(prefix.mopsize, et, average, "pavg", r, rm, rv), na) | 0xea -> let r, rm, rv, na = parse_modrm_vec None na in - (Ppackedbinop(prefix.mopsize, Type.imm 16, min_symbolic ~is_signed:true, "pmins", r, rm, rv), na) + (Ppackedbinop(prefix.mopsize, Type.imm 16, min_symbolic ~is_signed:true, "pminsw", r, rm, rv), na) | 0xeb -> let r, rm, rv, na = parse_modrm_vec None na in (Pbinop(prefix.mopsize, Bil.(lor), "por", r, rm, rv), na) + | 0xee -> + let r, rm, rv, na = parse_modrm_vec None na in + (Ppackedbinop(prefix.mopsize, Type.imm 16, max_symbolic ~is_signed:true, "pmaxsw", r, rm, rv), na) | 0xef -> let r, rm, rv, na = parse_modrm_vec None na in (Pbinop(prefix.mopsize, Bil.(lxor), "pxor", r, rm, rv), na) diff --git a/plugins/x86/x86_lifter.ml b/plugins/x86/x86_lifter.ml index 2412ec972..4aebcc250 100644 --- a/plugins/x86/x86_lifter.ml +++ b/plugins/x86/x86_lifter.ml @@ -446,56 +446,84 @@ module ToIR = struct Bil.Move (dt, de); assn t dest e] | Ppackedbinop(t, et, fbop, _, d, s, vs) -> - let nelem = match t, et with - | Type.Imm n, Type.Imm n' -> n / n' - | _ -> disfailwith "invalid" - in + let t_width = bitwidth_of_type t in + let e_width = bitwidth_of_type et in + let nops = t_width / e_width in + let byte = 8 in + let tmp_dst = tmp t in + let vdst = Option.value ~default:d vs in + let iv = tmp (Type.imm byte) in + let elt = tmp et in + let zero = Word.zero t_width in + let bits = Word.of_int ~width:byte e_width in + + let foreach_size f = List.concat @@ List.init nops ~f in let getelement o i = (* assumption: immediate operands are repeated for all vector elements *) match o with | Oimm _ -> op2e et o - | _ -> extract_element !!et (op2e t o) i - in - let f i = - fbop (getelement d i) (getelement s i) - in - let e = concat_explist (List.map ~f:f (List.range ~stride:(-1) ~stop:`inclusive (nelem-1) 0)) in - (match vs with - | None -> [assn t d e] - | Some vdst -> [assn t vdst e]) + | _ -> extract_element !!et (op2e t o) i in + + List.concat Bil.[ + [tmp_dst := int zero]; + foreach_size (fun i -> [ + elt := fbop (getelement d i) (getelement s i); + iv := int @@ Word.of_int ~width:byte i; + tmp_dst := + var tmp_dst lor + ((cast unsigned t_width (var elt)) lsl (var iv * int bits)) + ] + ); + [assn t vdst (var tmp_dst)] + ] | Pbinop(t, fbop, _s, o1, o2, vop) -> (match vop with | None -> [assn t o1 (fbop (op2e t o1) (op2e t o2))] | Some vop -> [assn t o1 (fbop (op2e t vop) (op2e t o2))]) | Pcmp (t,elet,bop,_,dst,src,vsrc) -> - let elebits = !!elet in - let ncmps = !!t / elebits in + let elebits = bitwidth_of_type elet in + let t_width = bitwidth_of_type t in + let ncmps = t_width / elebits in let src = match src with | Ovec _ -> op2e t src | Oaddr a -> load (size_of_typ t) a - | Oreg _ | Oimm _ | Oseg _ -> disfailwith "invalid" - in - let dst, vsrc = match vsrc with - | None -> dst, dst - | Some vsrc -> dst, vsrc - in - let compare_region i = - let byte1 = Bil.Extract(i*elebits-1, (i-1)*elebits, src) in - let byte2 = Bil.Extract(i*elebits-1, (i-1)*elebits, op2e t vsrc) in - let tmp = tmp ~name:("t" ^ string_of_int i) elet in - let ltw n t = (BV.of_int64 n ~width:t) |> Bil.int in - Bil.Var tmp, Bil.Move (tmp, Bil.(Ite (BinOp (bop, byte1, byte2), ltw (-1L) !!elet, ltw 0L !!elet))) - in - let indices = List.init ~f:(fun i -> i + 1) ncmps in (* list 1-nbytes *) - let comparisons = List.map ~f:compare_region indices in - let temps, cmps = List.unzip comparisons in - begin match List.rev temps with - | [] -> disfailwith "Pcmp element size mismatch" (* XXX what's actually going on in Pcmp? *) - | t_first::t_rest -> - (* could also be done with shifts *) - let store_back = List.fold_left ~f:(fun acc i -> Bil.Concat(acc,i)) ~init:t_first t_rest in - cmps @ [assn t dst store_back] end + | Oreg _ | Oimm _ | Oseg _ -> disfailwith "invalid" in + let vsrc = Option.value ~default:dst vsrc in + let byte = 8 in + let tmp_dst = tmp t in + let iv = tmp (Type.imm byte) in + let elt = tmp elet in + let elt_1 = tmp elet in + let elt_2 = tmp elet in + let _one = Word.of_int ~width:elebits (-1) in + let zero = Word.zero elebits in + let bits = Word.of_int ~width:byte elebits in + let zero_long = Word.zero t_width in + let foreach_size f = + let sizes = List.init ncmps ~f:(fun i -> + let left_bit = i * elebits in + let right_bit = (i + 1) * elebits - 1 in + let i = Word.of_int ~width:byte i in + i, left_bit, right_bit) in + List.concat @@ List.map sizes ~f in + + List.concat Bil.[ + [tmp_dst := int zero_long]; + foreach_size (fun (i, left_bit, right_bit) -> [ + elt_1 := extract right_bit left_bit src; + elt_2 := extract right_bit left_bit (op2e t vsrc); + iv := int i; + if_ (binop bop (var elt_1) (var elt_2)) [ + elt := int _one; + ] [ + elt := int zero; + ]; + tmp_dst := + var tmp_dst lor + ((cast unsigned t_width (var elt)) lsl (var iv * int bits)) + ]); + [assn t dst (var tmp_dst)] ] | Pmov (t, dstet, srcet, dst, src, ext, _) -> let nelem = match t, dstet with | Type.Imm n, Type.Imm n' -> n / n' @@ -553,6 +581,15 @@ module ToIR = struct | None -> [assn t dst result] | Some vdst -> [assn t vdst result]) | Pcmpstr(t,xmm1,xmm2m128,_imm,imm8cb,pcmpinfo) -> + let open Pcmpstr in + let concat elt_width exps = match exps with + | [] -> disfailwith "trying concat on empty list" + | first :: exps' -> + let len = List.length exps * elt_width in + let exp = List.fold exps' ~init:first ~f:(fun e e' -> Bil.(e ^ e')) in + let tmp = tmp (Type.imm len) in + tmp, Bil.[tmp := exp] in + (* All bytes and bits are numbered with zero being the least significant. This includes strings! *) (* NOTE: Strings are backwards, at least when they are in @@ -563,40 +600,50 @@ module ToIR = struct let xmm2m128_e = op2e t xmm2m128 in let regm = type_of_mode mode in - let open Pcmpstr in - let nelem, _nbits, elemt = match imm8cb with - | {ssize=Bytes; _} -> 16, 8, Type.imm 8 - | {ssize=Words; _} -> 8, 16, Type.imm 16 - in + let nelem, _nbits, elemt = match imm8cb.ssize with + | Bytes -> 16, 8, Type.imm 8 + | Words -> 8, 16, Type.imm 16 in + (* Get element index in e *) let get_elem = extract_element !!elemt in - (* Get from xmm1/xmm2 *) let get_xmm1 = get_elem xmm1_e in let get_xmm2 = get_elem xmm2m128_e in + + let nelem_range = + List.range ~stride:(-1) ~stop:`inclusive (nelem-1) 0 in + (* Build expressions that assigns the correct values to the - is_valid variables using implicit (NULL-based) string - length. *) - let build_implicit_valid_xmm_i is_valid_xmm_i get_xmm_i = + is_valid variables using implicit (NULL-based) string length. *) + let implicit_check is_valid_xmm_i get_xmm_i = let f acc i = - (* Previous element is valid *) - let prev_valid = if i = 0 then exp_true else Bil.var (is_valid_xmm_i (i-1)) in - (* Current element is valid *) - let curr_valid = Bil.(get_xmm_i i <> (int_exp 0 !!elemt)) in - Bil.Let(is_valid_xmm_i i, Bil.(prev_valid land curr_valid), acc) - in (fun e -> List.fold_left ~f:f ~init:e (List.range ~stride:(-1) ~stop:`inclusive (nelem-1) 0)) - in + let previous_valid = + if i = 0 then exp_true + else Bil.var (is_valid_xmm_i (i - 1)) in + let current_valid = + Bil.(get_xmm_i i <> (int_exp 0 !!elemt)) in + let x = is_valid_xmm_i i in + Bil.(x := previous_valid land current_valid) :: acc in + List.fold ~f:f ~init:[] nelem_range in + (* Build expressions that assigns the correct values to the is_valid variables using explicit string length. *) - let build_explicit_valid_xmm_i is_valid_xmm_i sizee = + let explicit_check is_valid_xmm_i sizee = (* Max size is nelem *) + let nelem_e = Word.of_int ~width:(bitwidth_of_type regm) nelem in let sizev = tmp ~name:"sz" regm in - let sizee = Bil.(Ite (BinOp (LT, int_exp nelem !!regm, sizee), int_exp nelem !!regm, sizee)) in + let init = Bil.[ + if_ (int nelem_e < sizee) [ + sizev := int nelem_e; + ] [ + sizev := sizee; + ] + ] in let f acc i = (* Current element is valid *) - let curr_valid = Bil.(BinOp (LT, int_exp i !!regm, Var sizev)) in - Bil.Let(is_valid_xmm_i i, curr_valid, acc) - in (fun e -> Bil.Let(sizev, sizee, List.fold_left ~f:f ~init:e (List.range ~stride:(-1) ~stop:`inclusive (nelem-1) 0))) - in + let current_valid = Bil.(int_exp i !!regm < var sizev) in + let x = is_valid_xmm_i i in + Bil.(x := current_valid) :: acc in + List.fold_left ~f ~init nelem_range in (* Get var name indicating whether index in xmm num is a valid byte (before NULL byte). *) @@ -606,156 +653,154 @@ module ToIR = struct (fun xmmnum index -> match Hashtbl.find vh (xmmnum,index) with | Some v -> v | None -> - let v = tmp ~name:("is_valid_xmm"^string_of_int xmmnum^"_ele"^string_of_int index) bool_t in + let name = sprintf "is_valid_xmm%d_ele%d" xmmnum index in + let v = tmp ~name bool_t in Hashtbl.add_exn vh ~key:(xmmnum,index) ~data:v; - v) - in + v) in let is_valid_xmm1 index = is_valid 1 index in let is_valid_xmm2 index = is_valid 2 index in let is_valid_xmm1_e index = Bil.Var(is_valid_xmm1 index) in let is_valid_xmm2_e index = Bil.Var(is_valid_xmm2 index) in - let build_valid_xmm1,build_valid_xmm2 = - match pcmpinfo with - | {len=Implicit; _} -> - build_implicit_valid_xmm_i is_valid_xmm1 get_xmm1, - build_implicit_valid_xmm_i is_valid_xmm2 get_xmm2 - | {len=Explicit; _} -> - build_explicit_valid_xmm_i is_valid_xmm1 rax_e, - build_explicit_valid_xmm_i is_valid_xmm2 rdx_e - in + let xmm1_checks, xmm2_checks = + match pcmpinfo.len with + | Implicit -> + implicit_check is_valid_xmm1 get_xmm1, + implicit_check is_valid_xmm2 get_xmm2 + | Explicit -> + explicit_check is_valid_xmm1 rax_e, + explicit_check is_valid_xmm2 rdx_e in - let get_intres1_bit index = - match imm8cb with - | {agg=EqualAny; _} -> + let get_bit index = + match imm8cb.agg with + | EqualAny -> (* Is xmm2[index] at xmm1[j]? *) let check_char acc j = - let eql = Bil.((get_xmm2 index) = (get_xmm1 j)) in - let valid = is_valid_xmm1_e j in - Bil.(Ite ((eql land valid), exp_true, acc)) + let is_eql = Bil.(get_xmm2 index = get_xmm1 j) in + let is_valid = is_valid_xmm1_e j in + Bil.((is_eql land is_valid) lor acc) in - Bil.BinOp (AND, is_valid_xmm2_e index, - (* Is xmm2[index] included in xmm1[j] for any j? *) - (List.fold ~f:check_char ~init:exp_false (List.range - ~stride:(-1) ~stop:`inclusive (nelem-1) 0))) - | {agg=Ranges; _} -> + (* Is xmm2[index] included in xmm1[j] for any j? *) + Bil.(is_valid_xmm2_e index land + (List.fold ~f:check_char ~init:exp_false nelem_range)) + | Ranges -> (* Is there an even j such that xmm1[j] <= xmm2[index] <= xmm1[j+1]? *) let check_char acc j = (* XXX: Should this be AND? *) - let rangevalid = Bil.(is_valid_xmm1_e Pervasives.(2*j) land is_valid_xmm1_e Pervasives.(2*j+1)) in - let lte = match imm8cb with - | {ssign=Unsigned; _} -> LE - | {ssign=Signed; _} -> SLE - in + let ind0 = 2 * j in + let ind1 = ind0 + 1 in + let rangevalid = Bil.(is_valid_xmm1_e ind0 land is_valid_xmm1_e ind1) in + let (<=) = match imm8cb.ssign with + | Unsigned -> Bil.(<=) + | Signed -> Bil.(<=$) in + let (land) = Bil.(land) in let inrange = - Bil.((BinOp (lte, (get_xmm1 Pervasives.(2*j)), (get_xmm2 index))) - land (BinOp (lte, (get_xmm2 index), (get_xmm1 Pervasives.(2*j+1))))) - in - Bil.(Ite (UnOp (NOT, rangevalid), exp_false, Ite (inrange, exp_true, acc))) - in - Bil.(is_valid_xmm2_e index - (* Is xmm2[index] in the jth range pair? *) - land List.fold_left ~f:check_char ~init:exp_false (List.range ~stride:(-1) ~stop:`inclusive Pervasives.(nelem/2-1) 0)) - | {agg=EqualEach; _} -> + (get_xmm1 ind0 <= get_xmm2 index) land (get_xmm2 index <= get_xmm1 ind1) in + Bil.(rangevalid land (inrange lor acc)) in + Bil.(is_valid_xmm2_e index land + List.fold_left ~f:check_char ~init:exp_false (List.range ~stride:(-1) ~stop:`inclusive Pervasives.(nelem/2-1) 0)) + | EqualEach -> (* Does xmm1[index] = xmm2[index]? *) let xmm1_invalid = Bil.(UnOp (NOT, (is_valid_xmm1_e index))) in let xmm2_invalid = Bil.(UnOp (NOT, (is_valid_xmm2_e index))) in let bothinvalid = Bil.(xmm1_invalid land xmm2_invalid) in let eitherinvalid = Bil.(xmm1_invalid lor xmm2_invalid) in - let eq = Bil.(get_xmm1 index = get_xmm2 index) in + let equal = Bil.(get_xmm1 index = get_xmm2 index) in (* both invalid -> true one invalid -> false both valid -> check same byte *) - Bil.Ite (bothinvalid, exp_true, - Bil.Ite (eitherinvalid, exp_false, - Bil.Ite (eq, exp_true, exp_false))) - | {agg=EqualOrdered; _} -> + Bil.(bothinvalid lor (UnOp (NOT, eitherinvalid) land equal)) + | EqualOrdered -> (* Does the substring xmm1 occur at xmm2[index]? *) let check_char acc j = - let neq = Bil.(get_xmm1 j <> get_xmm2 Pervasives.(index+j)) in + let equal = Bil.(get_xmm1 j = get_xmm2 Pervasives.(index+j)) in let substrended = Bil.(UnOp (NOT, (is_valid_xmm1_e j))) in let bigstrended = Bil.UnOp (NOT, (is_valid_xmm2_e (index+j))) in (* substrended => true bigstrended => false byte diff => false byte same => keep going *) - Bil.Ite (substrended, exp_true, - Bil.Ite (bigstrended, exp_false, - Bil.Ite (neq, exp_false, acc))) - in + Bil.(substrended lor + (UnOp (NOT,bigstrended) land (equal land acc))) in (* Is xmm1[j] equal to xmm2[index+j]? *) List.fold_left ~f:check_char ~init:exp_true (List.range ~stride:(-1) ~stop:`inclusive (nelem-index-1) 0) in - let bits = List.map ~f:get_intres1_bit (List.range ~stride:(-1) ~stop:`inclusive (nelem-1) 0) in - let res_e = build_valid_xmm1 (build_valid_xmm2 (concat_explist bits)) in + let bits = List.map ~f:get_bit nelem_range in + let res, res_bil = concat 1 bits in let int_res_1 = tmp ~name:"IntRes1" reg16_t in let int_res_2 = tmp ~name:"IntRes2" reg16_t in let contains_null e = - List.fold_left ~f:(fun acc i -> - Bil.Ite (Bil.(get_elem e i = int_exp 0 !!elemt), exp_true, acc)) ~init:exp_false (List.init ~f:(fun x -> x) nelem) - in + let elts = List.init nelem ~f:(fun i -> Bil.(get_elem e i = int_exp 0 !!elemt)) in + List.fold elts ~init:exp_false ~f:(fun acc elt -> Bil.(acc lor elt)) in + (* For pcmpistri/pcmpestri *) - let sb e = + let sb exp = List.fold_left ~f:(fun acc i -> - Bil.Ite (Bil.(exp_true = Extract (i, i, e)), - (int_exp i !!regm), - acc)) + Bil.Ite (Bil.(exp_true = Extract (i, i, exp)), + (int_exp i !!regm), acc)) ~init:(int_exp nelem !!regm) - (match imm8cb with - | {outselectsig=LSB; _} -> List.range ~stride:(-1) ~start:`exclusive ~stop:`inclusive nelem 0 - | {outselectsig=MSB; _} -> List.init ~f:(fun x -> x) nelem) + (match imm8cb.outselectsig with + | LSB -> List.range ~stride:(-1) ~start:`exclusive ~stop:`inclusive nelem 0 + | MSB -> List.init ~f:(fun x -> x) nelem) in + (* For pcmpistrm/pcmpestrm *) let mask e = - match imm8cb with - | {outselectmask=Bitmask; _} -> - Bil.(Cast (UNSIGNED, !!reg128_t, e)) - | {outselectmask=Bytemask; _} -> + match imm8cb.outselectmask with + | Bitmask -> Bil.(cast unsigned 128 e) + | Bytemask -> let get_element i = - Bil.(Cast (UNSIGNED, !!elemt, Extract (i, i, e))) - in - concat_explist (List.map ~f:get_element (List.range ~stride:(-1) ~start:`exclusive ~stop:`inclusive nelem 0)) - in - (* comment crap from earlier *) - (*comment - ::*) - let open Stmt in - Move (int_res_1, Bil.(Cast (UNSIGNED, !!reg16_t, res_e))) - :: (match imm8cb with - | {negintres1=false; _} -> - Move (int_res_2, Bil.Var int_res_1) - | {negintres1=true; maskintres1=false; _} -> - (* int_res_1 is bitwise-notted *) - Move (int_res_2, Bil.(UnOp (NOT, (Var int_res_1)))) - | {negintres1=true; maskintres1=true; _} -> - (* only the valid elements in xmm2 are bitwise-notted *) - (* XXX: Right now we duplicate the valid element computations - when negating the valid elements. They are also used by the - aggregation functions. A better way to implement this might - be to write the valid element information out as a temporary - bitvector. The aggregation functions and this code would - then extract the relevant bit to see if an element is - valid. *) - let validvector = - let bits = List.map ~f:is_valid_xmm2_e (List.range ~stride:(-1) ~start:`exclusive ~stop:`inclusive nelem 0) in - build_valid_xmm2 (Bil.(Cast (UNSIGNED, !!reg16_t, concat_explist bits))) - in - Move (int_res_2, Bil.(validvector lxor Var int_res_1))) - :: (match pcmpinfo with - | {out=Index; _} -> Move (rcx, sb (Bil.Var int_res_2)) - (* FIXME: ymms should be used instead of xmms here *) - | {out=Mask; _} -> Move (ymms.(0), mask (Bil.Var int_res_2))) - :: Move (cf, Bil.(Var int_res_2 <> int_exp 0 16)) - :: Move (zf ,contains_null xmm2m128_e) - :: Move (sf, contains_null xmm1_e) - :: Move (oF, Bil.(Extract (0, 0, Var int_res_2))) - :: Move (af, int_exp 0 1) - :: Move (pf, int_exp 0 1) - :: [] + Bil.(cast unsigned !!elemt (extract i i e)) in + let range = List.range ~stride:(-1) + ~start:`exclusive ~stop:`inclusive nelem 0 in + concat_explist (List.map ~f:get_element range) in + + let res_of_cb = match imm8cb with + | {negintres1=false; _} -> Bil.(int_res_2 := var int_res_1) + | {negintres1=true; maskintres1=false; _} -> (* int_res_1 is bitwise-notted *) + Bil.(int_res_2 := unop not (var int_res_1)) + | {negintres1=true; maskintres1=true; _} -> + (* only the valid elements in xmm2 are bitwise-notted *) + (* XXX: Right now we duplicate the valid element computations + when negating the valid elements. They are also used by the + aggregation functions. A better way to implement this might + be to write the valid element information out as a temporary + bitvector. The aggregation functions and this code would + then extract the relevant bit to see if an element is + valid. *) + let validvector = + let range = List.range ~stride:(-1) + ~start:`exclusive ~stop:`inclusive nelem 0 in + let bits = List.map ~f:is_valid_xmm2_e range in + Bil.(cast unsigned 16 (concat_explist bits)) in + Bil.(int_res_2 := validvector lxor var int_res_1) in + + let res_of_pcmpinfo = match pcmpinfo.out with + | Index -> Bil.(rcx := sb (var int_res_2)) + (* FIXME: ymms should be used instead of xmms here *) + | Mask -> Bil.(ymms.(0) := mask (var int_res_2)) in + + List.concat [ + xmm1_checks; + xmm2_checks; + res_bil; + Bil.[ + int_res_1 := cast unsigned 16 (var res); + res_of_cb; + res_of_pcmpinfo; + cf := var int_res_2 <> int_exp 0 16; + zf := contains_null xmm2m128_e; + sf := contains_null xmm1_e; + oF := extract 0 0 (var int_res_2); + af := int_exp 0 1; + pf := int_exp 0 1; + ] + ] + | Pshufd (t, dst, src, vsrc, imm) -> let src_e = op2e t src in let imm_e = op2e t imm in