SAW C 验证示例失败

Question

文档SAWScript Galois中有一个验证点积实现的例子。我得到一个错误：

dotprod.c:

#include <stdint.h>
#include <stdlib.h>

uint32_t dotprod(uint32_t *x, uint32_t *y, uint32_t size)
{
    uint32_t res = 0;
    for(size_t i = 0; i < size; i++) {
        res += x[i] * y[i];
    }
    return res;
}

dotprod.saw:

import "dotprod.cry";
m <- llvm_load_module "dotprod.bc";


xs <- fresh_symbolic "xs" {| [12][32] |};
ys <- fresh_symbolic "ys" {| [12][32] |};
let allocs = [ ("x", 12), ("y", 12) ];
let inputs = [ ("*x", xs, 12) , ("*y", ys, 12) , ("size", {{ 12:[32] }}, 1)     ];
let outputs = [(" return", 1)];

t <- llvm_symexec m "dotprod" allocs inputs outputs true;
thm1 <- abstract_symbolic {{ t == dotprod xs ys }};
prove_print thm1;

SAW脚本报错：

Loading module Cryptol
Loading file "dotprod.saw"
Loading module Main
saw: user error (Bitcode parsing of inc_file.bc failed:
not implemented
  from:
    FUNC_CODE_INST_GEP
    dotprod
    FUNCTION_BLOCK
    MODULE_BLOCK)

我使用：

SAW 版本 0.2
cryptol 版本 2.5.0
clang 版本 3.7

更新 1：

SAW 是从其 git 存储库重新编译的，我正在使用 stack version 1.5.1。

更新后错误改为：

Loading module Cryptol
Loading file "... /dotprod.saw"
Loading module Main
saw: user error ("llvm_symexec" (... /dotprod.saw:11:6):
"Parse error: \"expr\" (line 1, column 1):\nunexpected \" \"\nexpecting   \"*\", \"return\", \"args[\", letter, \"_\" or \"(\"")

Answer 1

问题已在 project's git site

上得到回答

解决方案片段

let outputs = [("return", 1)];

t <- llvm_symexec m "dotprod" allocs inputs outputs true;
thm1 <- abstract_symbolic {{ t == dotprod xs ys }};
prove_print abc thm1;

SAW C 验证示例失败

SAW C verification example fail

formal-verification

更新 1：