Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Bitrotted example programs #324

Open
RyanGlScott opened this issue Feb 28, 2023 · 0 comments
Open

Bitrotted example programs #324

RyanGlScott opened this issue Feb 28, 2023 · 0 comments
Labels
ci documentation Documentation issues

Comments

@RyanGlScott
Copy link
Contributor

RyanGlScott commented Feb 28, 2023

The macaw repo has a number of small example programs that are not tested by CI. These have been overlooked when updating the code over time, and as such, they no longer compile:

  • The three programs in the symbolic/examples. These might be worth converting to executable stanzas in macaw-symbolic.cabal so that CI builds them.

  • The program given in the module Haddocks for Data.Macaw.Symbolic.Memory:

    -- >>> :{
    -- useCFG :: forall sym arch blocks
    -- . ( CB.IsSymInterface sym
    -- , MS.SymArchConstraints arch
    -- , 16 <= MC.ArchAddrWidth arch
    -- , Ord (WI.SymExpr sym WI.BaseIntegerType)
    -- , KnownNat (MC.ArchAddrWidth arch)
    -- )
    -- => CFH.HandleAllocator
    -- -- ^ The handle allocator used to construct the CFG
    -- -> sym
    -- -- ^ The symbolic backend
    -- -> MS.ArchVals arch
    -- -- ^ 'ArchVals' from a prior call to 'archVals'
    -- -> CS.RegMap sym (MS.MacawFunctionArgs arch)
    -- -- ^ Initial register state for the simulation
    -- -> MC.Memory (MC.ArchAddrWidth arch)
    -- -- ^ The memory recovered by macaw
    -- -> MS.LookupFunctionHandle sym arch
    -- -- ^ A translator for machine code addresses to function handles
    -- -> CC.CFG (MS.MacawExt arch) blocks (MS.MacawFunctionArgs arch) (MS.MacawFunctionResult arch)
    -- -- ^ The CFG to simulate
    -- -> IO ()
    -- useCFG hdlAlloc sym avals initialRegs mem lfh cfg =
    -- let ?recordLLVMAnnotation = \_ _ -> (pure () :: IO ())
    -- in MS.withArchEval avals sym $ \archEvalFns -> do
    -- let rep = CFH.handleReturnType (CC.cfgHandle cfg)
    -- memModelVar <- CLM.mkMemVar "macaw:llvm_memory" hdlAlloc
    -- (initialMem, memPtrTbl) <- MSM.newGlobalMemory (Proxy @arch) sym LDL.LittleEndian MSM.SymbolicMutable mem
    -- let mkValidityPred = MSM.mkGlobalPointerValidityPred memPtrTbl
    -- let extImpl = MS.macawExtensions archEvalFns memModelVar (MSM.mapRegionPointers memPtrTbl) lfh mkValidityPred
    -- let simCtx = CS.initSimContext sym CLI.llvmIntrinsicTypes hdlAlloc IO.stderr (CS.FnBindings CFH.emptyHandleMap) extImpl MS.MacawSimulatorState
    -- let simGlobalState = CSG.insertGlobal memModelVar initialMem CS.emptyGlobals
    -- let simulation = CS.regValue <$> CS.callCFG cfg initialRegs
    -- let initialState = CS.InitialState simCtx simGlobalState CS.defaultAbortHandler rep (CS.runOverrideSim rep simulation)
    -- let executionFeatures = []
    -- execRes <- CS.executeCrucible executionFeatures initialState
    -- case execRes of
    -- CS.FinishedResult {} -> return ()
    -- _ -> putStrLn "Simulation failed"
    -- :}

    This seems like a poor place to maintain this example, given how difficult it would be to test that it still compiles after making changes. Moreover, this code is almost identical to the code in the symbolic/examples/memory.hs example, so I think we should just point interested readers to that example in the module Haddocks.

    I think we should do something similar for the reference to symbolic/examples/simulation.hs here and a reference to symbolic/examples/translation.hs here.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
ci documentation Documentation issues
Projects
None yet
Development

No branches or pull requests

1 participant