jtpaasch

#include "library.dl"

// =========================================================
// EXAMPLE
// =========================================================
 
/*

------------------------------------------------------------
THE PROGRAM

jtpaasch

// Here's one way to use Souffle datalog to simulate
// reading bytes from memory and assembling a value
// out of them (big/little endian-wise).

// Working with string representations of binary numbers
// in Souffle is somewhat tedious, so I'm going to do
// this by storing bytes as numbers. Then, when I pull
// out the bytes and assemble them into a value, I just
// need to calculate the number from that sequence of
// integer byte values.

jtpaasch

C++ BNF Grammar

The C++ grammar is convoluted. These notes offer a quickstart/bird's eye view into it.

BNF grammars

Here are some versions of the grammar (or C-variants):

• https://alx71hub.github.io/hcb/

jtpaasch

Clang AST parsing

Quick start for using Clang to parse C++ and get an AST.

Some useful resources on this matter:

• https://shaharmike.com/cpp/libclang/
• https://bastian.rieck.me/blog/posts/2015/baby_steps_libclang_ast/
• https://clang.llvm.org/doxygen/group__CINDEX.html

jtpaasch

/*
=======================================================
01 - Arithmetic expressions
=======================================================

Encoding arithmetic expressions and simple assignments with datalog.
The language is a subset of the one in PPA, pp. 3-4.

*/

jtpaasch

#include <iostream>

using namespace std;

typedef struct list {
    struct list * n;
    int d;
} list;

void insert(list * l, int d) {

jtpaasch

module Main where

import qualified Control.Monad.State as M
import qualified Data.Array as A
import System.Random (StdGen, mkStdGen, randomR)


-- In a tic-tac-toe game, there is an 'X' player, and an 'O' player
data Player = PlayerO | PlayerX deriving (Eq, Show)

jtpaasch

module Main where

import qualified Data.Text as T
import qualified Text.Parsec.Pos as P
import qualified Data.SCargot as S
import qualified Data.SCargot.Common as C
import qualified Data.SCargot.Language.Basic as B
import qualified Data.SCargot.Repr.WellFormed as W

type Sexp = W.WellFormedExpr (C.Located T.Text)

jtpaasch

-- This version of fold applies 'f' to the head of the list '[a]' 
-- to get a new accumulation 'acc', then it recurses into the tail
-- of the list '[a]' where it then repeats. This means that the
-- accumulated results are built up by adding in the elements 
-- of the list, one at a time, starting with the first element 
-- (on the left), and then moving through them, going right.
foldLeft :: (b -> a -> b) -> b -> [a] -> b
foldLeft f acc xs =
  case xs of
    [] -> acc

jtpaasch

Relational Verification

Beckert, B. and M. Ulbrich. (2018) "Trends in Relational Program Verification." In I. Schaefer and P. Muller (Eds.), Principled Software Development: Essays Dedicated to Arnd Poetzsch-Heffter on the Occasion of His 60th Birthday. Springer, pp. 41-58.

Relational verification verifies relational properties that relate different programs.

To verify relational properties, one must (in principle) compare several runs of the same program.

Some examples of relational properties: