initial commit

.docker/Dockerfile

@@ -0,0 +1,34 @@
+FROM node:latest
+
+LABEL maintaner "Sacha \"Giltho\" Ayoun"
+
+ARG DEBIAN_FRONTEND=noninteractive
+
+ENV LD_LIBRARY_PATH=/usr/local/lib:/usr/lib:/lib
+
+RUN apt-get update && apt-get install -y apt-utils
+
+RUN apt-get install -y \
+  build-essential \
+  curl \
+  git \
+  zsh \
+  m4
+
+RUN npm install -g [email protected] --unsafe-perm
+
+RUN mkdir /app
+
+WORKDIR /app
+
+RUN git clone https://github.com/GillianPlatform/javert-test262.git test262
+
+RUN git clone https://github.com/GillianPlatform/collections-c-for-gillian.git collections-c
+
+RUN git clone https://github.com/GillianPlatform/Gillian.git
+
+WORKDIR /app/Gillian
+
+RUN esy
+
+CMD [ "zsh" ]

.github/workflows/build.yml

@@ -0,0 +1,176 @@
+name: CI
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - master
+
+jobs:
+  build:
+    strategy:
+      matrix:
+        operating-system: [ macos-latest ]
+    runs-on: ${{ matrix.operating-system }}
+    steps:
+    - uses: actions/checkout@v2
+    - uses: actions/setup-node@v1
+    - name: Installing esy
+      run: npm install -g [email protected] --unsafe-perm
+    - name: Restore Cache
+      id: restore-cache
+      uses: actions/cache@v1
+      with:
+        path: _export
+        key:  ${{ runner.os }}-esy-${{ hashFiles('esy.lock/index.json') }}
+        restore-keys: |
+          ${{ runner.os }}-esy-
+    - name: Esy install
+      run: 'esy install'
+    - name: Import Cache
+      run: |
+        esy import-dependencies _export
+        rm -rf _export
+    - name: Esy build
+      run: 'esy build'
+      id: esy-build
+    - name: Format checking
+      run: 'esy format-check'
+    - name: Building release
+      run: 'esy release'
+    - name: Sending artifact for next jobs
+      uses: actions/upload-artifact@v1
+      with:
+        name: ${{ runner.os }}-release
+        path: _release
+    - name: Setting dependency cache
+      run: |
+        esy cleanup .
+        esy export-dependencies
+      if: steps.restore-cache.outputs.cache-hit != 'true'
+
+  gillian_c_tests:
+    strategy:
+      matrix:
+        operating-system: [ macos-latest ]
+    runs-on: ${{ matrix.operating-system }}
+    needs: build
+    steps:
+      - name: download release
+        uses: actions/download-artifact@v1
+        with:
+          name: ${{ runner.os }}-release
+          path: release
+      - name: setting up node
+        uses: actions/setup-node@v1
+      - name: install release
+        run: npm install -g ./release
+      - name: checkout project
+        uses: actions/checkout@v2
+        with:
+          path: Gillian
+      - name: init env
+        run: 'Gillian-C/scripts/setup_environment.sh'
+        working-directory: 'Gillian'
+      - name: Test All
+        run: './testAll.sh'
+        working-directory: 'Gillian/Gillian-C/environment/'
+
+  gillian_js_tests:
+    strategy:
+      matrix:
+        operating-system: [ macos-latest ]
+    runs-on: ${{ matrix.operating-system }}
+    needs: build
+    steps:
+      - name: download release
+        uses: actions/download-artifact@v1
+        with:
+          name: ${{ runner.os }}-release
+          path: release
+      - name: setting up node
+        uses: actions/setup-node@v1
+      - name: install release
+        run: npm install -g ./release
+      - name: checkout project
+        uses: actions/checkout@v2
+        with:
+          path: Gillian
+      - name: init env
+        run: 'Gillian-JS/scripts/setup_environment.sh'
+        working-directory: 'Gillian'
+      - name: Test JaVerT
+        run: './testJaVerT.sh'
+        working-directory: 'Gillian/Gillian-JS/environment/'
+
+  # test262:
+  #   strategy:
+  #     matrix:
+  #       operating-system: [ macos-latest ]
+  #   runs-on: ${{ matrix.operating-system }}
+  #   needs: build
+  #   steps:
+  #     - name: download release
+  #       uses: actions/[email protected]
+  #       with:
+  #         name: ${{ runner.os }}-release
+  #         path: release
+  #     - name: setting up node
+  #       uses: actions/[email protected]
+  #     - name: install release
+  #       run: npm install -g ./release
+  #     - name: checkout project
+  #       uses: actions/[email protected]
+  #       with:
+  #         repository:  giltho/javert-test262
+  #         path: test262
+  #     - name: Test262
+  #       run: 'gillian-js test262 test262/test --ci'
+
+  # collection-c:
+  #   strategy:
+  #     matrix:
+  #       operating-system: [ macos-latest ]
+  #   runs-on: ${{ matrix.operating-system }}
+  #   needs: build
+  #   steps:
+  #     - name: download release
+  #       uses: actions/download-artifact@v1
+  #       with:
+  #         name: ${{ runner.os }}-release
+  #         path: release
+  #     - name: setting up node
+  #       uses: actions/setup-node@v1
+  #     - name: install release
+  #       run: npm install -g ./release
+  #     - name: checkout project
+  #       uses: actions/checkout@v2
+  #       with:
+  #         repository:  giltho/collection-c-for-gillian
+  #         path: collection-c
+  #     - name: Symbolic Testing Collection-C
+  #       run: 'gillian-c bulk-wpst collection-c/for-gillian --ci'
+
+  # test-Buckets:
+  #   strategy:
+  #     matrix:
+  #       operating-system: [ macos-latest ]
+  #   runs-on: ${{ matrix.operating-system }}
+  #   needs: build
+  #   steps:
+  #     - name: download release
+  #       uses: actions/download-artifact@v1
+  #       with:
+  #         name: ${{ runner.os }}-release
+  #         path: release
+  #     - name: setting up node
+  #       uses: actions/setup-node@v1
+  #     - name: install release
+  #       run: npm install -g ./release
+  #     - name: checkout project
+  #       uses: actions/checkout@v2
+  #     - name: Symbolic Testing Buckets.js
+  #       run: 'gillian-js cosette-bulk Gillian-JS/Examples/Cosette/Buckets --ci'
+

