diff --git a/libASL/primops.ml b/libASL/primops.ml index 97b453bb..37f42b7c 100644 --- a/libASL/primops.ml +++ b/libASL/primops.ml @@ -104,7 +104,9 @@ let prim_round_up_real (x: real): bigint = Z.add Z.one (Q.to_bigint x) end -let prim_sqrt_real (x: real): real = failwith "prim_sqrt_real" +(* TODO: Not sure exactly what rounding/precision is expected here *) +let prim_sqrt_real (x: real): real = + Q.make (Z.sqrt (Q.num x)) (Z.sqrt (Q.den x)) (****************************************************************) diff --git a/libASL/value.ml b/libASL/value.ml index 4b106365..8fd89fa1 100644 --- a/libASL/value.ml +++ b/libASL/value.ml @@ -307,7 +307,7 @@ let eval_prim (f: string) (tvs: value list) (vs: value list): value option = | ("round_tozero_real", [ ], [VReal x ]) -> Some (VInt (prim_round_tozero_real x)) | ("round_down_real", [ ], [VReal x ]) -> Some (VInt (prim_round_down_real x)) | ("round_up_real", [ ], [VReal x ]) -> Some (VInt (prim_round_up_real x)) - | ("sqrt_real", [ ], [VReal x; VReal y ]) -> Some (VReal (prim_sqrt_real x)) + | ("sqrt_real", [ ], [VReal x ]) -> Some (VReal (prim_sqrt_real x)) | ("cvt_int_bits", [_ ], [VInt x; VInt n ]) -> Some (VBits (prim_cvt_int_bits n x)) | ("cvt_bits_sint", [VInt n], [VBits x ]) -> Some (VInt (prim_cvt_bits_sint x)) | ("cvt_bits_uint", [VInt n], [VBits x ]) -> Some (VInt (prim_cvt_bits_uint x)) diff --git a/tests/aslt/test_cntlm_vec.t b/tests/aslt/test_cntlm_vec.t index 8adb581a..e89b9012 100644 --- a/tests/aslt/test_cntlm_vec.t +++ b/tests/aslt/test_cntlm_vec.t @@ -298,36 +298,44 @@ __array _Z [ 1 ] = and_bits.0 {{ 128 }} ( __array _Z [ 5 ],__array _Z [ 1 ] ) ; "0x4e61d800" Decoding instruction A64 4e61d800 + constant bits ( 128 ) Exp6__5 = __array _Z [ 0 ] ; bits ( 128 ) result__4 ; + constant bits ( 32 ) Exp7__4 = FPCR ; bits ( 4 ) FPDecodeRounding9__6 ; FPDecodeRounding9__6 = ZeroExtend.0 {{ 2,4 }} ( FPCR [ 22 +: 2 ],4 ) ; - constant bits ( 64 ) Exp12__5 = FixedToFP.0 {{ 64,64 }} ( Elem.read.0 {{ 128,64 }} ( __array _Z [ 0 ],0,64 ),0,FALSE,FPCR,cvt_bits_uint.0 {{ 4 }} ( FPDecodeRounding9__6 ) ) ; - constant bits ( 64 ) Exp13__5 = FixedToFP.0 {{ 64,64 }} ( Elem.read.0 {{ 128,64 }} ( __array _Z [ 0 ],1,64 ),0,FALSE,FPCR,cvt_bits_uint.0 {{ 4 }} ( FPDecodeRounding9__6 ) ) ; - __array _Z [ 0 ] = Elem.set.0 {{ 128,64 }} ( Elem.set.0 {{ 128,64 }} ( result__4,0,64,Exp12__5 ),1,64,Exp13__5 ) ; + constant bits ( 4 ) Exp10__6 = FPDecodeRounding9__6 ; + result__4 = fixed_to_fp_vec.0 {{ 2,64,64 }} ( Exp6__5,0,FALSE,Exp7__4,cvt_bits_uint.0 {{ 4 }} ( Exp10__6 ),2 ) ; + __array _Z [ 0 ] = result__4 ; "0x4e61d821" Decoding instruction A64 4e61d821 + constant bits ( 128 ) Exp6__5 = __array _Z [ 1 ] ; bits ( 128 ) result__4 ; + constant bits ( 32 ) Exp7__4 = FPCR ; bits ( 4 ) FPDecodeRounding9__6 ; FPDecodeRounding9__6 = ZeroExtend.0 {{ 2,4 }} ( FPCR [ 22 +: 2 ],4 ) ; - constant bits ( 64 ) Exp12__5 = FixedToFP.0 {{ 64,64 }} ( Elem.read.0 {{ 128,64 }} ( __array _Z [ 1 ],0,64 ),0,FALSE,FPCR,cvt_bits_uint.0 {{ 4 }} ( FPDecodeRounding9__6 ) ) ; - constant bits ( 64 ) Exp13__5 = FixedToFP.0 {{ 64,64 }} ( Elem.read.0 {{ 128,64 }} ( __array _Z [ 1 ],1,64 ),0,FALSE,FPCR,cvt_bits_uint.0 {{ 4 }} ( FPDecodeRounding9__6 ) ) ; - __array _Z [ 1 ] = Elem.set.0 {{ 128,64 }} ( Elem.set.0 {{ 128,64 }} ( result__4,0,64,Exp12__5 ),1,64,Exp13__5 ) ; + constant bits ( 4 ) Exp10__6 = FPDecodeRounding9__6 ; + result__4 = fixed_to_fp_vec.0 {{ 2,64,64 }} ( Exp6__5,0,FALSE,Exp7__4,cvt_bits_uint.0 {{ 4 }} ( Exp10__6 ),2 ) ; + __array _Z [ 1 ] = result__4 ; "0x4e61d842" Decoding instruction A64 4e61d842 + constant bits ( 128 ) Exp6__5 = __array _Z [ 2 ] ; bits ( 128 ) result__4 ; + constant bits ( 32 ) Exp7__4 = FPCR ; bits ( 4 ) FPDecodeRounding9__6 ; FPDecodeRounding9__6 = ZeroExtend.0 {{ 2,4 }} ( FPCR [ 22 +: 2 ],4 ) ; - constant bits ( 64 ) Exp12__5 = FixedToFP.0 {{ 64,64 }} ( Elem.read.0 {{ 128,64 }} ( __array _Z [ 2 ],0,64 ),0,FALSE,FPCR,cvt_bits_uint.0 {{ 4 }} ( FPDecodeRounding9__6 ) ) ; - constant bits ( 64 ) Exp13__5 = FixedToFP.0 {{ 64,64 }} ( Elem.read.0 {{ 128,64 }} ( __array _Z [ 2 ],1,64 ),0,FALSE,FPCR,cvt_bits_uint.0 {{ 4 }} ( FPDecodeRounding9__6 ) ) ; - __array _Z [ 2 ] = Elem.set.0 {{ 128,64 }} ( Elem.set.0 {{ 128,64 }} ( result__4,0,64,Exp12__5 ),1,64,Exp13__5 ) ; + constant bits ( 4 ) Exp10__6 = FPDecodeRounding9__6 ; + result__4 = fixed_to_fp_vec.0 {{ 2,64,64 }} ( Exp6__5,0,FALSE,Exp7__4,cvt_bits_uint.0 {{ 4 }} ( Exp10__6 ),2 ) ; + __array _Z [ 2 ] = result__4 ; "0x4e61d863" Decoding instruction A64 4e61d863 + constant bits ( 128 ) Exp6__5 = __array _Z [ 3 ] ; bits ( 128 ) result__4 ; + constant bits ( 32 ) Exp7__4 = FPCR ; bits ( 4 ) FPDecodeRounding9__6 ; FPDecodeRounding9__6 = ZeroExtend.0 {{ 2,4 }} ( FPCR [ 22 +: 2 ],4 ) ; - constant bits ( 64 ) Exp12__5 = FixedToFP.0 {{ 64,64 }} ( Elem.read.0 {{ 128,64 }} ( __array _Z [ 3 ],0,64 ),0,FALSE,FPCR,cvt_bits_uint.0 {{ 4 }} ( FPDecodeRounding9__6 ) ) ; - constant bits ( 64 ) Exp13__5 = FixedToFP.0 {{ 64,64 }} ( Elem.read.0 {{ 128,64 }} ( __array _Z [ 3 ],1,64 ),0,FALSE,FPCR,cvt_bits_uint.0 {{ 4 }} ( FPDecodeRounding9__6 ) ) ; - __array _Z [ 3 ] = Elem.set.0 {{ 128,64 }} ( Elem.set.0 {{ 128,64 }} ( result__4,0,64,Exp12__5 ),1,64,Exp13__5 ) ; + constant bits ( 4 ) Exp10__6 = FPDecodeRounding9__6 ; + result__4 = fixed_to_fp_vec.0 {{ 2,64,64 }} ( Exp6__5,0,FALSE,Exp7__4,cvt_bits_uint.0 {{ 4 }} ( Exp10__6 ),2 ) ; + __array _Z [ 3 ] = result__4 ; "0x4ea11c23" Decoding instruction A64 4ea11c23 __array _Z [ 3 ] = or_bits.0 {{ 128 }} ( __array _Z [ 1 ],__array _Z [ 1 ] ) ; diff --git a/tests/coverage/aarch64_float b/tests/coverage/aarch64_float index 80e07702..f0a9292d 100644 --- a/tests/coverage/aarch64_float +++ b/tests/coverage/aarch64_float @@ -2741,12 +2741,12 @@ ENCODING: aarch64_float_arithmetic_unary 0x1e2143e0: [ftype=0 ; opc=2 ; Rn=31 ; Rd=0] --> OK 0x1e2143e1: [ftype=0 ; opc=2 ; Rn=31 ; Rd=1] --> OK 0x1e2143ff: [ftype=0 ; opc=2 ; Rn=31 ; Rd=31] --> OK -0x1e21c000: [ftype=0 ; opc=3 ; Rn=0 ; Rd=0] --> [1] Evaluation failure: EvalError at file "./prelude.asl" line 318 char 11 - line 319 char 0: getFun sqrt_real.0 +0x1e21c000: [ftype=0 ; opc=3 ; Rn=0 ; Rd=0] --> OK 0x1e21c001: [ftype=0 ; opc=3 ; Rn=0 ; Rd=1] --> OK -0x1e21c01f: [ftype=0 ; opc=3 ; Rn=0 ; Rd=31] --> [1] Evaluation failure: EvalError at file "./prelude.asl" line 318 char 11 - line 319 char 0: getFun sqrt_real.0 -0x1e21c020: [ftype=0 ; opc=3 ; Rn=1 ; Rd=0] --> [1] Evaluation failure: EvalError at file "./prelude.asl" line 318 char 11 - line 319 char 0: getFun sqrt_real.0 +0x1e21c01f: [ftype=0 ; opc=3 ; Rn=0 ; Rd=31] --> OK +0x1e21c020: [ftype=0 ; opc=3 ; Rn=1 ; Rd=0] --> OK 0x1e21c021: [ftype=0 ; opc=3 ; Rn=1 ; Rd=1] --> OK -0x1e21c03f: [ftype=0 ; opc=3 ; Rn=1 ; Rd=31] --> [1] Evaluation failure: EvalError at file "./prelude.asl" line 318 char 11 - line 319 char 0: getFun sqrt_real.0 +0x1e21c03f: [ftype=0 ; opc=3 ; Rn=1 ; Rd=31] --> OK 0x1e21c3e0: [ftype=0 ; opc=3 ; Rn=31 ; Rd=0] --> OK 0x1e21c3e1: [ftype=0 ; opc=3 ; Rn=31 ; Rd=1] --> OK 0x1e21c3ff: [ftype=0 ; opc=3 ; Rn=31 ; Rd=31] --> OK @@ -2777,15 +2777,15 @@ ENCODING: aarch64_float_arithmetic_unary 0x1e6143e0: [ftype=1 ; opc=2 ; Rn=31 ; Rd=0] --> OK 0x1e6143e1: [ftype=1 ; opc=2 ; Rn=31 ; Rd=1] --> OK 0x1e6143ff: [ftype=1 ; opc=2 ; Rn=31 ; Rd=31] --> OK -0x1e61c000: [ftype=1 ; opc=3 ; Rn=0 ; Rd=0] --> [1] Evaluation failure: EvalError at file "./prelude.asl" line 318 char 11 - line 319 char 0: getFun sqrt_real.0 -0x1e61c001: [ftype=1 ; opc=3 ; Rn=0 ; Rd=1] --> [1] Evaluation failure: EvalError at file "./prelude.asl" line 318 char 11 - line 319 char 0: getFun sqrt_real.0 -0x1e61c01f: [ftype=1 ; opc=3 ; Rn=0 ; Rd=31] --> [1] Evaluation failure: EvalError at file "./prelude.asl" line 318 char 11 - line 319 char 0: getFun sqrt_real.0 -0x1e61c020: [ftype=1 ; opc=3 ; Rn=1 ; Rd=0] --> [1] Evaluation failure: EvalError at file "./prelude.asl" line 318 char 11 - line 319 char 0: getFun sqrt_real.0 -0x1e61c021: [ftype=1 ; opc=3 ; Rn=1 ; Rd=1] --> [1] Evaluation failure: EvalError at file "./prelude.asl" line 318 char 11 - line 319 char 0: getFun sqrt_real.0 -0x1e61c03f: [ftype=1 ; opc=3 ; Rn=1 ; Rd=31] --> [1] Evaluation failure: EvalError at file "./prelude.asl" line 318 char 11 - line 319 char 0: getFun sqrt_real.0 -0x1e61c3e0: [ftype=1 ; opc=3 ; Rn=31 ; Rd=0] --> [1] Evaluation failure: EvalError at file "./prelude.asl" line 318 char 11 - line 319 char 0: getFun sqrt_real.0 -0x1e61c3e1: [ftype=1 ; opc=3 ; Rn=31 ; Rd=1] --> [1] Evaluation failure: EvalError at file "./prelude.asl" line 318 char 11 - line 319 char 0: getFun sqrt_real.0 -0x1e61c3ff: [ftype=1 ; opc=3 ; Rn=31 ; Rd=31] --> [1] Evaluation failure: EvalError at file "./prelude.asl" line 318 char 11 - line 319 char 0: getFun sqrt_real.0 +0x1e61c000: [ftype=1 ; opc=3 ; Rn=0 ; Rd=0] --> OK +0x1e61c001: [ftype=1 ; opc=3 ; Rn=0 ; Rd=1] --> OK +0x1e61c01f: [ftype=1 ; opc=3 ; Rn=0 ; Rd=31] --> OK +0x1e61c020: [ftype=1 ; opc=3 ; Rn=1 ; Rd=0] --> OK +0x1e61c021: [ftype=1 ; opc=3 ; Rn=1 ; Rd=1] --> OK +0x1e61c03f: [ftype=1 ; opc=3 ; Rn=1 ; Rd=31] --> OK +0x1e61c3e0: [ftype=1 ; opc=3 ; Rn=31 ; Rd=0] --> OK +0x1e61c3e1: [ftype=1 ; opc=3 ; Rn=31 ; Rd=1] --> OK +0x1e61c3ff: [ftype=1 ; opc=3 ; Rn=31 ; Rd=31] --> OK 0x1ea04000: [ftype=2 ; opc=0 ; Rn=0 ; Rd=0] --> (invalid) 0x1ea04001: [ftype=2 ; opc=0 ; Rn=0 ; Rd=1] --> (invalid) 0x1ea0401f: [ftype=2 ; opc=0 ; Rn=0 ; Rd=31] --> (invalid) @@ -2850,14 +2850,14 @@ ENCODING: aarch64_float_arithmetic_unary 0x1ee143e1: [ftype=3 ; opc=2 ; Rn=31 ; Rd=1] --> OK 0x1ee143ff: [ftype=3 ; opc=2 ; Rn=31 ; Rd=31] --> OK 0x1ee1c000: [ftype=3 ; opc=3 ; Rn=0 ; Rd=0] --> OK -0x1ee1c001: [ftype=3 ; opc=3 ; Rn=0 ; Rd=1] --> [1] Evaluation failure: EvalError at file "./prelude.asl" line 318 char 11 - line 319 char 0: getFun sqrt_real.0 -0x1ee1c01f: [ftype=3 ; opc=3 ; Rn=0 ; Rd=31] --> [1] Evaluation failure: EvalError at file "./prelude.asl" line 318 char 11 - line 319 char 0: getFun sqrt_real.0 -0x1ee1c020: [ftype=3 ; opc=3 ; Rn=1 ; Rd=0] --> [1] Evaluation failure: EvalError at file "./prelude.asl" line 318 char 11 - line 319 char 0: getFun sqrt_real.0 +0x1ee1c001: [ftype=3 ; opc=3 ; Rn=0 ; Rd=1] --> OK +0x1ee1c01f: [ftype=3 ; opc=3 ; Rn=0 ; Rd=31] --> OK +0x1ee1c020: [ftype=3 ; opc=3 ; Rn=1 ; Rd=0] --> OK 0x1ee1c021: [ftype=3 ; opc=3 ; Rn=1 ; Rd=1] --> OK 0x1ee1c03f: [ftype=3 ; opc=3 ; Rn=1 ; Rd=31] --> OK -0x1ee1c3e0: [ftype=3 ; opc=3 ; Rn=31 ; Rd=0] --> [1] Evaluation failure: EvalError at file "./prelude.asl" line 318 char 11 - line 319 char 0: getFun sqrt_real.0 +0x1ee1c3e0: [ftype=3 ; opc=3 ; Rn=31 ; Rd=0] --> OK 0x1ee1c3e1: [ftype=3 ; opc=3 ; Rn=31 ; Rd=1] --> OK -0x1ee1c3ff: [ftype=3 ; opc=3 ; Rn=31 ; Rd=31] --> [1] Evaluation failure: EvalError at file "./prelude.asl" line 318 char 11 - line 319 char 0: getFun sqrt_real.0 +0x1ee1c3ff: [ftype=3 ; opc=3 ; Rn=31 ; Rd=31] --> OK ENCODING: aarch64_float_compare_cond 0x1e201400: [ftype=0 ; Rm=0 ; cond=1 ; Rn=0 ; op=0 ; nzcv=0] --> OK