3

I have a static-length list of values ks :: [SInt16] and an index x :: SInt16. I'd like to index into the list using x:

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

I would expect to be able to use (.!) with a sufficiently constrained x like this:

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

However, this fails with the error coming from (.!).

Of course, in my real program, I use (.!) all over the place in locations where there is no suitable default value to use in select. How can I index into a list with a constrained-to-be-in-bounds index?

4

1 回答 1

3

简单的解决方案

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'

现在假设您尝试执行 a 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 求解器总是可以“聪明地”选择值来给你意想不到的模型。这样，您至少可以保护自己免受最明显的错误的侵害。在生产系统中，我坚持使用第三种方法，因为在实践中调试由于复杂约束而出现的错误可能相当困难。您为自己留下的“跟踪”变量越多越好。

于 2020-07-02T05:00:29.997 回答