diff options
| author | Gabriel Kerneis | 2014-03-20 12:31:07 +0000 |
|---|---|---|
| committer | Gabriel Kerneis | 2014-03-20 12:31:07 +0000 |
| commit | 32790be4b54ee7cd6aa3ffa279900d4acaee96a6 (patch) | |
| tree | 6f6235d0c252055caf5f5676d170dd9150948f09 /src/test | |
| parent | 1a18428234dc9f3462593ea5cb8d96d8f924db90 (diff) | |
Remove work-around from interpreter, move it to power.sail
Two bugs are worked-around here:
- missing cast to nat when a vector is wrapped in exts
(exts is a no-op currently anyway, so we are discarding it)
- missing cast (due to limited type-inference) in one if branch:
type given explicitly.
Diffstat (limited to 'src/test')
| -rw-r--r-- | src/test/power.sail | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/src/test/power.sail b/src/test/power.sail index 07b74c60..dc774f1d 100644 --- a/src/test/power.sail +++ b/src/test/power.sail @@ -1,7 +1,4 @@ -(* XXX sign extension *) -function forall Type 'a . 'a exts ( x ) = x - register (vector <0, 63, inc, bit>) GPR0 register (vector <0, 63, inc, bit>) GPR1 register (vector <0, 63, inc, bit>) GPR2 @@ -50,7 +47,7 @@ scattered function ast decode function clause execute ( AddImmediate ( RA, RT, SI ) ) = { - if ( RA == 0 ) then GPR[ RT ] := ( exts ( SI )) else GPR[ RT ] := ( (GPR[ RA ]) + ( exts ( SI )) ) ; + if ( RA == 0 ) then GPR[ RT ] := ( ( SI )) else GPR[ RT ] := ( (GPR[ RA ]) + ( ( SI )) ) ; } union ast member bit [ 1 ] (* BH *) * bit [ 4 ] (* BI *) * bit [ 4 ] (* BO *) * bit (* LK *) BranchConditionaltoLinkRegister @@ -77,7 +74,7 @@ scattered function ast decode function clause execute ( LoadWordandZero ( D, RA, RT ) ) = { if ( RA == 0 ) then b := 0 else b := (GPR[ RA ]) ; - EA := ( b + ( exts ( D )) ) ; + EA := ( b + ( ( D )) ) ; GPR[ RT ] := ( 0b00000000000000000000000000000000 : MEM( EA , 4 ) ) ; } @@ -96,8 +93,9 @@ scattered function ast decode function clause execute ( StoreWord ( D, RA, RS ) ) = { + (bit[64]) b := 0; if ( RA == 0 ) then b := 0 else b := (GPR[ RA ]) ; - EA := ( b + ( exts ( D )) ) ; + EA := ( b + ( ( D )) ) ; MEM( EA , 4 ) := (( (GPR[ RS ]) )[ 32 .. 63 ]) ; } @@ -108,7 +106,7 @@ scattered function ast decode function clause execute ( StoreWordwithUpdate ( D, RA, RS ) ) = { - EA := ( (GPR[ RA ]) + ( exts ( D )) ) ; + EA := ( (GPR[ RA ]) + ( ( D )) ) ; MEM( EA , 4 ) := (( (GPR[ RS ]) )[ 32 .. 63 ]) ; GPR[ RA ] := EA ; } |