forked from Hara-Laboratory/subleq-mips
-
-
Notifications
You must be signed in to change notification settings - Fork 0
/
TestFix2.hs
611 lines (511 loc) · 26.3 KB
/
TestFix2.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
{-# LANGUAGE FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, UndecidableInstances, TemplateHaskell, OverloadedStrings #-}
module Main where
import Language.Subleq.Model.Prim
import Language.Subleq.Model.Memory as Mem
import Language.Subleq.Model.Architecture.IntMachine
import qualified Language.Subleq.Model.InstructionSet.Subleq as Subleq
import qualified Language.Subleq.Assembly as A
import qualified Language.Subleq.Assembly.Export.Elf2Mem as A
import Text.Parsec
import Control.Applicative
import Text.PrettyPrint hiding ((<+>))
import qualified Text.PrettyPrint as PP
import qualified Data.ByteString as B
-- import Data.Maybe
import Data.String.ToString
import Data.Map (Map)
import qualified Data.Map as M
import Data.Set (Set)
import qualified Data.Set as S
import Data.FileEmbed
import Control.Monad
-- import Control.Monad.State
-- import Control.Lens
import Control.Arrow
import Test.QuickCheck
-- import Test.QuickCheck.Text
-- import Test.QuickCheck.All
import Data.Word
import Data.Int
import Data.Bits
import qualified Data.Bits as Bit
import Data.Function
import Text.Printf
import System.Environment
import qualified Data.ByteString.Lazy as BL
import qualified Data.Random as R
import qualified Data.Random.Distribution.Exponential as R
import qualified Data.Random.Distribution.Uniform as R
import qualified Data.Csv as CSV
import Data.Vector(Vector)
import qualified Data.Vector as V
import qualified System.FilePath as FP
import qualified SubleqTestUtils as T
type SubleqWord = Int32
type SubleqUWord = Word32
wordLength :: (Integral a, Num a) => a
wordLength = 32
{-
type SubleqWord = Int16
type SubleqUWord = Word16
wordLength :: (Integral a, Num a) => a
wordLength = 16
-}
type Fix2SubleqMemory = M.Map SubleqWord SubleqWord
type Fix2SubleqState = SubleqState SubleqWord SubleqWord Fix2SubleqMemory
locateArg :: A.LocateArg
locateArg xs = M.fromList $ zip xs [0..3]
subleqRoutines :: B.ByteString
subleqRoutines = $(embedFile "subleq-int-fix2.sq")
subleqModule :: A.Module
subleqModule = either (error . show) A.expandMacroAll $ parse A.parseModule "parserModule" subleqRoutines
inc, dec :: SubleqWord
inc = 0x4
dec = 0x5
-- \mo-> renderLoadPackResult $ A.loadModulePacked (memoryArchitectureFromConfig cfg) (s^.startAddress) (expand mo) (initialMemFromConfigure cfg)
subleqMA :: A.MemoryArchitecture (M.Map SubleqWord SubleqWord)
subleqMA = A.MemoryArchitecture { A.instructionLength = 3
, A.wordLength = 1
, A.locateArg = locateArg
, A.locateStatic = M.fromList [ ("End", -0x1)
, ("Inc", 0x4)
, ("Dec", 0x5)
, ("Z", 0x6)
, ("T0", 0x8)
, ("T1", 0x9)
, ("T2", 0xa)
, ("T3", 0xb)
, ("T4", 0xc)
, ("T5", 0xd)
, ("T6", 0xe)
, ("CW", 0xf)
-- , ("Lo", 0x120)
, ("Min", 0x10)
, ("Max", 0x11)
, ("WordLength", 32)
]
, A.writeWord = Mem.write `on` fromIntegral
}
subleqMAInitialMem :: M.Map SubleqWord SubleqWord
-- subleqMAInitialMem = Mem.write 0xf wordLength . Mem.write inc (-1) . Mem.write dec 1 $ M.empty
subleqMAInitialMem = Mem.write 0x11 maxBound . Mem.write 0x10 minBound . Mem.write 0xf wordLength . Mem.write inc (-1) . Mem.write dec 1 $ M.empty
subleqMATextSection :: Integer
subleqMATextSection = 0x1000
subleqProg = (Subleq.step, pos, mem)
where
(pos, mem) = T.assembleMachine subleqMA subleqMATextSection subleqModule subleqMAInitialMem
executeSubroutineWithStates :: A.Id -> [SubleqWord] -> Maybe Integer -> Maybe (Maybe ([SubleqWord], Fix2SubleqState), [Fix2SubleqState])
executeSubroutineWithStates = T.executeSubroutineWithStates subleqProg
maximumTry :: Maybe Integer
maximumTry = Just 1000000
executeSubroutineWithModification :: A.Id -> [SubleqWord] -> ([SubleqWord], Set SubleqWord)
executeSubroutineWithModification x args = case executeSubroutineWithStates x args maximumTry of
Just (Just (res, end), init:_) -> (res, changedAddresses end init)
Just (Nothing, _) -> error "Not terminated"
Nothing -> error "Not found"
executeSubroutine :: A.Id -> [SubleqWord] -> [SubleqWord]
executeSubroutine x args = if diffs `S.isSubsetOf` S.fromList [0..(fromIntegral $ length args - 1)] then res else error $ "it corrupses: " ++ show diffs
where
(res, diffs) = executeSubroutineWithModification x args
prop_IntWordTrip :: Int8 -> Bool
prop_IntWordTrip a = a == fromIntegral w
where
w :: Word8
w = fromIntegral a
prop_WordIntTrip :: Word8 -> Bool
prop_WordIntTrip a = a == fromIntegral w
where
w :: Int8
w = fromIntegral a
prop_Add :: SubleqWord -> SubleqWord -> SubleqWord -> Bool
prop_Add a b c = [b + c, b, c] == executeSubroutine "addu" [a, b, c]
prop_Sub :: SubleqWord -> SubleqWord -> SubleqWord -> Bool
prop_Sub a b c = [b - c, b, c] == executeSubroutine "subu" [a, b, c]
prop_Mflo :: SubleqWord -> SubleqWord -> Bool
prop_Mflo a lo = [lo, lo] == executeSubroutine "mflo" [a, lo]
prop_Mtlo :: SubleqWord -> SubleqWord -> Bool
prop_Mtlo lo a = [a, a] == executeSubroutine "mtlo" [lo, a]
-- prop_Mult :: SubleqWord -> SubleqWord -> SubleqWord -> Bool
-- prop_Mult a b c = [b * c, b, c] == executeSubroutine "mult" [a, b, c]
-- prop_MultuLo :: SubleqUWord -> SubleqUWord -> Bool
-- prop_MultuLo b c = fromIntegral a' == b * c
-- where
-- [a', _, _] = executeSubroutine "multuLo" $ map fromIntegral [0, b, c]
--prop_Floor2pow :: NonNegative SubleqWord -> NonNegative SubleqWord -> NonNegative SubleqWord -> Bool
--prop_Floor2pow (NonNegative a) (NonNegative b) (NonNegative c) = a' == a && r1 <= a && (a == 0 || a < 2 * r1) && r2 == a `div` 2
-- where
-- [r1, r2, a'] = executeSubroutine "floor2pow" [b, c, a]
prop_Bne :: SubleqWord -> SubleqWord -> SubleqWord -> SubleqWord -> Bool
prop_Bne rs rt off pc = [rs', rt', off'] == [rs, rt, off] && ((rs == rt && pc' == pc + off) || (rs /= rt && pc' == pc))
where
[rs', rt', off', pc'] = executeSubroutine "bne" [rs, rt, off, pc]
prop_BneA :: SubleqWord -> SubleqWord -> SubleqWord -> Bool
prop_BneA rs off pc = [rs', off'] == [rs, off] && pc' == pc + off
where
[rs', off', pc'] = executeSubroutine "bnea" [rs, off, pc]
prop_Lui :: SubleqUWord -> SubleqUWord -> Bool
prop_Lui rt imm = imm' == imm && rt' == imm `shift` 16
where
[rt', imm'] = map fromIntegral $ executeSubroutine "lui" $ map fromIntegral [rt, imm]
prop_Sll :: SubleqUWord -> SubleqUWord -> SubleqUWord -> Bool
prop_Sll rd rt sa = [rt', s'] == [rt, s] && rd' == rt `shift` fromIntegral s
where
s = sa `mod` wordLength
[rd', rt', s'] = map fromIntegral $ executeSubroutine "sll" $ map fromIntegral [rd, rt, s]
prop_Slli3 :: SubleqUWord -> SubleqUWord -> SubleqUWord -> Bool
prop_Slli3 rd rt sa = [rt', s'] == [rt, s] && rd' == rt `shift` (fromIntegral s `shift` 3)
where
s = sa `mod` wordLength
[rd', rt', s'] = map fromIntegral $ executeSubroutine "slli3" $ map fromIntegral [rd, rt, s]
prop_Slli4 :: SubleqUWord -> SubleqUWord -> SubleqUWord -> Bool
prop_Slli4 rd rt sa = [rt', s'] == [rt, s] && rd' == rt `shift` (fromIntegral s `shift` 4)
where
s = sa `mod` wordLength
[rd', rt', s'] = map fromIntegral $ executeSubroutine "slli4" $ map fromIntegral [rd, rt, s]
prop_Srl :: SubleqUWord -> SubleqUWord -> SubleqUWord -> Bool
prop_Srl rd rt sa = [rt', s'] == [rt, s] && rd' == rt `shift` (-(fromIntegral s))
where
s = sa `mod` wordLength
[rd', rt', s'] = map fromIntegral $ executeSubroutine "srl" $ map fromIntegral [rd, rt, s]
prop_Srli3 :: SubleqUWord -> SubleqUWord -> SubleqUWord -> Bool
prop_Srli3 rd rt sa = [rt', s'] == [rt, s] && rd' == rt `shift` (- (fromIntegral s `shift` 3))
where
s = sa `mod` wordLength
[rd', rt', s'] = map fromIntegral $ executeSubroutine "srli3" $ map fromIntegral [rd, rt, s]
prop_Srli4 :: SubleqUWord -> SubleqUWord -> SubleqUWord -> Bool
prop_Srli4 rd rt sa = [rt', s'] == [rt, s] && rd' == rt `shift` (- (fromIntegral s `shift` 4))
where
s = sa `mod` wordLength
[rd', rt', s'] = map fromIntegral $ executeSubroutine "srli4" $ map fromIntegral [rd, rt, s]
prop_Srl1dTest :: SubleqUWord -> SubleqUWord -> Bool
prop_Srl1dTest rh rl = rl' == rl `shift` 1 && rh' == (rh `shift` 1) + s
where
s = rl `shift` (1 - wordLength)
[rh', rl'] = map fromIntegral $ executeSubroutine "srl1dTest" $ map fromIntegral [rh, rl]
prop_Srl1dcTest :: SubleqUWord -> SubleqUWord -> SubleqUWord -> Bool
prop_Srl1dcTest rd rh rl = rd' == s && rl' == rl `shift` 1 && rh' == (rh `shift` 1) + s
where
s = rl `shift` (1 - wordLength)
[rd', rh', rl'] = map fromIntegral $ executeSubroutine "srl1dcTest" $ map fromIntegral [rd, rh, rl]
srl1dTestCd :: SubleqUWord -> SubleqUWord -> SubleqUWord -> (SubleqUWord, SubleqUWord, SubleqUWord)
srl1dTestCd rd rh rl = (s, (rh `shift` 1) + s, rl `shift` 1)
where
s = rl `shift` (1 - wordLength)
prop_Sra :: SubleqWord -> SubleqWord -> SubleqWord -> Bool
prop_Sra rd rt sa = [rt', s'] == [rt, s] && rd' == rt `shift` (-(fromIntegral s))
where
s = sa `mod` wordLength
[rd', rt', s'] = map fromIntegral $ executeSubroutine "sra" $ map fromIntegral [rd, rt, s]
prop_Multu :: SubleqUWord -> SubleqUWord -> SubleqUWord -> SubleqUWord -> Bool
prop_Multu hi lo rs rt = rs' == rs && rt' == rt && (iHi `shift` wordLength) + iLo == iRs * iRt
where
iHi, iLo, iRs, iRt :: Integer
[iHi, iLo, iRs, iRt] = map fromIntegral [hi', lo', rs', rt']
[hi', lo', rs', rt'] = map fromIntegral $ executeSubroutine "multu" $ map fromIntegral [hi, lo, rs, rt]
prop_MultD :: SubleqWord -> SubleqWord -> SubleqWord -> SubleqWord -> Bool
prop_MultD hi lo rs rt = (iHi `shift` wordLength) + iLo == iRs * iRt
where
iHi, iLo, iRs, iRt :: Integer
iLo = fromIntegral (fromIntegral lo' :: SubleqUWord)
[iHi, iRs, iRt] = map fromIntegral [hi', rs, rt]
[hi', lo', _, _] = executeSubroutine "multD" [hi, lo, rs, rt]
prop_Mult :: SubleqWord -> SubleqWord -> SubleqWord -> SubleqWord -> Bool
prop_Mult hi lo rs rt = [rs', rt'] == [rs, rt] && (iHi `shift` wordLength) + iLo == iRs * iRt
where
iHi, iLo, iRs, iRt :: Integer
iLo = fromIntegral (fromIntegral lo' :: SubleqUWord)
[iHi, iRs, iRt] = map fromIntegral [hi', rs, rt]
[hi', lo', rs', rt'] = executeSubroutine "mult" [hi, lo, rs, rt]
prop_Slt :: SubleqWord -> SubleqWord -> SubleqWord -> Bool
prop_Slt rd rs rt = [rd', rs', rt'] == [if rs < rt then 1 else 0, rs, rt]
where
[rd', rs', rt'] = executeSubroutine "slt" [rd, rs, rt]
prop_Sltu :: SubleqUWord -> SubleqUWord -> SubleqUWord -> Bool
prop_Sltu rd rs rt = [rd', rs', rt'] == [if rs < rt then 1 else 0, rs, rt]
where
[rd', rs', rt'] = map fromIntegral $ executeSubroutine "sltu" $ map fromIntegral [rd, rs, rt]
prop_And :: SubleqUWord -> SubleqUWord -> SubleqUWord -> Bool
prop_And rd rs rt = [rd', rs', rt'] == [rs Bit..&. rt, rs, rt]
where
[rd', rs', rt'] = map fromIntegral $ executeSubroutine "and" $ map fromIntegral [rd, rs, rt]
prop_Or :: SubleqUWord -> SubleqUWord -> SubleqUWord -> Bool
prop_Or rd rs rt = [rd', rs', rt'] == [rs Bit..|. rt, rs, rt]
where
[rd', rs', rt'] = map fromIntegral $ executeSubroutine "or" $ map fromIntegral [rd, rs, rt]
prop_Xor :: SubleqUWord -> SubleqUWord -> SubleqUWord -> Bool
prop_Xor rd rs rt = [rd', rs', rt'] == [rs `xor` rt, rs, rt]
where
[rd', rs', rt'] = map fromIntegral $ executeSubroutine "xor" $ map fromIntegral [rd, rs, rt]
prop_Nor :: SubleqUWord -> SubleqUWord -> SubleqUWord -> Bool
prop_Nor rd rs rt = [rd', rs', rt'] == [complement $ rs Bit..|. rt, rs, rt]
where
[rd', rs', rt'] = map fromIntegral $ executeSubroutine "nor" $ map fromIntegral [rd, rs, rt]
prop_Not :: SubleqUWord -> SubleqUWord -> Bool
prop_Not rd rs = [rd', rs'] == [complement rs, rs]
where
[rd', rs'] = map fromIntegral $ executeSubroutine "not" $ map fromIntegral [rd, rs]
prop_Lw :: SubleqUWord -> SubleqUWord -> Bool
prop_Lw rt rs = [rt', rs'] == [rs, rs]
where
[rt', rs'] = map fromIntegral $ executeSubroutine "lwTest" $ map fromIntegral [rt, rs]
prop_Sw :: SubleqUWord -> SubleqUWord -> Bool
prop_Sw rt rs = [rt', rs'] == [rt, rt]
where
[rt', rs'] = map fromIntegral $ executeSubroutine "swTest" $ map fromIntegral [rt, rs]
testLSb' target n lsvi subr rt rs frB = ([rt, rs, fr], fr'', [rt', rs', fr'], t, lsvi rt rs f s, lsvi rs rt f s, [f, s])
where
t = if target then rt' else rs'
s = fromIntegral sa
f = fromIntegral (fr * sa)
sa = 1 `shift` n
fr = frB `mod` (wordLength `div` sa)
fr'' = fr * (sa `div` 8)
[rt', rs', fr'] = map fromIntegral $ executeSubroutine subr $ map fromIntegral [rt, rs, fr'']
testSb :: Int -> LSvi -> String -> SubleqUWord -> SubleqUWord -> SubleqUWord -> Bool
testSb n lsvi subr rt rs frB = fr' == fr'' && rs' == lsvi rs rt f s
where
s = fromIntegral sa
f = fromIntegral (fr * sa)
sa = 1 `shift` n
fr = frB `mod` (wordLength `div` sa)
fr'' = fr * (sa `div` 8)
[rt', rs', fr'] = map fromIntegral $ executeSubroutine subr $ map fromIntegral [rt, rs, fr'']
testLb :: Int -> LSvi -> String -> SubleqUWord -> SubleqUWord -> SubleqUWord -> Bool
testLb n lsvi subr rt rs frB = fr' == fr'' && rt' == lsvi rt rs f s
where
s = fromIntegral sa
f = fromIntegral (fr * sa)
sa = 1 `shift` n
fr = frB `mod` (wordLength `div` sa)
fr'' = fr * (sa `div` 8)
[rt', rs', fr'] = map fromIntegral $ executeSubroutine subr $ map fromIntegral [rt, rs, fr'']
prop_Sw2 = testSb 5 (\rt rs f s -> rs) "swTest"
prop_Lw2 = testLb 5 (\rt rs f s -> rs) "lwTest"
prop_Sh = testSb 4 svi "shTest"
prop_Lhu = testLb 4 lvui "lhuTest"
prop_Sb = testSb 3 svi "sbTest"
prop_Lbu = testLb 3 lvui "lbuTest"
prop_Rl :: SubleqUWord -> SubleqUWord -> Bool
prop_Rl rt saB = [sa] == [sa] && rt' == (rt `shift` s) Bit..|. (rt `shift` (s - wordLength))
where
s = fromIntegral sa
sa = saB `mod` wordLength
[rt', sa'] = map fromIntegral $ executeSubroutine "rlTest" $ map fromIntegral [rt, sa]
prop_RlSlm :: SubleqUWord -> SubleqUWord -> SubleqUWord -> Bool
prop_RlSlm rt rs saB = [sa] == [sa] && rt' == (rt `shift` s) Bit..|. (rs `shift` (s - wordLength)) && rs' == (rs `shift` s)
where
s = fromIntegral sa
sa = saB `mod` wordLength
[rt', rs', sa'] = map fromIntegral $ executeSubroutine "rlslmTest" $ map fromIntegral [rt, rs, sa]
mask f s = ((1 `shift` s) - 1) `shift` (f - s + 1)
type LSvi = (SubleqUWord -> SubleqUWord -> Int -> Int -> SubleqUWord)
-- svi rt rs f s = (rt Bit..&. complement (mask f s)) Bit..|. ((rs Bit..&. mask (wordLength - 1) s) `shift` (f - wordLength + 1))
svi :: LSvi
svi rt rs f s = (rt Bit..&. complement (mask (f+s-1) s)) Bit..|. ((rs Bit..&. mask (s - 1) s) `shift` f)
testLSvi :: LSvi -> String -> SubleqUWord -> SubleqUWord -> SubleqUWord -> SubleqUWord -> Bool
testLSvi lsvi subr rt rs frB saB = [fr', sa'] == [fr, sa] && rt' == lsvi rt rs f s
where
s = fromIntegral sa
f = fromIntegral fr
sa = saB `mod` (wordLength - fr + 1)
fr = frB `mod` wordLength
[rt', rs', fr', sa'] = map fromIntegral $ executeSubroutine subr $ map fromIntegral [rt, rs, fr, sa]
testLSbi :: Int -> LSvi -> String -> SubleqUWord -> SubleqUWord -> SubleqUWord -> Bool
testLSbi n lsvi subr rt rs frB = fr' == fr && rt' == lsvi rt rs f s
where
s = fromIntegral sa
f = fromIntegral (fr * sa)
sa = 1 `shift` n
fr = frB `mod` (wordLength `div` sa)
[rt', rs', fr'] = map fromIntegral $ executeSubroutine subr $ map fromIntegral [rt, rs, fr]
lvui :: LSvi
-- svi rt rs f s = (rt Bit..&. complement (mask f s)) Bit..|. ((rs Bit..&. mask (wordLength - 1) s) `shift` (f - wordLength + 1))
lvui rt rs f s = (rs Bit..&. mask (f+s-1) s) `shift` (-f)
prop_Svi :: SubleqUWord -> SubleqUWord -> SubleqUWord -> SubleqUWord -> Bool
prop_Svi = testLSvi svi "sviTest"
prop_Lvui :: SubleqUWord -> SubleqUWord -> SubleqUWord -> SubleqUWord -> Bool
prop_Lvui = testLSvi lvui "lvuiTest"
prop_Sbi = testLSbi 3 svi "sbiTest"
prop_Lbi = testLSbi 3 lvui "lbuiTest"
prop_Shi = testLSbi 4 svi "shiTest"
prop_Lhi = testLSbi 4 lvui "lhuiTest"
prop_Addrw :: SubleqUWord -> SubleqUWord -> Bool
prop_Addrw rd rs = [rs'] == [rs] && rd' == rs `shift` (-2)
where
d = fromIntegral rd
s = fromIntegral rs
[rd', rs'] = map fromIntegral $ executeSubroutine "addrwTest" $ map fromIntegral [rd, rs]
prop_Addrb :: SubleqUWord -> SubleqUWord -> SubleqUWord -> Bool
prop_Addrb rd rt rs = [rs'] == [rs] && rt' == rs Bit..&. 0x3 && rd' == rs `shift` (-2)
where
d = fromIntegral rd
t = fromIntegral rt
s = fromIntegral rs
[rd', rt', rs'] = map fromIntegral $ executeSubroutine "addrbTest" $ map fromIntegral [rd, rt, rs]
prop_Addrh :: SubleqUWord -> SubleqUWord -> SubleqUWord -> Bool
prop_Addrh rd rt rs = [rs'] == [rs] && rt' == (rs Bit..&. 0x2) `shift` (-1) && rd' == rs `shift` (-2)
where
d = fromIntegral rd
t = fromIntegral rt
s = fromIntegral rs
[rd', rt', rs'] = map fromIntegral $ executeSubroutine "addrhTest" $ map fromIntegral [rd, rt, rs]
multD hi lo rs rt = ([(iHi `shift` wordLength) + iLo, iHi `shift` wordLength, iHi, iLo, iRs, iRt], (iHi `shift` wordLength) + iLo == iRs * iRt)
where
iHi, iLo, iRs, iRt :: Integer
iLo = fromIntegral (fromIntegral lo' :: SubleqUWord)
[iHi, iRs, iRt] = map fromIntegral [hi', rs, rt]
[hi', lo', _, _] = executeSubroutine "multD" [hi, lo, rs, rt]
showFix2SubleqState :: Fix2SubleqState -> Doc
showFix2SubleqState (pc, mem) = integer (fromIntegral pc) <> colon PP.<+> hsep (map (\a-> integer $ memread a mem) [0..15]) PP.<+> colon PP.<+> hsep (map (\a-> integer $ memread a mem) [16..31]) PP.<+> colon PP.<+> integer (memread 0x120 mem) PP.<+> colon PP.<+> hsep (map (\a-> integer $ memread a mem) [pc..(pc+2)])
where
memread a mem = fromIntegral $ Mem.read (fromIntegral a) mem
printExecution :: Maybe (Maybe ([SubleqWord], Fix2SubleqState), [Fix2SubleqState]) -> Doc
printExecution Nothing = text "Subroutine not found"
printExecution (Just (Nothing, ss)) = text "Non terminated" $$ vcat (take 50 $ map showFix2SubleqState ss)
printExecution (Just (Just (args, end), ss)) = status $$ history $$ result $$ insns $$ memoryDiff
where
status = text "Terminated"
history = vcat (map showFix2SubleqState ss)
result = text "result: " <> text (show args) <> semi PP.<+> hsep (map (text . printf "%x") args)
insns = text "instructions: " <> integer (fromIntegral $ length ss - 1)
memoryDiff = text "modified: " <> text (show $ changedAddresses end $ head ss)
changedAddresses :: Fix2SubleqState -> Fix2SubleqState -> Set SubleqWord
changedAddresses (_, mem) (_,init) = M.foldrWithKey (\k v a-> if v then S.insert k a else a) S.empty $ M.mergeWithKey f g g mem init -- M.mergeWithKey (/=) mem init
where
f :: SubleqWord -> SubleqWord -> SubleqWord -> Maybe Bool
f _ m1 m2 | m1 == m2 = Nothing
| otherwise = Just True
g :: Map SubleqWord SubleqWord -> Map SubleqWord Bool
g = M.map (const True) . M.filter (/= 0)
printModule = putStrLn $ render $ A.printModule subleqModule
debugSubroutine :: A.Id -> [SubleqWord] -> Maybe Integer -> Doc
debugSubroutine i args tries = printExecution $ executeSubroutineWithStates i args tries
printSubroutine s addr = f loc
where
obj = A.lookupModule s subleqModule
loc = obj >>= A.locate subleqMA addr
f (Just (o, _)) = putStrLn $ render $ A.printObject o
f _ = putStrLn "not found"
res = T.res wordLength
randomSize = T.uniformTo wordLength
measureMultu n = do
xs <- map floor <$> res n
ys <- map floor <$> res n
let xys = zip xs ys
return $ do (x, y) <- xys
let res = T.measureInsns $ executeSubroutineWithStates "multu" [0,0,x,y] maximumTry
let ux = fromIntegral x :: SubleqUWord
let uy = fromIntegral y :: SubleqUWord
let pux = logBase 2 $ fromIntegral ux :: Double
let puy = logBase 2 $ fromIntegral uy :: Double
return (ux, uy, pux, puy, res)
measureSra n = do
xs <- map floor <$> res n
ys <- replicateM n $ R.sample randomSize
let xys = zip xs ys
return $ do (x, y) <- xys
let res = T.measureInsns $ executeSubroutineWithStates "sra" [0,x,y] maximumTry
return (x, y, res)
measureSrl n = do
xs <- map floor <$> res n
ys <- replicateM n $ R.sample randomSize
let xys = zip xs ys
return $ do (x, y) <- xys
let res = T.measureInsns $ executeSubroutineWithStates "srl" [0,x,y] maximumTry
return (x, y, res)
measureShiftType sub n = do
xs <- map floor <$> res n
ys <- replicateM n $ R.sample (T.uniformTo wordLength)
let xys = zip xs ys
return $ do (x, y) <- xys
let res = T.measureInsns $ executeSubroutineWithStates sub [0,x,y] maximumTry
return (x, y, res)
measureSviType sub n = do
xs <- map floor <$> res n
zs <- replicateM n $ R.sample randomSize
ys <- forM zs (\ z -> R.sample (T.uniformTo (wordLength - z + 1)))
let xys = zip3 xs ys zs
return $ do (x, y, z) <- xys
let res = T.measureInsns $ executeSubroutineWithStates sub [0,x,y,z] maximumTry
return (x, y, z, res)
measureSbiType b sub n = do
xs <- map floor <$> res n
ys <- replicateM n $ R.sample (T.uniformTo (wordLength `div` (1 `shift` b :: SubleqWord) - 1))
let xys = zip xs ys
return $ do (x, y) <- xys
let r' = executeSubroutineWithStates sub [0,x,y] maximumTry
case r' of
Nothing -> error $ mconcat [toString sub, " is non terminate with ", show (x,y)]
Just _ -> return ()
let res = T.measureInsns r'
return (x, y, res)
measureSvi = measureSviType "sviTest"
measureLvui = measureSviType "lvuiTest"
measureAddrbType sub n = do
xs <- map floor <$> res n
return $ do (x) <- xs
let r' = executeSubroutineWithStates sub [0,0,x] maximumTry
case r' of
Nothing -> error $ mconcat [toString sub, " is non terminate with ", show x]
Just _ -> return ()
let res = T.measureInsns r'
return (x, res)
measureBinaryWithP sub n = do
xs <- map floor <$> res n
xs' <- map (T.bitReversal . floor) <$> res n
ys <- map floor <$> res n
ys' <- map (T.bitReversal . floor) <$> res n
let xys = zip (xs ++ xs') (ys ++ ys')
return $ do (x, y) <- xys
let res = T.measureInsns $ executeSubroutineWithStates sub [0,x,y] maximumTry
let ux = fromIntegral x :: SubleqUWord
let uy = fromIntegral y :: SubleqUWord
let pux = logBase 2 $ fromIntegral ux :: Double
let puy = logBase 2 $ fromIntegral uy :: Double
return (ux, uy, pux, puy, res)
return []
outputCsv :: CSV.ToRecord a => FilePath -> [BL.ByteString] -> [a] -> IO ()
outputCsv path header f = BL.writeFile path $ BL.concat [BL.intercalate "," header, "\n", CSV.encode f]
showModule = A.renderLoadPackResult $ A.loadModulePacked subleqMA subleqMATextSection subleqModule subleqMAInitialMem
measureInstructions :: IO ()
measureInstructions = do
let n = 10000
putStrLn "Measure multu"
outputCsv "measure-subleq-multu.csv" ["arg1","arg2","parg1","parg2","insns"] =<< measureMultu n
putStrLn "Measure sra"
outputCsv "measure-subleq-sra.csv" ["arg1","arg2","insns"] =<< measureSra n
putStrLn "Measure srl"
outputCsv "measure-subleq-srl.csv" ["arg1","arg2","insns"] =<< measureSrl n
measureType "" measureBinaryWithP "and" ["arg1","arg2","parg1","parg2","insns"] n
measureType "" measureBinaryWithP "or" ["arg1","arg2","parg1","parg2","insns"] n
measureType "" measureBinaryWithP "xor" ["arg1","arg2","parg1","parg2","insns"] n
measureType "" measureBinaryWithP "nor" ["arg1","arg2","parg1","parg2","insns"] n
measureType "" measureShiftType "sll" ["arg1","arg2","insns"] n
measureType "" measureShiftType "srl" ["arg1","arg2","insns"] n
measureType "" measureShiftType "sra" ["arg1","arg2","insns"] n
measure "svi" measureSvi ["arg1","arg2","arg3","insns"] n
measure "lvui" measureLvui ["arg1","arg2","arg3","insns"] n
measureTest (measureSbiType 3) "sbi" ["arg1","arg2","insns"] n
measureTest (measureSbiType 3) "lbui" ["arg1","arg2","insns"] n
measureTest (measureSbiType 4) "shi" ["arg1","arg2","insns"] n
measureTest (measureSbiType 4) "lhui" ["arg1","arg2","insns"] n
measureTest measureAddrbType "addrb" ["arg1","insns"] n
measureTest measureAddrbType "addrh" ["arg1","insns"] n
where
arch = "subleq"
measure name func cols n = do
putStrLn $ "Measure " ++ toString name
outputCsv (mconcat ["measure-", arch, "-", name, ".csv"]) cols =<< func n
measureTest ty name = measure name (ty $ name `mappend` "Test")
measureType suf ty name = measure name (ty $ name `mappend` suf)
main :: IO ()
main = do
ok <- $quickCheckAll
args <- getArgs
-- if not ok then putStrLn "Verification Failed!" else return ()
unless ok $ putStrLn "Verification Failed!"
case args of
["measure"] -> measureInstructions
("read-trace":fs) -> forM_ fs $ T.readTraceFromFile "measure-subleq-" subleqProg
("read-traces":fs) -> T.readTraceFromFiles "measure-subleq.csv" subleqProg fs
_ -> error $ "Unknown options: " ++ show args