.gitignore

@@ -0,0 +1,75 @@
+# Misc Editors
+*.autosave
+.*.swp
+.*.swo
+*~
+
+# Images
+*.png
+*.dot
+
+# examples
+
+# Eclipse
+TAGS
+.metadata
+.paths
+.project
+.projectSettings
+.settings
+
+# OCaml
+*.cma
+*.cmi
+*.cmo
+*.cmx
+*.o
+_build
+*.native
+*.byte
+*.merlin
+
+
+# Mac Rubbish
+.DS_Store
+
+config/config.xml
+src/localconfig.ml
+src/formula_parser/formula_lexer.ml
+src/formula_parser/formula_parser.ml
+src/formula_parser/formula_parser.mli
+tests/dot
+
+rosette/compiled
+
+# Racket
+racket/hp.rkt
+racket/test.rkt
+racket/wp.rkt
+racket/internals_builtins_procs.rkt
+racket/compiled
+
+# LaTeX nonsense
+*.blg
+*.bbl
+*.aux
+*.out
+*.log
+tutorial/main.pdf
+
+# esy + docker stuff
+node_modules
+_esy
+doc
+*.install
+_build.prev
+_release
+
+# gillian specific stuff
+*/environment
+*.env
+
+#Sacha Printing dependency graphs
+with-depgraph.esy.lock
+with-depgraph.json
+see_deps.py

.ocamlformat

@@ -0,0 +1,9 @@
+align-cases=true
+align-constructors-decl=true
+align-variants-decl=true
+assignment-operator=end-line
+break-before-in=fit-or-vertical
+break-cases=fit-or-vertical
+break-collection-expressions=fit-or-vertical
+break-fun-decl=smart
+break-fun-sig=smart

.vscode/c_cpp_properties.json

@@ -0,0 +1,19 @@
+{
+    "configurations": [
+        {
+            "name": "Mac",
+            "includePath": [
+                "${workspaceFolder}/**"
+            ],
+            "defines": [],
+            "macFrameworkPath": [
+                "/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/System/Library/Frameworks"
+            ],
+            "compilerPath": "/usr/bin/clang",
+            "cStandard": "c11",
+            "cppStandard": "c++17",
+            "intelliSenseMode": "clang-x64"
+        }
+    ],
+    "version": 4
+}

.vscode/cgil.code-snippets

@@ -0,0 +1,34 @@
+{
+	// Place your cgil workspace snippets here. Each snippet is defined under a snippet name and has a scope, prefix, body and
+	// description. Add comma separated ids of the languages where the snippet is applicable in the scope field. If scope
+	// is left empty or omitted, the snippet gets applied to all languages. The prefix is what is
+	// used to trigger the snippet and the body will be expanded and inserted. Possible variables are:
+	// $1, $2 for tab stops, $0 for the final cursor position, and ${1:label}, ${2:another} for placeholders.
+	// Placeholders with the same ids are connected.
+	// Example:
+	// "Print to console": {
+	// 	"scope": "javascript,typescript",
+	// 	"prefix": "log",
+	// 	"body": [
+	// 		"console.log('$1');",
+	// 		"$2"
+	// 	],
+	// 	"description": "Log output to console"
+	// }
+	"Symbolic int": {
+		"scope": "c",
+		"prefix": "symb_int",
+		"body": [
+			"int $1 = __builtin_annot_intval(\"symb_int\", $1);"
+		]
+	},
+	"Symbolic string 1": {
+		"scope": "c",
+		"prefix": "symb_str",
+		"body": [
+			"char $1 = (char) __builtin_annot_intval(\"symb_int\", $1);",
+			"ASSUME(-128 <= $1 && $1 <= 127 && $1 != 0);",
+			"char str_$1[] = { $1, '\\0' };"
+		]
+	}
+}

.vscode/settings.json

@@ -0,0 +1,11 @@
+{
+  "search.exclude": {
+    "esy.lock/**": true
+  },
+  "files.associations": {
+    "stdlib.h": "c",
+    "stdio.h": "c",
+    "slist.h": "c",
+    "algorithm": "c"
+  }
+}