低レイヤのプログラムの形式検証ツール

opam repo add coq-released "https://coq.inria.fr/opam/released"
opam repo add iris-dev "https://gitlab.mpi-sws.org/iris/opam.git"
opam update
opam pin add -n -y cerberus "git+https://github.com/rems-project/cerberus.git#b60ea9a7d30dfa7f048c2b312dd86547939a035a"
opam pin add refinedc "git+https://gitlab.mpi-sws.org/iris/refinedc.git"

refinedc init

#include <refinedc.h>
[[rc::parameters("a : loc", "b : loc", "n : Z", "m : Z")]]
[[rc::args("a @ &own<n @ int<i32>>", "b @ &own<m @ int<i32>>")]]
[[rc::ensures("own a : m @ int<i32>", "own b : n @ int<i32>")]]
void swap(int *a, int *b)
{
	int tmp = *a;
	*a = *b;
	*b = tmp;
}

refinedc check swap.c

docker run -it diffblue/cbmc:5.71.0

int main() {
	char buf[3] = {'a', 'b', 'c'};
	buf[3] = 'd';
}

cbmc --bounds-check --pointer-check cbmc_sample.c --show-properties

opam install coq-vst coq-compcert

// swap.c
void swap(int *a, int *b)
{
	int tmp = *a;
	*a = *b;
	*b = tmp;
}
int main()
{
	int x = 1, y = 2;
	swap(&x, &y);
	return x;
}

clightgen swap.c

Definition swap_spec : ident * funspec :=
DECLARE _swap
WITH sh: share, a: val, b: val, a_val: Z, b_val: Z
  PRE [ tptr tint, tptr tint ]
    PROP (writable_share sh)
    PARAMS (a; b)
    SEP (data_at sh tint (Vint (Int.repr a_val)) a; data_at sh tint (Vint (Int.repr b_val)) b)
  POST [ tvoid ] (
    PROP()
    RETURN()
    SEP (data_at sh tint (Vint (Int.repr b_val)) a; data_at sh tint (Vint (Int.repr a_val)) b)
  ).

Definition main_spec :=
 DECLARE _main
  WITH gv : globals
  PRE [] main_pre prog tt gv
  POST [ tint ]
     PROP()
     RETURN (Vint (Int.repr 2))
     SEP(TT).

Lemma body_swap: semax_body Vprog Gprog f_swap swap_spec.
Proof.
  start_function.
  try repeat forward.
  entailer!.
Qed.

(* swap_verify.v *)
Require Import VST.floyd.proofauto.
Require Import swap.
Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs.  mk_varspecs prog. Defined.

Definition swap_spec : ident * funspec :=
DECLARE _swap
WITH sh: share, a: val, b: val, a_val: Z, b_val: Z
  PRE [ tptr tint, tptr tint ]
    PROP (writable_share sh)
    PARAMS (a; b)
    SEP (data_at sh tint (Vint (Int.repr a_val)) a; data_at sh tint (Vint (Int.repr b_val)) b)
  POST [ tvoid ] (
    PROP()
    RETURN()
    SEP (data_at sh tint (Vint (Int.repr b_val)) a; data_at sh tint (Vint (Int.repr a_val)) b)
  ).

Definition main_spec :=
 DECLARE _main
  WITH gv : globals
  PRE [] main_pre prog tt gv
  POST [ tint ]
     PROP()
     RETURN (Vint (Int.repr 2))
     SEP(TT).

Definition Gprog := [swap_spec; main_spec].

Lemma body_swap: semax_body Vprog Gprog f_swap swap_spec.
Proof.
  start_function.
  try repeat forward.
  entailer!.
Qed.

./isabelle/bin/isabelle jedit -d ./l4v -l CParser CParserExample.thy

theory CParserExample
  imports CParser.CTranslation
begin
install_C_file "path/to/c_src.c"

context c_src_global_addresses
begin
    thm f_your_function_body
end

// a.c
void f(void) {}

(* CParserVerySimpleExample.thy *)
theory CParserVerySimpleExample
  imports CParser.CTranslation
begin
install_C_file "a.c"
theorem (in a_global_addresses) shows "\Gamma \turnstile {| True |} PROC f() {| True |}"
    apply vcg
    done

opam install frama-c

/*@
   requires \valid(a);
   requires \valid(b);
   assigns *a;
   assigns *b;
   ensures *a == \old(*b);
   ensures *b == \old(*a);
*/
void swap(int *a, int* b);

void swap(int *a, int *b)
{
	int tmp = *a;
	*a = *b;
	*b = tmp;
}

frama-c -wp swap.c

mkdir $workdir && cd $workdir
git clone https://github.com/Microsoft/checkedc-clang src
cd src/llvm/projects/checkedc-wrapper/
git clone https://github.com/Microsoft/checkedc
cd $workdir
cmake -G Ninja -DLLVM_ENABLE_PROJECTS=clang \
          -DCMAKE_INSTALL_PREFIX=./install \
          -DCMAKE_BUILD_TYPE=Release \
          -DLLVM_ENABLE_ASSERTIONS=ON \
          -DLLVM_CCACHE_BUILD=ON \
          -DLLVM_INSTALL_TOOLCHAIN_ONLY=ON \
          -DLLVM_TARGETS_TO_BUILD="X86" \
          -DLLVM_LIT_ARGS=-v \
          ./src/llvm
ninja

#include <stdio.h>
#include <stdchecked.h>

struct BinTree _For_any(T) {
    T *elm;
    struct BinTree<T> *left;
    struct BinTree<T> *right;
};

_For_any(T) struct BinTree<T> new_bintree(T *elm) {
    struct BinTree<T> t =  {
        .elm = elm,
        .left = NULL,
        .right = NULL,
    };↲
    return t;
}

int main() {
    int e = 1;↲
    struct BinTree<int> t = new_bintree<int>(&e);
    printf("%i\n", *t.elm);
}

wget https://github.com/verifast/verifast/releases/download/nightly/verifast-21.04-118-gc2cdad9a-linux.tar.gz
tar xf verifast-21.04-118-gc2cdad9a-linux.tar.gz
./verifast-21.04-118-gc2cdad9a-linux/bin/verifast --help

void swap(int *a, int *b)
//@requires *a |-> ?x &*& *b |-> ?y;
//@ensures *a |-> y &*& *b |-> x;
{
	int tmp = *a;
	*a = *b;
	*b = tmp;
}

path/to/verifast -shared verifast_swap.c