Skip to content

Commit

Permalink
Guess sqrt impl
Browse files Browse the repository at this point in the history 
Original evaluator did not implement real sqrt.
Not entirely clear how this should be done, but
an implementation is needed for coverage to work.
  • Loading branch information
@ncough
ncough committed Nov 26, 2024
1 parent b7e68b2 commit ee24298
Show file tree
Hide file tree
Showing 4 changed files with 42 additions and 32 deletions.
4 changes: 3 additions & 1 deletion libASL/primops.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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))


(****************************************************************)
Expand Down
2 changes: 1 addition & 1 deletion libASL/value.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Expand Down
32 changes: 20 additions & 12 deletions tests/aslt/test_cntlm_vec.t
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 ] ) ;
Expand Down
36 changes: 18 additions & 18 deletions tests/coverage/aarch64_float
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand Down

0 comments on commit ee24298

Please sign in to comment.