Rebase on master of original repo

.github/workflows/build.yaml

@@ -1,6 +1,8 @@
 name: CI Build
 
 on:
+  schedule:
+    - cron: "0 3 * * 0"
   push:
     branches: [ '**' ]
   pull_request:
@@ -13,46 +15,53 @@ env:
 jobs:
   build:
     name: Build
-    runs-on: ubuntu-20.04
+    runs-on: ${{ matrix.os }}
 
     strategy:
       matrix:
-        polyml: ['v5.7.1', 'v5.8.1']
+        os: ['ubuntu-22.04']
+        polyml: [{version: 'PREPACKAGED'}, {version: 'v5.9.2', heapless: '1'}]
+        z3: ['4.13.4']
+        hol4: ['trindemossen-2']
 
     env:
-      HOLBA_POLYML_VERSION: ${{ matrix.polyml }}
+      HOLBA_POLYML_VERSION: ${{ matrix.polyml.version }}
+      HOLBA_POLYML_HEAPLESS: ${{ matrix.polyml.heapless }}
+      HOLBA_Z3_VERSION: ${{ matrix.z3 }}
+      HOLBA_Z3_ASSET_SUFFIX: '-x64-glibc-2.35.zip'
+      HOLBA_HOL4_VERSION: ${{ matrix.hol4 }}
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v2
+        uses: actions/checkout@v4
 
       - name: Cache dependencies
         id: cache-deps
-        uses: actions/cache@v2
+        uses: actions/cache@v3
         with:
           path: |
             ${{ env.HOLBA_OPT_DIR }}
-          key: os-${{ runner.os }}_polyml-${{ matrix.polyml }}_hol4-k14
+          key: os-${{ matrix.os }}_polyml-${{ matrix.polyml.version }}_z3-${{ matrix.z3 }}_hol4-${{ matrix.hol4 }}
 
       - name: Static analysis
         timeout-minutes: 5
         run: |
           ./scripts/ci/static-analysis.sh || echo "Static-analysis failed with status $?."
 
       - name: Prepare cached dependencies
-        timeout-minutes: 35
+        timeout-minutes: 45
         run: |
           ./scripts/setup/install_base.sh
           ./scripts/setup/install_z3.sh
 
       - name: Configure and compile
-        timeout-minutes: 35
+        timeout-minutes: 55
         run: |
           ./configure.sh
-          ./scripts/ci/run_make.sh main
+          ./scripts/ci/run_holmake.sh
 
       - name: Run tests
-        timeout-minutes: 35
+        timeout-minutes: 65
         run: |
           ./scripts/ci/run_make.sh tests
 

.gitignore

@@ -1,17 +1,8 @@
 # Compiled HOL files
-.HOLMK
-.hollogs
-*Theory.dat
-*Theory.sig
-*Theory.sml
-*.ui
-*.uo
 *~
 *.exe
 *-heap
-
-# Generated Holmake files
-Holmakefile
+.hol/
 
 # Makefile related stuff
 Makefile.local

.holpath

@@ -0,0 +1 @@
+HOLBADIR

CONTRIBUTING.md

@@ -1,67 +1,54 @@
-## Coding style
+# Contribution guide for the HolBA library
 
-* like HOL source code
-  - Spaces, no tabs
-  - No unicode
-  - `snake_case` (e.g. `bir_number_of_mem_splits_def`)
+## Coding style
 
+Like HOL4 source code:
 
-## Branch policy
+- Spaces, no tabs
+- No unicode
+- `snake_case` (e.g., `bir_number_of_mem_splits_def`)
 
-### `master` branch
+## Branch and tag policy
 
-`master` is the branch where every feature is available, but not necessarily finalized:
- - Can cheat, but has to be avoided (cheats are reported by the CI in Pull Requests)
-   - You must explicitely say why you cheated if it's not too obvious
- - Code should not be be commented out
- - Our CI must pass
-   - **Holmake must work** (i.e. must correctly compile)
-   - All tests must succeed
- - Bug-fixing commits are ok
- - At least 1 accepting review is needed in order to merge into `master`
+- The `master` is the branch where every feature is available, but not necessarily finalized
+- No development happens on the `master` branch, but rather on separate topic branches,
+  either inside the repository or in repository forks
+- When your changes are ready to be integrated into `master`, open a Pull Request (PR)
 
