Progrsss on symbolic and fixes to x86-support.

base/src/Data/Macaw/Memory.hs

@@ -219,6 +219,9 @@ instance Ord (MemWord w) where
 -- | Typeclass for legal memory widths
 class (1 <= w) => MemWidth w where
 
+  -- | Returns @AddrWidthRepr@ to identify width of pointer.
+  --
+  -- The argument is ignored.
   addrWidthRepr :: p w -> AddrWidthRepr w
 
   -- | @addrWidthMod w@ returns @2^(8 * addrSize w - 1)@.

symbolic/src/Data/Macaw/Symbolic.hs

@@ -68,23 +68,27 @@ regVars sym nameFn a =
     _ -> error "internal: regVars encountered case non-exhaustive pattern"
 #endif
 
+-- | An override that creates a fresh value with the given type.
 runFreshSymOverride :: M.TypeRepr tp
                     -> C.OverrideSim MacawSimulatorState sym ret
                                      EmptyCtx
                                      (ToCrucibleType tp)
                                      (C.RegValue sym (ToCrucibleType tp))
-runFreshSymOverride = undefined
+runFreshSymOverride tp = do
+  undefined tp
 
-runReadMemOverride :: NatRepr w
+-- | Run override that reads a value from memory.
-                   -> M.MemRepr tp
+runReadMemOverride :: M.AddrWidthRepr w -- ^ Width of the address.
+                   -> M.MemRepr tp -- ^ Type of value to read.
                    -> C.OverrideSim MacawSimulatorState sym ret
                                     (EmptyCtx ::> C.BVType w)
                                     (ToCrucibleType tp)
                                     (C.RegValue sym (ToCrucibleType tp))
 runReadMemOverride = undefined
 
-runWriteMemOverride :: NatRepr w
+-- | Run override that writes a value to memory.
-                    -> M.MemRepr tp
+runWriteMemOverride :: M.AddrWidthRepr w -- ^ Width of a pointer
+                    -> M.MemRepr tp      -- ^ Type of value to write to memory.
                     -> C.OverrideSim MacawSimulatorState sym ret
                                      (EmptyCtx ::> C.BVType w ::> ToCrucibleType tp)
                                      C.UnitType
@@ -99,7 +103,6 @@ createHandleBinding ctx hid =
     MkFreshSymId repr -> runFreshSymOverride repr
     ReadMemId repr    -> runReadMemOverride (archWidthRepr ctx) repr
     WriteMemId repr   -> runWriteMemOverride (archWidthRepr ctx) repr
-    SyscallId         -> undefined
 
 -- | This function identifies all the handles needed, and returns
 -- function bindings for each one.
@@ -113,10 +116,9 @@ createHandleMap ctx = MapF.foldrWithKey go C.emptyHandleMap
            -> C.FunctionBindings MacawSimulatorState sym
            -> C.FunctionBindings MacawSimulatorState sym
         go hid (HandleVal h) b =
-          let o = C.mkOverride' (handleIdName hid) (handleIdRetType ctx hid) (createHandleBinding ctx hid)
+          let o = C.mkOverride' (handleIdName hid) (handleIdRetType hid) (createHandleBinding ctx hid)
            in  C.insertHandleMap h (C.UseOverride o) b
 
-
 mkMemSegmentBinding :: (1 <= w)
                     => C.HandleAllocator s
                     -> NatRepr w

symbolic/src/Data/Macaw/Symbolic/CrucGen.hs

@@ -368,7 +368,7 @@ mkHandleVal hid = do
     Nothing -> do
       ctx <- getCtx
       let argTypes = handleIdArgTypes ctx hid
-      let retType = handleIdRetType ctx hid
+      let retType = handleIdRetType hid
       hndl <- liftST $ C.mkHandle' (handleAlloc ctx) (handleIdName hid) argTypes retType
       crucPStateLens . handleMapLens %= MapF.insert hid (HandleVal hndl)
       pure $! hndl

symbolic/src/Data/Macaw/Symbolic/PersistentState.hs

@@ -59,6 +59,7 @@ module Data.Macaw.Symbolic.PersistentState
   ) where
 
 import           Control.Lens hiding (Index, (:>), Empty)
+import           Data.List (intercalate)
 import qualified Data.Macaw.CFG as M
 import qualified Data.Macaw.Memory as M
 import qualified Data.Macaw.Types as M
@@ -66,6 +67,7 @@ import           Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import           Data.Parameterized.Classes
 import           Data.Parameterized.Context
+import qualified Data.Parameterized.List as P
 import           Data.Parameterized.Map (MapF)
 import qualified Data.Parameterized.Map as MapF
 import           Data.Parameterized.NatRepr
