Skip to content

Commit

Permalink
Make crucible_fresh_pointer work for pointers to non-memtypes.
Browse files Browse the repository at this point in the history
Fixes #193.
  • Loading branch information
Brian Huffman committed Aug 4, 2017
1 parent a252549 commit 6b21e65
Showing 1 changed file with 15 additions and 6 deletions.
21 changes: 15 additions & 6 deletions src/SAWScript/CrucibleBuiltins.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1007,6 +1007,15 @@ memTypeForLLVMType _bic lty =
Just m -> return m
Nothing -> fail ("unsupported type: " ++ show (L.ppType lty))

symTypeForLLVMType :: BuiltinContext -> L.Type -> CrucibleSetup Crucible.SymType
symTypeForLLVMType _bic lty =
do cctx <- getCrucibleContext
let lc = ccLLVMContext cctx
let ?lc = Crucible.llvmTypeCtx lc
case TyCtx.liftType lty of
Just m -> return m
Nothing -> fail ("unsupported type: " ++ show (L.ppType lty))

-- | See 'crucible_fresh_expanded_val'
--
-- This is the recursively-called worker function.
Expand All @@ -1027,7 +1036,7 @@ constructExpandedSetupValue sc t =

Crucible.PtrType symTy ->
case TyCtx.asMemType symTy of
Just memTy -> constructFreshPointer memTy
Just memTy -> constructFreshPointer (Crucible.MemType memTy)
Nothing -> fail ("lhs not a valid pointer type: " ++ show symTy)

Crucible.ArrayType n memTy ->
Expand Down Expand Up @@ -1061,13 +1070,13 @@ crucible_fresh_pointer ::
L.Type ->
CrucibleSetup SetupValue
crucible_fresh_pointer bic _opt lty =
do memTy <- memTypeForLLVMType bic lty
constructFreshPointer memTy
do symTy <- symTypeForLLVMType bic lty
constructFreshPointer symTy

constructFreshPointer :: Crucible.MemType -> CrucibleSetup SetupValue
constructFreshPointer memTy =
constructFreshPointer :: Crucible.SymType -> CrucibleSetup SetupValue
constructFreshPointer symTy =
do n <- csVarCounter <<%= nextAllocIndex
currentState.csFreshPointers.at n ?= Crucible.MemType memTy
currentState.csFreshPointers.at n ?= symTy
return (SetupVar n)

crucible_points_to ::
Expand Down

0 comments on commit 6b21e65

Please sign in to comment.