-Notice:
- - **No development happens on the `master` branch**, but rather on separate feature branches
- - **In order to prevent mayhem**, define good interfaces for your code (so that development won't break existing code)
-
-Follow these instructions whenever you merge to master:
-  - `grep` for "cheat"
-  - Check that the `README` is up to date (especially tool status)
-  - Find a reviewer for your Pull Request
+### `master` branch
 
-### tags
+PRs to `master` must abide by the following rules: 
 
-tags are like `master` and on top of this:
- - Should have as many **completed features** as possible
- - The `README` must be up to date, **especially in presence of cheat**
+- HolBA Continuous Integration (CI) must pass
+  - Running `Holmake` must work (i.e., the changes must correctly compile)
+  - All tests run in CI must succeed
+- Use of `cheat` should be a last resort (cheats are reported by the CI in PRs)
+  - You must explicitly say why you used `cheat` if it's not obvious
+  - `grep` for unexpected occurrences of `cheat` before submitting your PR
+- Code should not be be commented out
+- PRs that only fix bugs are welcome but should be documented as such
+- At least one accepting review is needed in order to merge into `master`
+- Standard ML code should come with interfaces (`.sig` files), so that new development won't easily break existing code
+- `README.md` must be up to date (especially w.r.t. tool status)
 
-### Feature branches
+### Tags
 
-Every "somewhat" working tool should be available in the `master` branch, but new
-features or any development must go on new branches prefixed with `dev_`, fixes with `fix_`.
+Tags are like the `master` branch with the following additional rules:
 
-Guidelines:
- - Branch names must be short and explicit (prefer explicit over short)
- - Every feature branch should involve small developments
- - **Rebase** feature branches on `master` **often**, by using `git rebase` or `git merge`: work on small features
- - Commits in a feature branch should compile, unless explicitly stated in commit message (with the prefix `[WIP] ...` for instance)
- - Further subbranch to do implementation experiments (keep them small)
+- A tag should have as many **completed features** as possible
+- `README.md` must be up to date, in particular if there are uses of `cheat`
 
-If you want to violate the rules for temporary development or experiments (only for feature branches):
-  1. Fork
-  2. Do a good mess
-  3. Merge in feature branch after history rewrite
+### Topic branches
 
-### Merging pull requests with GitHub
-  1. Preferably and if possible, rebase the changes for a cleaner and more readable history. And to avoid merging overhead for ongoing work later.
-  2. Have somebody review the pull request, especially if the change is more involving or around the core parts.
-  3. Make sure that one of the CI tasks that build and run the tests completes successfully. One is allowed to timeout for unclear PolyML/HOL4 reasons.
-  4. Merge the pull request with a merge commit to enable a standard GitHub commit message with reference to the pull request it belongs to.
+- Features or other new developments should go in new branches prefixed with `dev_`
+- Branch names should be short and explicit (prefer explicit over short)
+- Try to keep changes in feature branches as small as possible
+- **Rebase** feature branches on top of `master` **often**, by using `git rebase` or `git merge`
+- Commits in a feature branch should compile, unless explicitly stated in the commit message (with the prefix `[WIP] ...` for instance)
 
-### CI > Static analysis
+## Merging branches on GitHub
 
-This CI performs basic static analysis on the code:
- - locates all the places where `cheat` is used.
- - locates all the places where `TODO` or `FIXME` appear.
-
- It then post the results as a comment on the Pull Request (and in the CI logs as well). However, the CI **cannot** post a comment on the PR if the PR comes from a fork, for security reasons. In this case, there will be no comment posted. See #58 for more history.
+1. Preferably and if possible, rebase the changes against the target branch for a cleaner and more readable history, and to avoid merging overhead for later work.
+2. Have somebody review the PR, especially if changes are extensive or affect core modules of HolBA.
+3. Make sure that CI builds and runs the tests successfully. It is allowed to timeout for unclear PolyML/HOL4 reasons.
+4. Merge the PR with a merge commit to enable a standard GitHub commit message with reference to the pull request it belongs to.

Holmakefile

@@ -0,0 +1,30 @@
+CLINE_OPTIONS = -r
+
+INCLUDES = $(HOLBADIR)/src/extra \
+           $(HOLBADIR)/src/shared \
+           $(HOLBADIR)/src/shared/smt \
+           $(HOLBADIR)/src/theory/bir \
+           $(HOLBADIR)/src/theory/bir-support \
+           $(HOLBADIR)/src/theory/models/l3mod \
+           $(HOLBADIR)/src/theory/program_logic \
+           $(HOLBADIR)/src/theory/tools/lifter \
+           $(HOLBADIR)/src/theory/tools/wp \
+           $(HOLBADIR)/src/theory/tools/comp \
+           $(HOLBADIR)/src/theory/tools/backlifter \
+           $(HOLBADIR)/src/theory/tools/symbexec \
+           $(HOLBADIR)/src/tools/lifter \
+           $(HOLBADIR)/src/tools/wp \
+           $(HOLBADIR)/src/tools/comp \
+           $(HOLBADIR)/src/tools/cfg \
+           $(HOLBADIR)/src/tools/backlifter \
+           $(HOLBADIR)/src/tools/exec \
+           $(HOLBADIR)/src/tools/pass \
+           $(HOLBADIR)/src/tools/scamv \
+           $(HOLBADIR)/src/tools/scamv/obsmodel \
+           $(HOLBADIR)/src/tools/scamv/persistence \
+           $(HOLBADIR)/src/tools/scamv/symbexec \
+           $(HOLBADIR)/src/tools/scamv/proggen \
+           $(HOLBADIR)/src/tools/symbexec
+
+all: $(DEFAULT_TARGETS)
+.PHONY: all

Makefile

@@ -29,13 +29,13 @@ BENCHMARKS    = $(SRCDIR)/tools/lifter/benchmark      \
 # recursive wildcard function
 rwildcard=$(wildcard $1$2) $(foreach d,$(wildcard $1*),$(call rwildcard,$d/,$2))
 
-HOLMAKEFILE_GENS = $(call rwildcard,$(SRCDIR)/,Holmakefile.gen) \
-                   $(call rwildcard,$(EXSDIR)/,Holmakefile.gen)
-HOLMAKEFILES     = $(HOLMAKEFILE_GENS:.gen=)
-
+HOLMAKEFILES     = $(call rwildcard,$(SRCDIR)/,Holmakefile) \
+                   $(call rwildcard,$(EXSDIR)/,Holmakefile)
 
 ifdef HOLBA_HOLMAKE
-HOLMAKEFILE_DIRS = $(patsubst %/,%,$(sort $(foreach file,$(HOLMAKEFILE_GENS),$(dir $(file)))))
+HOLMAKEFILE_DIRS = $(patsubst %/,%,$(sort $(foreach file,$(HOLMAKEFILES),$(dir $(file)))))
+
+HOLMAKEFILE_CLEANS = $(foreach holmfld,$(HOLMAKEFILE_DIRS),$(holmfld)_clean)
 
 SML_RUNS         = $(foreach sml,$(call rwildcard,$(SRCDIR)/,*.sml),$(sml)_run) \
                    $(foreach sml,$(call rwildcard,$(EXSDIR)/,*.sml),$(sml)_run)
@@ -55,7 +55,6 @@ all: show-rules
 
 show-rules:
 	@echo 'Available rules:'
-	@echo '     - Holmakefiles: generates `Holmakefile`s from `Holmakefile.gen` files.'
 ifdef HOLBA_HOLMAKE
 	@echo '     - theory: builds only src/theory/'
 	@echo '     - main: builds HolBA, but without the examples or documentation'
@@ -69,17 +68,13 @@ endif
 
 ##########################################################
 
-%Holmakefile: %Holmakefile.gen $(SRCDIR)/Holmakefile.inc
-	@./scripts/gen_Holmakefiles.py $<
-
-Holmakefiles: $(HOLMAKEFILES)
-
-
-$(HOLMAKEFILE_DIRS): Holmakefiles
+$(HOLMAKEFILE_DIRS): $(HOLMAKEFILES)
 	source ./scripts/setup/env_derive.sh && cd $@ && $(HOLBA_HOLMAKE) $(HOLBA_HOLMAKE_OPTS)
 
+$(HOLMAKEFILE_CLEANS):
+	cd $(patsubst %_clean,%,$@) && $(HOLBA_HOLMAKE) clean && $(HOLBA_HOLMAKE) cleanAll
 
-%.exe: %.sml Holmakefiles
+%.exe: %.sml $(HOLMAKEFILES)
 	@/usr/bin/env HOLBA_HOLMAKE="$(HOLBA_HOLMAKE)" ./scripts/mk-exe.sh $(@:.exe=.sml)
 
 # this is a target for all sml files to run as scripts,
@@ -105,6 +100,7 @@ main:          $(SRCDIR)
 examples-base: main $(EXAMPLES_BASE)
 examples-all:  main $(EXAMPLES_ALL)
 benchmarks:    main $(BENCHMARKS)
+riscv:         main src/tools/symbexec/examples/riscv
 
 
 tests: $(TEST_EXES) $(TEST_DIRS)
@@ -124,8 +120,6 @@ cleanslate:
 
 ##########################################################
 
-.PHONY: Holmakefiles
-
 ifdef HOLBA_HOLMAKE
 .PHONY: $(HOLMAKEFILE_DIRS)
 .PHONY: $(SML_RUNS)