越界 `select` 即使我`约束`索引答案

【问题标题】：Out-of-bounds `select` even though I `constrain` the index越界 `select` 即使我`约束`索引
【发布时间】：2020-07-01 23:56:07
【问题描述】：

我有一个静态长度的值列表ks :: [SInt16] 和一个索引x :: SInt16。我想使用x 索引到列表中：

(.!) :: (Mergeable a) => [a] -> SInt16 -> a
xs .! i = select xs (error "(.!) : out of bounds") i

我希望能够像这样使用 (.!) 和充分受限的 x：

sat $ do
    let ks = [1, 3, 5, 2, 4]      

    x <- sInt16 "x"
    constrain $ 0 .<= x .&& x .< literal (fromIntegral $ length ks)

    let y = ks .! x
    return $ y .< x

但是，这失败了，错误来自(.!)。

当然，在我的实际程序中，我在没有合适的默认值可在select 中使用的位置处处处使用(.!)。 如何将索引限制在索引范围内的列表中？

【问题讨论】：

标签： haskell smt sbv symbolic-execution

【解决方案1】：

简单的解决方案

select 在符号执行期间被 SBV 完全扩展，因此您必须提供正确的默认值，正如您所发现的。因此，如果您确实想使用 select，您必须在此处找到一个实际值。

为了满足您的迫切需求，我建议您简单地定义：

(.!) :: (Mergeable a) => [a] -> SInt16 -> a
[]       .! _ = error "(.!): Empty list!"
xs@(x:_) .! i = select xs x i

只要您确保已对 i 声明了足够的约束，这应该可以正常工作。

稍微好一点的方法

以上要求您的用户跟踪对索引变量的适当约束，这可能会变得相当麻烦。在这些情况下使用的一个简单技巧是改用“智能”构造函数。先定义：

import Data.SBV

mkIndex :: SIntegral b => String -> [a] -> Symbolic (SBV b)
mkIndex nm lst = do i <- free nm
                    constrain $ 0 .<= i .&& i .< literal (fromIntegral (length lst))
                    pure i

(.!) :: (Mergeable a) => [a] -> SInt16 -> a
[]       .! _ = error "(.!): Empty list!"
xs@(x:_) .! i = select xs x i

现在你可以说：

p = sat $ do let ks = [1, 3, 5, 2, 4]

             x <- mkIndex "x" ks

             let y = ks .! x
             return $ y .< x

这只是比你原来的更冗长（因为你需要传递你想要索引到的列表），但它可以省去很多麻烦。此外，您可以更改您的 mkIndex 以进行诊断，或根据需要声明进一步的约束。

更具防御性的方法

上述“更好”的方法要求您提前知道要编入索引的列表的长度。这在您的示例中很明显，但我可以想象这些信息不容易获得的情况。如果是这种情况，我建议实际为越界访问元素创建一个符号值，并自己明确地跟踪它。这更复杂，但您可以将大部分内容隐藏在简单的数据类型后面。比如：

{-# LANGUAGE ScopedTypeVariables #-}

import Data.SBV

newtype Index a b = Index (SBV a, SBV b)

mkIndex :: (SymVal a, SymVal b) => String -> Symbolic (Index a b)
mkIndex nm = do def <- free $ nm ++ "_access_out_of_bounds_value"
                idx <- free nm
                pure $ Index (def, idx)

(.!) :: (SymVal a, SIntegral b) => [SBV a] -> Index a b -> SBV a
xs .! Index (i, i') = select xs i i'

现在假设您尝试执行sat，但对索引设置了不正确的约束：

p = sat $ do let ks = [1, 3, 5, 2, 4]

             xi@(Index (_, x)) :: Index Int16 Int16 <- mkIndex "x"

             -- incorrectly constrain x here to do out-of-bounds
             constrain $ x .> 10

             let y = ks .! xi

             pure $ y .< x

你会得到：

*Main> p
Satisfiable. Model:
  x_access_out_of_bounds_value =     0 :: Int16
  x                            = 16386 :: Int16

这样，您可以看到出现了问题，以及求解器选择了什么值来满足访问越界的情况。

总结

您采用哪种方法实际上取决于您的实际需求。但如果可能的话，我建议至少选择第二种选择，因为 SMT 求解器总是可以“聪明地”选择值来给你意想不到的模型。这样，您至少可以保护自己免受最明显的错误的侵害。在生产系统中，我坚持使用第三种方法，因为在实践中调试由于复杂约束而出现的错误可能相当困难。留给自己的“跟踪”变量越多越好。

【讨论】：