JT Paasch jtpaasch

C++ BNF Grammar

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

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

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

Some useful resources on this matter:

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:

	// 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.

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

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

	*/

	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)

	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)

	-- 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