@@ -83,9 +85,18 @@ import qualified Lang.Crucible.Types as C
 ------------------------------------------------------------------------
 -- Type mappings
 
+type family ToCrucibleBaseTypeList (l :: [M.Type]) :: Ctx C.BaseType where
+  ToCrucibleBaseTypeList '[] = EmptyCtx
+  ToCrucibleBaseTypeList (h ': l) = ToCrucibleBaseTypeList l ::> ToCrucibleBaseType h
+
 type family ToCrucibleBaseType (mtp :: M.Type) :: C.BaseType where
-  ToCrucibleBaseType (M.BVType w) = C.BaseBVType w
   ToCrucibleBaseType M.BoolType   = C.BaseBoolType
+  ToCrucibleBaseType (M.BVType w) = C.BaseBVType w
+  ToCrucibleBaseType ('M.TupleType l) = C.BaseStructType (ToCrucibleBaseTypeList l)
+
+type family CtxToCrucibleBaseType (mtp :: Ctx M.Type) :: Ctx C.BaseType where
+  CtxToCrucibleBaseType EmptyCtx   = EmptyCtx
+  CtxToCrucibleBaseType (c ::> tp) = CtxToCrucibleBaseType c ::> ToCrucibleBaseType tp
 
 type ToCrucibleType tp = C.BaseToType (ToCrucibleBaseType tp)
 
@@ -129,7 +140,11 @@ typeToCrucibleBase tp =
   case tp of
     M.BoolTypeRepr  -> C.BaseBoolRepr
     M.BVTypeRepr w  -> C.BaseBVRepr w
---    M.TupleTypeRepr a -> C.BaseStructRepr (macawAssignToCruc tpyeToCrucibleBase a)
+    M.TupleTypeRepr a -> C.BaseStructRepr (typeListToCrucibleBase a)
+
+typeListToCrucibleBase :: P.List M.TypeRepr ctx -> Assignment C.BaseTypeRepr (ToCrucibleBaseTypeList ctx)
+typeListToCrucibleBase P.Nil = Empty
+typeListToCrucibleBase (h P.:< r) = typeListToCrucibleBase r :> typeToCrucibleBase h
 
 typeToCrucible :: M.TypeRepr tp -> C.TypeRepr (ToCrucibleType tp)
 typeToCrucible = C.baseToType . typeToCrucibleBase
@@ -161,10 +176,10 @@ mkRegIndexMap :: OrdF r
               => Assignment r ctx
               -> Size (CtxToCrucibleType ctx)
               -> MapF r (IndexPair ctx)
-mkRegIndexMap r0 csz =
+mkRegIndexMap Empty _ = MapF.empty
-  case (r0, viewSize csz) of
+mkRegIndexMap (a :> r) csz =
-    (Empty, _) -> MapF.empty
+  case viewSize csz of
-    (a :> r, IncSize csz0) ->
+    IncSize csz0 ->
       let m = fmapF extendIndexPair (mkRegIndexMap a csz0)
           idx = IndexPair (nextIndex (size a)) (nextIndex csz0)
        in MapF.insert r idx m
@@ -201,12 +216,8 @@ data CrucGenContext arch s
      -- variable storing the base address.
    }
 
-archWidthRepr :: forall arch ids s . CrucGenContext arch s -> NatRepr (M.ArchAddrWidth arch)
+archWidthRepr :: forall arch s . CrucGenContext arch s -> M.AddrWidthRepr (M.ArchAddrWidth arch)
-archWidthRepr ctx = archConstraints ctx $
+archWidthRepr ctx = archConstraints ctx $ M.addrWidthRepr (archWidthRepr ctx)
-  let arepr :: M.AddrWidthRepr (M.ArchAddrWidth arch)
-      arepr = M.addrWidthRepr arepr
-   in M.addrWidthNatRepr arepr
-
 
 regStructRepr :: CrucGenContext arch s -> C.TypeRepr (ArchRegStruct arch)
 regStructRepr ctx = archConstraints ctx $
@@ -229,7 +240,6 @@ data HandleId arch (ftp :: (Ctx C.CrucibleType, C.CrucibleType)) where
                           '( EmptyCtx ::> ArchAddrCrucibleType arch ::> ToCrucibleType tp
                            , C.UnitType
                            )
-  SyscallId :: HandleId arch '(EmptyCtx ::> ArchRegStruct arch, ArchRegStruct arch)
 
 instance TestEquality (HandleId arch) where
   testEquality x y = orderingF_refl (compareF x y)
@@ -244,23 +254,27 @@ instance OrdF (HandleId arch) where
   compareF _ ReadMemId{} = GTF
 
   compareF (WriteMemId xr) (WriteMemId yr) = lexCompareF xr yr $ EQF
-  compareF WriteMemId{} _ = LTF
+--  compareF WriteMemId{} _ = LTF
-  compareF _ WriteMemId{} = GTF
+--  compareF _ WriteMemId{} = GTF
 
-  compareF SyscallId SyscallId = EQF
+typeName :: M.TypeRepr tp -> String
+typeName M.BoolTypeRepr = "Bool"
+typeName (M.BVTypeRepr w) = "BV" ++ show w
+typeName (M.TupleTypeRepr ctx) = "(" ++ intercalate "," (toListFC typeName ctx)  ++ ")"
+
+endName :: M.Endianness -> String
+endName M.LittleEndian = "le"
+endName M.BigEndian = "be"
 
 handleIdName :: HandleId arch ftp -> C.FunctionName
 handleIdName h =
   case h of
     MkFreshSymId repr ->
-      case repr of
+      fromString $ "symbolic_" ++ typeName repr
-        M.BoolTypeRepr -> "symbolicBool"
+    ReadMemId (M.BVMemRepr w end) ->
-        M.BVTypeRepr w -> fromString $ "symbolicBV" ++ show w
+      fromString $ "readMem_" ++ show (8 * natValue w) ++ "_" ++ endName end
-    ReadMemId (M.BVMemRepr w _) ->
+    WriteMemId (M.BVMemRepr w end) ->
-      fromString $ "readMem" ++ show (8 * natValue w)
+      fromString $ "writeMem_" ++ show (8 * natValue w) ++ "_" ++ endName end
-    WriteMemId (M.BVMemRepr w _) ->
-      fromString $ "writeMem" ++ show (8 * natValue w)
-    SyscallId -> "syscall"
 
 handleIdArgTypes :: CrucGenContext arch s
                  -> HandleId arch '(args, ret)
@@ -269,23 +283,18 @@ handleIdArgTypes ctx h =
   case h of
     MkFreshSymId _repr -> empty
     ReadMemId _repr -> archConstraints ctx $
-      empty :> C.BVRepr (archWidthRepr ctx)
+      empty :> C.BVRepr (M.addrWidthNatRepr (archWidthRepr ctx))
     WriteMemId repr -> archConstraints ctx $
-      empty :> C.BVRepr (archWidthRepr ctx)
+      empty :> C.BVRepr (M.addrWidthNatRepr (archWidthRepr ctx))
             :> memReprToCrucible repr
-    SyscallId ->
-      empty :> regStructRepr ctx
 
-handleIdRetType :: CrucGenContext arch s
+handleIdRetType :: HandleId arch '(args, ret)
-                -> HandleId arch '(args, ret)
                 -> C.TypeRepr ret
-handleIdRetType ctx h =
+handleIdRetType h =
   case h of
     MkFreshSymId repr -> typeToCrucible repr
     ReadMemId  repr -> memReprToCrucible repr
     WriteMemId _ -> C.UnitRepr
-    SyscallId -> regStructRepr ctx
-
 
 -- | A particular handle in the UsedHandleSet
 data HandleVal (ftp :: (Ctx C.CrucibleType, C.CrucibleType)) =

x86/support/macaw-x86-support.cabal

@@ -10,7 +10,7 @@ executable make_bsd_syscalls
   build-depends:
     base >= 4,
     bytestring,
-    language-c >= 0.6,
+    language-c >= 0.7,
     lens,
     pretty,
     containers,

x86/support/make_bsd_syscalls/Main.hs

@@ -81,7 +81,7 @@ syscallLine idents =
 
     parseDecl bytes =
       -- FIXME: we should maybe chain through newNameSupply?  I don't think it is ever used ...
-      case execParser extDeclP bytes (position 0 "" 0 0) idents newNameSupply of
+      case execParser extDeclP bytes (position 0 "" 0 0 Nothing) idents newNameSupply of
         Left _err                   -> Nothing
         Right (cdecl, _unusedNames) -> Just cdecl
 
@@ -248,7 +248,7 @@ main = do
 
   let (syscalls, split_headers) = splitFile (filter (not . BS.null) ls)
       headers = BS.intercalate "\n" split_headers
-      Right tunit  = parseC headers (position 0 "" 0 0)
+      Right tunit  = parseC headers (position 0 "" 0 0 Nothing)
       idents       = translUnitToIdents tunit
 
   ms <- mapM (parseSyscallLine idents) (tail syscalls)