Merge pull request #1000 from GaloisInc/aesimc

Update x86 backend to support the AESIMC instruction
GaloisInc · Jan 14, 2021 · 41b864a · 41b864a
2 parents 21565d7 + 83da326
commit 41b864a
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 7 deletions.
diff --git a/deps/macaw b/deps/macaw
diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs
@@ -201,18 +201,13 @@ cryptolUninterpreted ::
   SharedContext ->
   [Term] ->
   m Term
-cryptolUninterpreted env nm sc xs@[_, _] =
+cryptolUninterpreted env nm sc xs =
   case lookupIn nm $ eTermEnv env of
     Left _err -> throwX86 $ mconcat
       [ "Failed to lookup Cryptol name \"", nm
       , "\" in Cryptol environment"
       ]
     Right t -> liftIO $ scApplyAll sc t xs
-cryptolUninterpreted _ nm _ xs = throwX86 $ mconcat
-  [ "Type error in call to \"", nm
-  , "\": Expected 2 arguments, given ", show $ length xs
-  , " arguments"
-  ]
 
 -------------------------------------------------------------------------------
 -- ** Entrypoint
@@ -248,6 +243,7 @@ llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat se
       liftIO $ C.sawRegisterSymFunInterp sym (Macaw.fnAesDec sfs) $ cryptolUninterpreted cenv "aesdec"
       liftIO $ C.sawRegisterSymFunInterp sym (Macaw.fnAesDecLast sfs) $ cryptolUninterpreted cenv "aesdeclast"
       liftIO $ C.sawRegisterSymFunInterp sym (Macaw.fnAesKeyGenAssist sfs) $ cryptolUninterpreted cenv "aeskeygenassist"
+      liftIO $ C.sawRegisterSymFunInterp sym (Macaw.fnAesIMC sfs) $ cryptolUninterpreted cenv "aesimc"
       liftIO $ C.sawRegisterSymFunInterp sym (Macaw.fnClMul sfs) $ cryptolUninterpreted cenv "clmul"
 
       let preserved = Set.fromList . catMaybes $ stringToReg . Text.toLower . Text.pack <$> rwPreservedRegs rw
+1 −0		refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs
+118 −5		symbolic/src/Data/Macaw/Symbolic.hs
+1 −0		x86/src/Data/Macaw/X86.hs
+7 −0		x86/src/Data/Macaw/X86/ArchTypes.hs
+13 −0		x86/src/Data/Macaw/X86/Semantics/AESNI.hs
+12 −5		x86_symbolic/src/Data/Macaw/X86/Crucible.hs