Skip to content

Commit

Permalink
x86-symbolic: Structured exceptions for missing primitive function se…
Browse files Browse the repository at this point in the history
…mantics
  • Loading branch information
langston-barrett committed Jan 23, 2024
1 parent 5f8300b commit a023434
Showing 1 changed file with 17 additions and 16 deletions.
33 changes: 17 additions & 16 deletions x86_symbolic/src/Data/Macaw/X86/Crucible.hs
Original file line number Diff line number Diff line change
Expand Up @@ -134,6 +134,7 @@ withConcreteCountAndDir state val_size wrapped_count _wrapped_dir func =
data MissingSemantics
= MissingStmtSemantics String
| MissingTermSemantics String
| MissingPrimFnSemantics String
deriving Show

instance Exception MissingSemantics
Expand Down Expand Up @@ -373,13 +374,13 @@ pureSem sym fn = do
do x <- getPointerOffset x0
evalE sym $ app $ Not $ foldr1 xor [ bvTestBit x i | i <- [ 0 .. 7 ] ]
where xor a b = app (BoolXor a b)
M.ReadFSBase -> error " ReadFSBase"
M.ReadGSBase -> error "ReadGSBase"
M.GetSegmentSelector _ -> error "GetSegmentSelector"
M.CPUID{} -> error "CPUID"
M.CMPXCHG8B{} -> error "CMPXCHG8B"
M.RDTSC{} -> error "RDTSC"
M.XGetBV {} -> error "XGetBV"
M.ReadFSBase -> throw (MissingPrimFnSemantics "ReadFSBase")
M.ReadGSBase -> throw (MissingPrimFnSemantics "ReadGSBase")
M.GetSegmentSelector _ -> throw (MissingPrimFnSemantics "GetSegmentSelector")
M.CPUID{} -> throw (MissingPrimFnSemantics "CPUID")
M.CMPXCHG8B{} -> throw (MissingPrimFnSemantics "CMPXCHG8B")
M.RDTSC{} -> throw (MissingPrimFnSemantics "RDTSC")
M.XGetBV {} -> throw (MissingPrimFnSemantics "XGetBV")
M.PShufb sw (AtomWrapper vxs) (AtomWrapper vys) ->
case sw of
M.SIMDByteCount_XMM
Expand All @@ -390,9 +391,9 @@ pureSem sym fn = do
let res = DV.fromList $ V.toList $ shuffleB xs ys
mapM (llvmPointer_bv (symIface sym) <=< evalE sym) res
_ -> error "PShufb is not implemented for 64-bit operands"
M.MemCmp{} -> error "MemCmp"
M.RepnzScas{} -> error "RepnzScas"
M.MMXExtend {} -> error "MMXExtend"
M.MemCmp{} -> throw (MissingPrimFnSemantics "MemCmp")
M.RepnzScas{} -> throw (MissingPrimFnSemantics "RepnzScas")
M.MMXExtend {} -> throw (MissingPrimFnSemantics "MMXExtend")
M.X86IDivRem w num1 num2 d -> do
sDivRem sym w num1 num2 d
M.X86DivRem w num1 num2 d -> do
Expand Down Expand Up @@ -465,11 +466,11 @@ pureSem sym fn = do
iSBVToFloat symi (floatInfoFromSSEType tp) RNE
=<< toValBV bak x

M.X87_Extend{} -> error "X87_Extend"
M.X87_FAdd{} -> error "X87_FAdd"
M.X87_FSub{} -> error "X87_FSub"
M.X87_FMul{} -> error "X87_FMul"
M.X87_FST {} -> error "X87_FST"
M.X87_Extend{} -> throw (MissingPrimFnSemantics "X87_Extend")
M.X87_FAdd{} -> throw (MissingPrimFnSemantics "X87_FAdd")
M.X87_FSub{} -> throw (MissingPrimFnSemantics "X87_FSub")
M.X87_FMul{} -> throw (MissingPrimFnSemantics "X87_FMul")
M.X87_FST {} -> throw (MissingPrimFnSemantics "X87_FST")

M.VOp1 w op1 x ->
case op1 of
Expand Down Expand Up @@ -570,7 +571,7 @@ pureSem sym fn = do
vecOp2 sym LittleEndian (natMultiply elNum elSz) elSz v1 v2 $ \xs ys ->
V.zipWith (semPointwise op elSz) xs ys

M.VExtractF128 {} -> error "VExtractF128"
M.VExtractF128 {} -> throw (MissingPrimFnSemantics "VExtractF128")

M.CLMul x y ->
do let f = fnClMul (symFuns sym)
Expand Down

0 comments on commit a023434

Please sign in to comment.