GitHub - au-ts/gordian

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 207 Commits
.github/workflows		.github/workflows
demo/arith_sum		demo/arith_sum
examples		examples
reports		reports
tests		tests
.envrc		.envrc
.gitignore		.gitignore
Dockerfile		Dockerfile
LICENSE		LICENSE
README		README
abc_cfg.py		abc_cfg.py
add.txt		add.txt
assume_prove.py		assume_prove.py
check-gen-test-results.py		check-gen-test-results.py
copy-prelude.smt2		copy-prelude.smt2
copy_spec.py		copy_spec.py
dot_graph.py		dot_graph.py
dsa.py		dsa.py
error_reporting.py		error_reporting.py
eval_point.py		eval_point.py
gen.py		gen.py
ghost_code.py		ghost_code.py
ghost_data.py		ghost_data.py
ghost_data_helpers.py		ghost_data_helpers.py
handler_loop_ghost.py		handler_loop_ghost.py
irreducible_loops.txt		irreducible_loops.txt
lc_helper.py		lc_helper.py
logic.py		logic.py
main.py		main.py
make-graph-from-c.sh		make-graph-from-c.sh
microkit-manual-prelude.smt2		microkit-manual-prelude.smt2
microkit-prelude.smt2		microkit-prelude.smt2
microkit_spec.py		microkit_spec.py
monitor-manual-prelude.smt2		monitor-manual-prelude.smt2
monitor_spec.py		monitor_spec.py
nip.py		nip.py
parser_combinator.py		parser_combinator.py
plan.txt		plan.txt
potential_undefined_behaviour_explanation.txt		potential_undefined_behaviour_explanation.txt
pre-commit		pre-commit
provenance.py		provenance.py
pytest.ini		pytest.ini
sel4cp-manual-prelude.smt2		sel4cp-manual-prelude.smt2
sel4cp-prelude.smt2		sel4cp-prelude.smt2
sel4cp_spec.py		sel4cp_spec.py
shell.nix		shell.nix
smt.py		smt.py
smt_parser.py		smt_parser.py
source.py		source.py
split_prove_nodes.py		split_prove_nodes.py
sublime-smt-argument.txt		sublime-smt-argument.txt
syntax.py		syntax.py
target_objects.py		target_objects.py
test_dsa.py		test_dsa.py
test_examples.py		test_examples.py
test_nip.py		test_nip.py
test_parser_combinator.py		test_parser_combinator.py
test_reducible_check.py		test_reducible_check.py
test_smt_parser.py		test_smt_parser.py
test_source.py		test_source.py
utils.py		utils.py
validate_dsa.py		validate_dsa.py

Repository files navigation

Undefined behavior C
====================

Setup
-----

Install the pre commit hook.

    ln -s "$PWD/pre-commit" .git/hooks/pre-commit

Install pytest and dot (for visualizing the CFG)

Run the tests:

    pytest

Type verification:

    mypy --strict .

Code formatting:

    find -name '*.py' | xargs autopep8 -i

Usage
-----

To convert C to graph lang

    env TV_ROOT=... L4V_ARCH=RISCV64 bash make-graph-from-c.sh <in.c> <out.txt>

To use ubc:

    usage: python3 main.py [options] <graphfile.txt> function-names...

      --show-graph: Show the graph lang
      --show-dsa: Show the graph after having applied dynamic single assignment
      --show-ap: Show the assume prove prog
      --show-smt: Show the SMT given to the solvers
      --show-sats: Show the raw results from the smt solvers (sat/unsat)