From 854b5ca5f69dc5e1f3588b88103ee79e7b275e0d Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Fri, 17 Sep 2021 11:09:09 -0700
Subject: [PATCH] Add support for `local`, `var` and `label` expressions in the
What4 module.
Some example specs generated these nodes. Note, however, that the support
for `local` here suffers from the same issue as the C code generator
and interpreter do regarding locals that may escape their scope
(CF https://github.com/Copilot-Language/copilot/issues/253).
---
copilot-theorem/src/Copilot/Theorem/What4.hs | 59 ++++++++++++--------
1 file changed, 35 insertions(+), 24 deletions(-)
diff --git a/copilot-theorem/src/Copilot/Theorem/What4.hs b/copilot-theorem/src/Copilot/Theorem/What4.hs
index 5bea6fe0..f9854aa1 100644
--- a/copilot-theorem/src/Copilot/Theorem/What4.hs
+++ b/copilot-theorem/src/Copilot/Theorem/What4.hs
@@ -152,16 +152,16 @@ prove solver spec = do
let bufLen (CS.Stream _ buf _ _) = genericLength buf
maxBufLen = maximum (0 : (bufLen <$> CS.specStreams spec))
prefix <- forM [0 .. maxBufLen - 1] $ \k -> do
- XBool p <- translateExpr sym (CS.propertyExpr pr) (AbsoluteOffset k)
+ XBool p <- translateExpr sym mempty (CS.propertyExpr pr) (AbsoluteOffset k)
return p
-- translate the induction hypothesis for all values up to maxBufLen in the past
ind_hyps <- forM [0 .. maxBufLen-1] $ \k -> do
- XBool hyp <- translateExpr sym (CS.propertyExpr pr) (RelativeOffset k)
+ XBool hyp <- translateExpr sym mempty (CS.propertyExpr pr) (RelativeOffset k)
return hyp
-- translate the predicate for the "current" value
- XBool p <- translateExpr sym (CS.propertyExpr pr) (RelativeOffset maxBufLen)
+ XBool p <- translateExpr sym mempty (CS.propertyExpr pr) (RelativeOffset maxBufLen)
-- compute the predicate (ind_hyps ==> p)
p' <- liftIO $ foldrM (WI.impliesPred sym) p ind_hyps
@@ -270,12 +270,12 @@ computeTriggerState ::
TransM t [(CE.Name, WB.BoolExpr t, [(Some CT.Type, XExpr t)])]
computeTriggerState sym spec = forM (CS.specTriggers spec) $
\CS.Trigger{ CS.triggerName = nm, CS.triggerGuard = guard, CS.triggerArgs = args } ->
- do XBool guard' <- translateExpr sym guard (RelativeOffset 0)
+ do XBool guard' <- translateExpr sym mempty guard (RelativeOffset 0)
args' <- mapM computeArg args
return (nm, guard', args')
where
computeArg CE.UExpr{ CE.uExprType = tp, CE.uExprExpr = ex } =
- do v <- translateExpr sym ex (RelativeOffset 0)
+ do v <- translateExpr sym mempty ex (RelativeOffset 0)
return (Some tp, v)
computeExternalInputs ::
@@ -551,36 +551,47 @@ computeStreamValue
AbsoluteOffset i
| i < 0 -> fail ("Invalid absolute offset " ++ show i ++ " for stream " ++ show id)
| i < len -> liftIO (translateConstExpr sym tp (genericIndex buf i))
- | otherwise -> translateExpr sym ex (AbsoluteOffset (i - len))
+ | otherwise -> translateExpr sym mempty ex (AbsoluteOffset (i - len))
RelativeOffset i
| i < 0 -> fail ("Invalid relative offset " ++ show i ++ " for stream " ++ show id)
| i < len -> let nm = "s" ++ show id ++ "_r" ++ show i
in liftIO (freshCPConstant sym nm tp)
- | otherwise -> translateExpr sym ex (RelativeOffset (i - len))
+ | otherwise -> translateExpr sym mempty ex (RelativeOffset (i - len))
where
len = genericLength buf
-translateExpr :: WB.ExprBuilder t st fs -> CE.Expr a -> StreamOffset -> TransM t (XExpr t)
-translateExpr sym e offset = case e of
+type LocalEnv t = Map.Map CE.Name (StreamOffset -> TransM t (XExpr t))
+
+translateExpr :: WB.ExprBuilder t st fs -> LocalEnv t -> CE.Expr a -> StreamOffset -> TransM t (XExpr t)
+translateExpr sym localEnv e offset = case e of
CE.Const tp a -> liftIO $ translateConstExpr sym tp a
CE.Drop _tp ix streamId -> getStreamValue sym streamId (addOffset offset ix)
CE.ExternVar tp nm _prefix -> getExternConstant sym tp nm offset
- CE.Op1 op e -> liftIO . translateOp1 sym op =<< translateExpr sym e offset
- CE.Op2 op e1 e2 -> do
- xe1 <- translateExpr sym e1 offset
- xe2 <- translateExpr sym e2 offset
- powFn <- gets pow
- logbFn <- gets logb
- liftIO $ translateOp2 sym powFn logbFn op xe1 xe2
- CE.Op3 op e1 e2 e3 -> do
- xe1 <- translateExpr sym e1 offset
- xe2 <- translateExpr sym e2 offset
- xe3 <- translateExpr sym e3 offset
- liftIO $ translateOp3 sym op xe1 xe2 xe3
- CE.Label _ _ _ -> error "translateExpr: Label unimplemented"
- CE.Local _ _ _ _ _ -> error "translateExpr: Local unimplemented"
- CE.Var _ _ -> error "translateExpr: Var unimplemented"
+ CE.Op1 op e1 ->
+ do xe1 <- translateExpr sym localEnv e1 offset
+ liftIO $ translateOp1 sym op xe1
+ CE.Op2 op e1 e2 ->
+ do xe1 <- translateExpr sym localEnv e1 offset
+ xe2 <- translateExpr sym localEnv e2 offset
+ powFn <- gets pow
+ logbFn <- gets logb
+ liftIO $ translateOp2 sym powFn logbFn op xe1 xe2
+ CE.Op3 op e1 e2 e3 ->
+ do xe1 <- translateExpr sym localEnv e1 offset
+ xe2 <- translateExpr sym localEnv e2 offset
+ xe3 <- translateExpr sym localEnv e3 offset
+ liftIO $ translateOp3 sym op xe1 xe2 xe3
+ CE.Label _ _ e1 ->
+ translateExpr sym localEnv e1 offset
+ CE.Local _tpa _tpb nm e1 body ->
+ do let f = translateExpr sym localEnv e1
+ let localEnv' = Map.insert nm f localEnv
+ translateExpr sym localEnv' body offset
+ CE.Var _tp nm ->
+ case Map.lookup nm localEnv of
+ Nothing -> fail ("translateExpr: unknown var " ++ show nm)
+ Just f -> f offset
getExternConstant ::
WB.ExprBuilder t st fs -> CT.Type a -> CE.Name -> StreamOffset -> TransM t (XExpr t)