diff --git a/.github/workflows/cygwin-530-trunk.yml b/.github/workflows/cygwin-530-trunk.yml index 9d39a3ba0..fd0ef0dd5 100644 --- a/.github/workflows/cygwin-530-trunk.yml +++ b/.github/workflows/cygwin-530-trunk.yml @@ -6,8 +6,6 @@ on: - cron: '22 2 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/cygwin-540-trunk.yml b/.github/workflows/cygwin-540-trunk.yml index 021b36e7b..4c80dcb2d 100644 --- a/.github/workflows/cygwin-540-trunk.yml +++ b/.github/workflows/cygwin-540-trunk.yml @@ -6,8 +6,6 @@ on: - cron: '33 3 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/cygwin-550-trunk.yml b/.github/workflows/cygwin-550-trunk.yml index 93e69c031..a068da025 100644 --- a/.github/workflows/cygwin-550-trunk.yml +++ b/.github/workflows/cygwin-550-trunk.yml @@ -6,8 +6,6 @@ on: - cron: '44 4 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/gh-pages.yml b/.github/workflows/gh-pages.yml deleted file mode 100644 index 2156be2f8..000000000 --- a/.github/workflows/gh-pages.yml +++ /dev/null @@ -1,42 +0,0 @@ -name: github pages - -on: - push: - branches: - - main # Set a branch name to trigger deployment - -jobs: - deploy: - runs-on: ubuntu-latest - steps: - - name: Checkout code - uses: actions/checkout@v4 - - - name: Cache opam - id: cache-opam - uses: actions/cache@v4 - with: - path: ~/.opam - key: opam-ubuntu-latest-5.0.0 - - - uses: avsm/setup-ocaml@v3 - with: - ocaml-compiler: 'ocaml-base-compiler.5.0.0' - default: https://github.com/ocaml/opam-repository.git - - - name: Pin packages - run: opam pin -n . - - - name: Install dependencies - run: opam install -d . --deps-only - - - name: Build - run: opam exec -- dune build @doc - - - name: Deploy - uses: peaceiris/actions-gh-pages@v4 - with: - github_token: ${{ secrets.GITHUB_TOKEN }} - publish_dir: ./_build/default/_doc/_html/ - destination_dir: dev - enable_jekyll: true diff --git a/.github/workflows/linux-530-trunk-32bit.yml b/.github/workflows/linux-530-trunk-32bit.yml index b5158862c..0f12e3fd8 100644 --- a/.github/workflows/linux-530-trunk-32bit.yml +++ b/.github/workflows/linux-530-trunk-32bit.yml @@ -6,8 +6,6 @@ on: - cron: '22 2 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/linux-530-trunk-arm64.yml b/.github/workflows/linux-530-trunk-arm64.yml index 21f97e858..f4f04312b 100644 --- a/.github/workflows/linux-530-trunk-arm64.yml +++ b/.github/workflows/linux-530-trunk-arm64.yml @@ -6,8 +6,6 @@ on: - cron: '22 2 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/linux-530-trunk-bytecode.yml b/.github/workflows/linux-530-trunk-bytecode.yml index 90c056683..b2281aaf8 100644 --- a/.github/workflows/linux-530-trunk-bytecode.yml +++ b/.github/workflows/linux-530-trunk-bytecode.yml @@ -6,8 +6,6 @@ on: - cron: '22 2 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/linux-530-trunk-debug.yml b/.github/workflows/linux-530-trunk-debug.yml index 03728baa5..d8f408fda 100644 --- a/.github/workflows/linux-530-trunk-debug.yml +++ b/.github/workflows/linux-530-trunk-debug.yml @@ -6,8 +6,6 @@ on: - cron: '22 2 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/linux-530-trunk-fp.yml b/.github/workflows/linux-530-trunk-fp.yml index 3faf669c7..c0a8fffd5 100644 --- a/.github/workflows/linux-530-trunk-fp.yml +++ b/.github/workflows/linux-530-trunk-fp.yml @@ -6,8 +6,6 @@ on: - cron: '22 2 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/linux-530-trunk-musl.yml b/.github/workflows/linux-530-trunk-musl.yml index 43d279c8d..0ef4bf364 100644 --- a/.github/workflows/linux-530-trunk-musl.yml +++ b/.github/workflows/linux-530-trunk-musl.yml @@ -6,8 +6,6 @@ on: - cron: '22 2 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/linux-530-trunk.yml b/.github/workflows/linux-530-trunk.yml index 26f4820ac..d8fb68a9f 100644 --- a/.github/workflows/linux-530-trunk.yml +++ b/.github/workflows/linux-530-trunk.yml @@ -6,8 +6,6 @@ on: - cron: '22 2 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/linux-540-trunk-32bit.yml b/.github/workflows/linux-540-trunk-32bit.yml index 7830fceb0..da1c8540b 100644 --- a/.github/workflows/linux-540-trunk-32bit.yml +++ b/.github/workflows/linux-540-trunk-32bit.yml @@ -6,8 +6,6 @@ on: - cron: '33 3 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/linux-540-trunk-arm64.yml b/.github/workflows/linux-540-trunk-arm64.yml index e0d07c8aa..f6a8d5c0f 100644 --- a/.github/workflows/linux-540-trunk-arm64.yml +++ b/.github/workflows/linux-540-trunk-arm64.yml @@ -6,8 +6,6 @@ on: - cron: '33 3 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/linux-540-trunk-bytecode.yml b/.github/workflows/linux-540-trunk-bytecode.yml index 9c26e89ba..696594ef7 100644 --- a/.github/workflows/linux-540-trunk-bytecode.yml +++ b/.github/workflows/linux-540-trunk-bytecode.yml @@ -6,8 +6,6 @@ on: - cron: '33 3 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/linux-540-trunk-debug.yml b/.github/workflows/linux-540-trunk-debug.yml index 6d1af659d..5bbc86d4f 100644 --- a/.github/workflows/linux-540-trunk-debug.yml +++ b/.github/workflows/linux-540-trunk-debug.yml @@ -6,8 +6,6 @@ on: - cron: '33 3 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/linux-540-trunk-fp.yml b/.github/workflows/linux-540-trunk-fp.yml index b02ca4c85..1cfc7f22b 100644 --- a/.github/workflows/linux-540-trunk-fp.yml +++ b/.github/workflows/linux-540-trunk-fp.yml @@ -6,8 +6,6 @@ on: - cron: '33 3 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/linux-540-trunk-musl.yml b/.github/workflows/linux-540-trunk-musl.yml index fede355de..ddcc661f1 100644 --- a/.github/workflows/linux-540-trunk-musl.yml +++ b/.github/workflows/linux-540-trunk-musl.yml @@ -6,8 +6,6 @@ on: - cron: '33 3 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/linux-540-trunk.yml b/.github/workflows/linux-540-trunk.yml index 355fb56c0..0228f6dbb 100644 --- a/.github/workflows/linux-540-trunk.yml +++ b/.github/workflows/linux-540-trunk.yml @@ -6,8 +6,6 @@ on: - cron: '33 3 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/linux-550-trunk-32bit.yml b/.github/workflows/linux-550-trunk-32bit.yml index 1606c1a44..aefd5dd79 100644 --- a/.github/workflows/linux-550-trunk-32bit.yml +++ b/.github/workflows/linux-550-trunk-32bit.yml @@ -6,8 +6,6 @@ on: - cron: '44 4 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/linux-550-trunk-arm64.yml b/.github/workflows/linux-550-trunk-arm64.yml index 7e3318c93..fd128fa25 100644 --- a/.github/workflows/linux-550-trunk-arm64.yml +++ b/.github/workflows/linux-550-trunk-arm64.yml @@ -6,8 +6,6 @@ on: - cron: '44 4 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/linux-550-trunk-bytecode.yml b/.github/workflows/linux-550-trunk-bytecode.yml index e7acbaab6..590ddaff7 100644 --- a/.github/workflows/linux-550-trunk-bytecode.yml +++ b/.github/workflows/linux-550-trunk-bytecode.yml @@ -6,8 +6,6 @@ on: - cron: '44 4 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/linux-550-trunk-debug.yml b/.github/workflows/linux-550-trunk-debug.yml index dad6be936..72089560b 100644 --- a/.github/workflows/linux-550-trunk-debug.yml +++ b/.github/workflows/linux-550-trunk-debug.yml @@ -6,8 +6,6 @@ on: - cron: '44 4 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/linux-550-trunk-fp.yml b/.github/workflows/linux-550-trunk-fp.yml index af52b1a72..38d0165fe 100644 --- a/.github/workflows/linux-550-trunk-fp.yml +++ b/.github/workflows/linux-550-trunk-fp.yml @@ -6,8 +6,6 @@ on: - cron: '44 4 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/linux-550-trunk-musl.yml b/.github/workflows/linux-550-trunk-musl.yml index 3476c96fd..f7b89346a 100644 --- a/.github/workflows/linux-550-trunk-musl.yml +++ b/.github/workflows/linux-550-trunk-musl.yml @@ -6,8 +6,6 @@ on: - cron: '44 4 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/linux-550-trunk.yml b/.github/workflows/linux-550-trunk.yml index 6e86621cd..e4dec40f3 100644 --- a/.github/workflows/linux-550-trunk.yml +++ b/.github/workflows/linux-550-trunk.yml @@ -6,8 +6,6 @@ on: - cron: '44 4 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/macosx-arm64-530-trunk.yml b/.github/workflows/macosx-arm64-530-trunk.yml index 86f466f01..cb69cf0c6 100644 --- a/.github/workflows/macosx-arm64-530-trunk.yml +++ b/.github/workflows/macosx-arm64-530-trunk.yml @@ -6,8 +6,6 @@ on: - cron: '22 2 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/macosx-arm64-540-trunk.yml b/.github/workflows/macosx-arm64-540-trunk.yml index d3c958a47..b9b01c315 100644 --- a/.github/workflows/macosx-arm64-540-trunk.yml +++ b/.github/workflows/macosx-arm64-540-trunk.yml @@ -6,8 +6,6 @@ on: - cron: '33 3 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/macosx-arm64-550-trunk.yml b/.github/workflows/macosx-arm64-550-trunk.yml index f32cc6c87..639bf356c 100644 --- a/.github/workflows/macosx-arm64-550-trunk.yml +++ b/.github/workflows/macosx-arm64-550-trunk.yml @@ -6,8 +6,6 @@ on: - cron: '44 4 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/macosx-intel-530-trunk.yml b/.github/workflows/macosx-intel-530-trunk.yml index 8ae97bb56..01e93ffcd 100644 --- a/.github/workflows/macosx-intel-530-trunk.yml +++ b/.github/workflows/macosx-intel-530-trunk.yml @@ -6,8 +6,6 @@ on: - cron: '22 2 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/macosx-intel-540-trunk.yml b/.github/workflows/macosx-intel-540-trunk.yml index dc1c274dd..9213505ce 100644 --- a/.github/workflows/macosx-intel-540-trunk.yml +++ b/.github/workflows/macosx-intel-540-trunk.yml @@ -6,8 +6,6 @@ on: - cron: '33 3 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/macosx-intel-550-trunk.yml b/.github/workflows/macosx-intel-550-trunk.yml index 4fa11811e..4a8ad2ca8 100644 --- a/.github/workflows/macosx-intel-550-trunk.yml +++ b/.github/workflows/macosx-intel-550-trunk.yml @@ -6,8 +6,6 @@ on: - cron: '44 4 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/mingw-530-trunk-bytecode.yml b/.github/workflows/mingw-530-trunk-bytecode.yml index 753e21ca6..fffa0694a 100644 --- a/.github/workflows/mingw-530-trunk-bytecode.yml +++ b/.github/workflows/mingw-530-trunk-bytecode.yml @@ -6,8 +6,6 @@ on: - cron: '22 2 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/mingw-530-trunk.yml b/.github/workflows/mingw-530-trunk.yml index bc3e675ff..0153b6741 100644 --- a/.github/workflows/mingw-530-trunk.yml +++ b/.github/workflows/mingw-530-trunk.yml @@ -6,8 +6,6 @@ on: - cron: '22 2 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/mingw-540-trunk-bytecode.yml b/.github/workflows/mingw-540-trunk-bytecode.yml index 283fac45a..0e4d5d804 100644 --- a/.github/workflows/mingw-540-trunk-bytecode.yml +++ b/.github/workflows/mingw-540-trunk-bytecode.yml @@ -6,8 +6,6 @@ on: - cron: '33 3 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/mingw-540-trunk.yml b/.github/workflows/mingw-540-trunk.yml index e4df53a15..65b3d69e9 100644 --- a/.github/workflows/mingw-540-trunk.yml +++ b/.github/workflows/mingw-540-trunk.yml @@ -6,8 +6,6 @@ on: - cron: '33 3 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/mingw-550-trunk-bytecode.yml b/.github/workflows/mingw-550-trunk-bytecode.yml index bbcb09899..9249bffcd 100644 --- a/.github/workflows/mingw-550-trunk-bytecode.yml +++ b/.github/workflows/mingw-550-trunk-bytecode.yml @@ -6,8 +6,6 @@ on: - cron: '44 4 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/mingw-550-trunk.yml b/.github/workflows/mingw-550-trunk.yml index 0e4fe3ee1..81dabbe23 100644 --- a/.github/workflows/mingw-550-trunk.yml +++ b/.github/workflows/mingw-550-trunk.yml @@ -6,8 +6,6 @@ on: - cron: '44 4 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/msvc-530-trunk-bytecode.yml b/.github/workflows/msvc-530-trunk-bytecode.yml index e0d57dc27..62fddcb18 100644 --- a/.github/workflows/msvc-530-trunk-bytecode.yml +++ b/.github/workflows/msvc-530-trunk-bytecode.yml @@ -6,8 +6,6 @@ on: - cron: '22 2 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/msvc-530-trunk.yml b/.github/workflows/msvc-530-trunk.yml index c599ee866..aecd19f93 100644 --- a/.github/workflows/msvc-530-trunk.yml +++ b/.github/workflows/msvc-530-trunk.yml @@ -6,8 +6,6 @@ on: - cron: '22 2 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/msvc-540-trunk-bytecode.yml b/.github/workflows/msvc-540-trunk-bytecode.yml index 23535e3e0..043708079 100644 --- a/.github/workflows/msvc-540-trunk-bytecode.yml +++ b/.github/workflows/msvc-540-trunk-bytecode.yml @@ -6,8 +6,6 @@ on: - cron: '33 3 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/msvc-540-trunk.yml b/.github/workflows/msvc-540-trunk.yml index c190f6240..ce0ad8737 100644 --- a/.github/workflows/msvc-540-trunk.yml +++ b/.github/workflows/msvc-540-trunk.yml @@ -6,8 +6,6 @@ on: - cron: '33 3 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/msvc-550-trunk-bytecode.yml b/.github/workflows/msvc-550-trunk-bytecode.yml index 2e0651853..70b95ab07 100644 --- a/.github/workflows/msvc-550-trunk-bytecode.yml +++ b/.github/workflows/msvc-550-trunk-bytecode.yml @@ -6,8 +6,6 @@ on: - cron: '44 4 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/msvc-550-trunk.yml b/.github/workflows/msvc-550-trunk.yml index a8307af86..17baa3b46 100644 --- a/.github/workflows/msvc-550-trunk.yml +++ b/.github/workflows/msvc-550-trunk.yml @@ -6,8 +6,6 @@ on: - cron: '44 4 * * 1' pull_request: push: - branches: - - main workflow_dispatch: jobs: diff --git a/.github/workflows/opam.yml b/.github/workflows/opam.yml deleted file mode 100644 index 37728bc31..000000000 --- a/.github/workflows/opam.yml +++ /dev/null @@ -1,52 +0,0 @@ -name: OPAM installation - -concurrency: - group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }} - cancel-in-progress: true - -on: - pull_request: - push: - branches: - - main - workflow_dispatch: - -jobs: - build-and-test: - env: - QCHECK_MSG_INTERVAL: '60' - - strategy: - fail-fast: false - matrix: - ocaml-compiler: - - 4.12.x - - 4.13.x - - 4.14.x - - 5.0.0 - - 5.1.0 - - 5.2.0 - - 5.3.0 - - ocaml-variants.5.4.0+trunk - - runs-on: ubuntu-latest - - steps: - - name: Checkout code - uses: actions/checkout@v4 - - - name: Install OCaml compiler - uses: ocaml/setup-ocaml@v3 - with: - ocaml-compiler: ${{ matrix.ocaml-compiler }} - - - name: Test installation of the OPAM packages - run: | - opam install --with-test ./qcheck-multicoretests-util.opam ./qcheck-lin.opam ./qcheck-stm.opam - - - name: Show configuration - run: | - opam exec -- ocamlc -config - opam config list - opam exec -- dune printenv - opam list --columns=name,installed-version,repository,synopsis-or-target diff --git a/dune b/dune index 23c9304ff..b23414518 100644 --- a/dune +++ b/dune @@ -36,8 +36,8 @@ (name ci) (package multicoretests) (deps - (alias_rec %{env:DUNE_CI_ALIAS=testsuite}))) - ; (alias_rec focusedtest))) + ; (alias_rec %{env:DUNE_CI_ALIAS=testsuite}) + (alias_rec focusedtest))) ; @focusedtest ; repeat a single test a couple of times @@ -48,7 +48,7 @@ ; To change the test to repeat, change the source of the `copy`: (rule - (copy src/io/lin_tests_domain.exe focusedtest.exe)) + (copy src/sys/stm_tests.exe focusedtest.exe)) (rule (alias focusedtest) @@ -61,7 +61,7 @@ (write-file hoped "") (write-file failed-runs "") (bash - "for i in `seq 20`; do echo Starting $i-th run; if ! ./focusedtest.exe -v ; then echo $i >> failed-runs; fi; done") + "for i in `seq 5`; do echo Starting $i-th run; if ! ./focusedtest.exe -v ; then echo $i >> failed-runs; fi; done") ; edit the previous line to focus on a particular seed (diff failed-runs hoped))))) @@ -76,6 +76,6 @@ (write-file hoped "") (write-file failed-runs "") (run cmd /q /c - "for %G in (1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20) do (echo Starting %G-th run && focusedtest.exe -v || echo %G >> failed-runs)") + "for %G in (1,2,3,4,5) do (echo Starting %G-th run && focusedtest.exe -v || echo %G >> failed-runs)") ; edit the previous line to focus on a particular seed (diff failed-runs hoped))))) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 72ae3b807..5e85f1348 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -1,12 +1,119 @@ open QCheck open STM +module Model = +struct + module Map_names = Map.Make (String) + + type filesys = + | Directory of {fs_map: filesys Map_names.t} + | File + + let empty_dir = Directory {fs_map = Map_names.empty} + + let rec find_opt fs path = + match fs with + | File -> + if path = [] + then Some fs + else None + | Directory d -> + (match path with + | [] -> Some (Directory d) + | hd :: tl -> + (match Map_names.find_opt hd d.fs_map with + | None -> None + | Some fs -> find_opt fs tl)) + + let mem fs path = find_opt fs path <> None + + (* generic removal function *) + let rec remove fs path file_name = + match fs with + | File -> fs + | Directory d -> + (match path with + | [] -> + (match Map_names.find_opt file_name d.fs_map with + | None + | Some _ -> Directory { fs_map = Map_names.remove file_name d.fs_map }) + | dir::dirs -> + Directory + { fs_map = Map_names.update dir (function + | None -> None + | Some File -> Some File + | Some (Directory _ as d') -> Some (remove d' dirs file_name)) d.fs_map + }) + + let readdir fs path = + match find_opt fs path with + | None -> None + | Some fs -> + (match fs with + | File -> None + | Directory d -> Some (Map_names.fold (fun k _ l -> k::l) d.fs_map [])) + + let update_map_name map_name k v = Map_names.update k (fun _ -> Some v) map_name + + (* generic insertion function *) + let rec insert fs path new_file_name sub_tree = + match fs with + | File -> fs + | Directory d -> + (match path with + | [] -> + Directory {fs_map = Map_names.add new_file_name sub_tree d.fs_map} + | next_in_path :: tl_path -> + (match Map_names.find_opt next_in_path d.fs_map with + | None -> fs + | Some sub_fs -> + let nfs = insert sub_fs tl_path new_file_name sub_tree in + if nfs = sub_fs + then fs + else Directory {fs_map = update_map_name d.fs_map next_in_path nfs})) + + let separate_path path = + match List.rev path with + | [] -> None + | name::rev_path -> Some (List.rev rev_path, name) + + let rename fs old_path new_path = + match separate_path old_path, separate_path new_path with + | None, _ + | _, None -> fs + | Some (old_path_pref, old_name), Some (new_path_pref, new_name) -> + (match find_opt fs new_path_pref with + | None + | Some File -> fs + | Some (Directory _) -> + (match find_opt fs old_path with + | None -> fs + | Some sub_fs -> + let fs' = remove fs old_path_pref old_name in + insert fs' new_path_pref new_name sub_fs)) + + let path_is_a_file fs path = + match find_opt fs path with + | None + | Some (Directory _) -> false + | Some File -> true + + let path_is_a_dir fs path = + match find_opt fs path with + | None + | Some File -> false + | Some (Directory _) -> true +end + module SConf = struct type path = string list type cmd = | File_exists of path + | Is_directory of path + | Remove of path * string + | Rename of path * path | Mkdir of path * string | Rmdir of path * string | Readdir of path @@ -17,6 +124,9 @@ struct let pp_path = pp_list pp_string in match x with | File_exists x -> cst1 pp_path "File_exists" par fmt x + | Is_directory x -> cst1 pp_path "Is_directory" par fmt x + | Remove (x, y) -> cst2 pp_path pp_string "Remove" par fmt x y + | Rename (x, y) -> cst2 pp_path pp_path "Rename" par fmt x y | Mkdir (x, y) -> cst2 pp_path pp_string "Mkdir" par fmt x y | Rmdir (x, y) -> cst2 pp_path pp_string "Rmdir" par fmt x y | Readdir x -> cst1 pp_path "Readdir" par fmt x @@ -24,171 +134,124 @@ struct let show_cmd = Util.Pp.to_show pp_cmd - module Map_names = Map.Make (String) - - type filesys = - | Directory of {fs_map: filesys Map_names.t} - | File - - type state = filesys + type state = Model.filesys type sut = unit let (/) = Filename.concat - let update_map_name map_name k v = Map_names.update k (fun _ -> Some v) map_name - - (* var gen_existing_path : filesys -> path Gen.t *) - let rec gen_existing_path fs = + (* var existing_contents : filesys -> path list * path list *) + let rec existing_contents fs : path list * path list = match fs with - | File -> Gen.return [] - | Directory d -> - (match Map_names.bindings d.fs_map with - | [] -> Gen.return [] - | bindings -> Gen.(oneofl bindings >>= fun (n, sub_fs) -> - Gen.oneof [ - Gen.return [n]; - Gen.map (fun l -> n::l) (gen_existing_path sub_fs)] - ) - ) - - (* var gen_existing_pair : filesys -> (path * string) option Gen.t *) - let rec gen_existing_pair fs = match fs with - | File -> Gen.return None (*failwith "no sandbox directory"*) - | Directory d -> - (match Map_names.bindings d.fs_map with - | [] -> Gen.return None - | bindings -> - Gen.(oneofl bindings >>= fun (n, sub_fs) -> - oneof [ - return (Some ([],n)); - map (function None -> Some ([],n) - | Some (path,name) -> Some (n::path,name)) (gen_existing_pair sub_fs)] - ) - ) - - let name_gen = Gen.oneofl ["aaa" ; "bbb" ; "ccc" ; "ddd" ; "eee"] - let path_gen s = Gen.(oneof [gen_existing_path s; list_size (int_bound 5) name_gen]) (* can be empty *) - let pair_gen s = - let fresh_pair_gen = Gen.(pair (list_size (int_bound 5) name_gen)) name_gen in - Gen.(oneof [ - fresh_pair_gen; - (gen_existing_pair s >>= function None -> fresh_pair_gen - | Some (p,_) -> map (fun n -> (p,n)) name_gen); - (gen_existing_pair s >>= function None -> fresh_pair_gen - | Some (p,n) -> return (p,n)); - ]) + | Model.File -> [[]],[] + | Model.Directory d -> + let bindings = Model.Map_names.bindings d.fs_map in + let files, dirs = List.partition (fun p -> snd p = Model.File) bindings in + let sub_res = + List.map (fun (n,sub_fs) -> + let sub_files, sub_dirs = existing_contents sub_fs in + List.map (fun l -> n::l) sub_files, + List.map (fun l -> n::l) sub_dirs) dirs in + let files = List.map (fun (n,_) -> [n]) files in + List.concat (files :: List.map fst sub_res), + []::List.concat (List.map snd sub_res) + + let name_gen = Gen.oneofl ["aaa" ; "bbb" ; "ccc" ; "ddd" ; "eee"; "fff"; "ggg"; "hhh"; "iii"] let arb_cmd s = + let files, dirs = existing_contents s in + let gen_file = Gen.oneofl files in + let gen_file_sep = Gen.oneofl (List.filter_map Model.separate_path files) in + let gen_dir = Gen.oneofl dirs in + let gen_dir_sep = Gen.oneofl (List.filter_map Model.separate_path dirs) in + let gen_arb_path = Gen.(list_size (int_bound 5) name_gen) in + let gen_arb_path_sep = Gen.(pair (list_size (int_bound 4) name_gen) name_gen) in QCheck.make ~print:show_cmd - Gen.(oneof [ - map (fun path -> File_exists path) (path_gen s); - map (fun (path,new_dir_name) -> Mkdir (path, new_dir_name)) (pair_gen s); - map (fun (path,delete_dir_name) -> Rmdir (path, delete_dir_name)) (pair_gen s); - map (fun path -> Readdir path) (path_gen s); - map (fun (path,new_file_name) -> Mkfile (path, new_file_name)) (pair_gen s); + Gen.( + if files = [] + then + oneof [ + map2 (fun path new_file_name -> Mkfile (path, new_file_name)) gen_dir name_gen; + map2 (fun path new_dir_name -> Mkdir (path, new_dir_name)) gen_dir name_gen; + ] + else + frequency [ + 1,map (fun path -> File_exists path) (frequency [8,gen_file; 1,gen_dir; 1,gen_arb_path]); + 1,map (fun path -> Is_directory path) (frequency [1,gen_file; 8,gen_dir; 1,gen_arb_path]); + 1,map (fun (path,file_name) -> Remove (path, file_name)) (if List.length dirs > 1 + then frequency [8,gen_file_sep; 1,gen_dir_sep; 1,gen_arb_path_sep] + else frequency [1,gen_file_sep; 1,gen_arb_path_sep]); + 1,map (fun (old_path,new_path) -> Rename (old_path, new_path)) (frequency [5,(pair gen_file gen_arb_path); + 5,(pair gen_dir gen_arb_path); + 1,(pair gen_arb_path gen_arb_path); + ]); + 3,map2 (fun path new_dir_name -> Mkdir (path, new_dir_name)) (frequency [1,gen_file; 8,gen_dir; 1,gen_arb_path]) name_gen; + 1,map (fun (path,dir_name) -> Rmdir (path, dir_name)) (if List.length dirs > 1 + then frequency [1,gen_file_sep; 8,gen_dir_sep; 1,gen_arb_path_sep] + else gen_arb_path_sep); + 1,map (fun path -> Readdir path) (frequency [1,gen_file; 8,gen_dir; 1,gen_arb_path]); + 3,map2 (fun path new_file_name -> Mkfile (path, new_file_name)) gen_dir name_gen; ]) let sandbox_root = "_sandbox" - let init_state = Directory {fs_map = Map_names.empty} - - let rec find_opt_model fs path = - match fs with - | File -> - if path = [] - then Some fs - else None - | Directory d -> - (match path with - | [] -> Some (Directory d) - | hd :: tl -> - (match Map_names.find_opt hd d.fs_map with - | None -> None - | Some fs -> find_opt_model fs tl)) - - let mem_model fs path = find_opt_model fs path <> None - - let rec mkdir_model fs path new_dir_name = - match fs with - | File -> fs - | Directory d -> - (match path with - | [] -> - let new_dir = Directory {fs_map = Map_names.empty} in - Directory {fs_map = Map_names.add new_dir_name new_dir d.fs_map} - | next_in_path :: tl_path -> - (match Map_names.find_opt next_in_path d.fs_map with - | None -> fs - | Some sub_fs -> - let nfs = mkdir_model sub_fs tl_path new_dir_name in - if nfs = sub_fs - then fs - else - let new_map = Map_names.remove next_in_path d.fs_map in - let new_map = Map_names.add next_in_path nfs new_map in - Directory {fs_map = new_map})) - - let readdir_model fs path = - match find_opt_model fs path with - | None -> None - | Some fs -> - (match fs with - | File -> None - | Directory d -> Some (Map_names.fold (fun k _ l -> k::l) d.fs_map [])) - - let rec rmdir_model fs path delete_dir_name = - match fs with - | File -> fs - | Directory d -> - (match path with - | [] -> - (match Map_names.find_opt delete_dir_name d.fs_map with - | Some (Directory target) when Map_names.is_empty target.fs_map -> - Directory {fs_map = Map_names.remove delete_dir_name d.fs_map} - | None | Some File | Some (Directory _) -> fs) - | next_in_path :: tl_path -> - (match Map_names.find_opt next_in_path d.fs_map with - | None -> fs - | Some sub_fs -> - let nfs = rmdir_model sub_fs tl_path delete_dir_name in - if nfs = sub_fs - then fs - else Directory {fs_map = (update_map_name d.fs_map next_in_path nfs)})) - - let rec mkfile_model fs path new_file_name = - match fs with - | File -> fs - | Directory d -> - (match path with - | [] -> - let new_file = File in - Directory {fs_map = Map_names.add new_file_name new_file d.fs_map} - | next_in_path :: tl_path -> - (match Map_names.find_opt next_in_path d.fs_map with - | None -> fs - | Some sub_fs -> - let nfs = mkfile_model sub_fs tl_path new_file_name in - if nfs = sub_fs - then fs - else Directory {fs_map = update_map_name d.fs_map next_in_path nfs})) - + let init_state = Model.empty_dir + + let path_is_an_empty_dir fs path = + Model.readdir fs path = Some [] + + let rec path_prefixes path = match path with + | [] -> [] + | [_] -> [] + | n::ns -> [n]::(List.map (fun p -> n::p) (path_prefixes ns)) + + let rec is_true_prefix path1 path2 = match path1, path2 with + | [], [] -> false + | [], _::_ -> true + | _::_, [] -> false + | n1::p1, n2::p2 -> n1=n2 && is_true_prefix p1 p2 + + (* Note: This model-based test has previously found a number of issues under MinGW/MSVC: + - non-existing readdir on MinGW https://github.com/ocaml/ocaml/issues/11829 (5.1) + - rename dir-to-empty-target-dir https://github.com/ocaml/ocaml/issues/12073 (5.1) + - rename dir-to-file https://github.com/ocaml/ocaml/issues/12073 (5.1) + - rename empty-dir to itself (regression) https://github.com/ocaml/ocaml/issues/12317 (5.1) + - rename parent-to-empty-child-dir https://github.com/ocaml/ocaml/pull/13166 (5.3) + These issues have since been fixed and the test workarounds have therefore been removed again. + As a result this test may fail on MinGW/MSVC with OCaml 5.0-5.2. + *) let next_state c fs = match c with | File_exists _path -> fs | Mkdir (path, new_dir_name) -> - if mem_model fs (path @ [new_dir_name]) + if Model.mem fs (path @ [new_dir_name]) + then fs + else Model.insert fs path new_dir_name Model.empty_dir + | Remove (path, file_name) -> + if Model.find_opt fs (path @ [file_name]) = Some File + then Model.remove fs path file_name + else fs + | Rename (old_path, new_path) -> + if is_true_prefix old_path new_path then fs - else mkdir_model fs path new_dir_name + else + (match Model.find_opt fs old_path with + | None -> fs + | Some File -> + if (not (Model.mem fs new_path) || Model.path_is_a_file fs new_path) then Model.rename fs old_path new_path else fs + | Some (Directory _) -> + if (not (Model.mem fs new_path) || path_is_an_empty_dir fs new_path) then Model.rename fs old_path new_path else fs) + | Is_directory _path -> fs | Rmdir (path,delete_dir_name) -> - if mem_model fs (path @ [delete_dir_name]) - then rmdir_model fs path delete_dir_name + let complete_path = path @ [delete_dir_name] in + if Model.mem fs complete_path && path_is_an_empty_dir fs complete_path + then Model.remove fs path delete_dir_name else fs | Readdir _path -> fs | Mkfile (path, new_file_name) -> - if mem_model fs (path @ [new_file_name]) + if Model.mem fs (path @ [new_file_name]) then fs - else mkfile_model fs path new_file_name + else Model.insert fs path new_file_name File let init_sut () = try Sys.mkdir sandbox_root 0o700 @@ -212,6 +275,9 @@ struct let run c _file_name = match c with | File_exists path -> Res (bool, Sys.file_exists (p path)) + | Is_directory path -> Res (result bool exn, protect Sys.is_directory (p path)) + | Remove (path, file_name) -> Res (result unit exn, protect Sys.remove ((p path) / file_name)) + | Rename (old_path, new_path) -> Res (result unit exn, protect (Sys.rename (p old_path)) (p new_path)) | Mkdir (path, new_dir_name) -> Res (result unit exn, protect (Sys.mkdir ((p path) / new_dir_name)) 0o755) | Rmdir (path, delete_dir_name) -> @@ -221,115 +287,84 @@ struct | Mkfile (path, new_file_name) -> Res (result unit exn, protect mkfile (p path / new_file_name)) - let fs_is_a_dir fs = match fs with | Directory _ -> true | File -> false - - let path_is_a_dir fs path = - match find_opt_model fs path with - | None -> false - | Some target_fs -> fs_is_a_dir target_fs - - let postcond c (fs: filesys) res = + let postcond c (fs: Model.filesys) res = match c, res with - | File_exists path, Res ((Bool,_),b) -> b = mem_model fs path + | File_exists path, Res ((Bool,_),b) -> + b = Model.mem fs path + | Is_directory path, Res ((Result (Bool,Exn),_),res) -> + (match res with + | Ok b -> + (match Model.find_opt fs path with + | Some (Directory _) -> b = true + | Some File -> b = false + | None -> false) + | Error (Sys_error _) -> not (Model.mem fs path) + | _ -> false) + | Remove (path, file_name), Res ((Result (Unit,Exn),_), res) -> + let full_path = path @ [file_name] in + (match res with + | Ok () -> Model.mem fs full_path && Model.path_is_a_dir fs path && not (Model.path_is_a_dir fs full_path) + | Error (Sys_error _) -> + (not (Model.mem fs full_path)) || Model.path_is_a_dir fs full_path || not (Model.path_is_a_dir fs path) + | Error _ -> false + ) + | Rename (old_path, new_path), Res ((Result (Unit,Exn),_), res) -> + (match res with + | Ok () -> Model.mem fs old_path (* permits dir-to-file MingW success https://github.com/ocaml/ocaml/issues/12073 *) + | Error (Sys_error _) -> + (* general conditions *) + (not (Model.mem fs old_path)) || + is_true_prefix old_path new_path || (* parent-to-child *) + is_true_prefix new_path old_path || (* child-to-parent *) + (Model.path_is_a_file fs old_path && Model.path_is_a_dir fs new_path) || (* file-to-dir *) + (Model.path_is_a_dir fs old_path && Model.path_is_a_file fs new_path) || (* dir-to-file *) + (Model.path_is_a_dir fs new_path && not (path_is_an_empty_dir fs new_path)) || (* to-non-empty-dir *) + List.exists (fun pref -> not (Model.path_is_a_dir fs pref)) (path_prefixes new_path) (* malformed-target-path *) + | Error _ -> false) | Mkdir (path, new_dir_name), Res ((Result (Unit,Exn),_), res) -> - let complete_path = (path @ [new_dir_name]) in + let full_path = path @ [new_dir_name] in (match res with - | Error err -> - (match err with - | Sys_error s -> - (s = (p complete_path) ^ ": Permission denied") || - (s = (p complete_path) ^ ": File exists" && mem_model fs complete_path) || - ((s = (p complete_path) ^ ": No such file or directory" - || s = (p complete_path) ^ ": Invalid argument") && not (mem_model fs path)) || - if Sys.win32 && not (path_is_a_dir fs complete_path) - then s = (p complete_path) ^ ": No such file or directory" - else s = (p complete_path) ^ ": Not a directory" - | _ -> false) - | Ok () -> mem_model fs path && path_is_a_dir fs path && not (mem_model fs complete_path)) + | Ok () -> Model.mem fs path && Model.path_is_a_dir fs path && not (Model.mem fs full_path) + | Error (Sys_error _) -> + Model.mem fs full_path || (not (Model.mem fs path)) || not (Model.path_is_a_dir fs full_path) + | Error _ -> false) | Rmdir (path, delete_dir_name), Res ((Result (Unit,Exn),_), res) -> - let complete_path = (path @ [delete_dir_name]) in + let full_path = path @ [delete_dir_name] in (match res with - | Error err -> - (match err with - | Sys_error s -> - (s = (p complete_path) ^ ": Permission denied") || - (s = (p complete_path) ^ ": Directory not empty" && not (readdir_model fs complete_path = Some [])) || - (s = (p complete_path) ^ ": No such file or directory" && not (mem_model fs complete_path)) || - if Sys.win32 && not (path_is_a_dir fs complete_path) (* if not a directory *) - then s = (p complete_path) ^ ": Invalid argument" - else s = (p complete_path) ^ ": Not a directory" - | _ -> false) - | Ok () -> - mem_model fs complete_path && path_is_a_dir fs complete_path && readdir_model fs complete_path = Some []) + | Ok () -> + Model.mem fs full_path && Model.path_is_a_dir fs full_path && path_is_an_empty_dir fs full_path + | Error (Sys_error _) -> + (not (Model.mem fs full_path)) || + (not (Model.path_is_a_dir fs full_path)) || + (not (path_is_an_empty_dir fs full_path)) + | Error _ -> false) | Readdir path, Res ((Result (Array String,Exn),_), res) -> (match res with - | Error err -> - (match err with - | Sys_error s -> - (s = (p path) ^ ": Permission denied") || - (s = (p path) ^ ": No such file or directory" && not (mem_model fs path)) || - if Sys.win32 && not (path_is_a_dir fs path) (* if not a directory *) - then s = (p path) ^ ": Invalid argument" - else s = (p path) ^ ": Not a directory" - | _ -> false) - | Ok array_of_subdir -> - (* Temporary work around for mingW, see https://github.com/ocaml/ocaml/issues/11829 *) - if Sys.win32 && not (mem_model fs path) - then array_of_subdir = [||] - else - (mem_model fs path && path_is_a_dir fs path && - (match readdir_model fs path with + | Ok array_of_subdir -> + Model.mem fs path && Model.path_is_a_dir fs path && + (match Model.readdir fs path with | None -> false | Some l -> List.sort String.compare l - = List.sort String.compare (Array.to_list array_of_subdir)))) - | Mkfile (path, new_file_name), Res ((Result (Unit,Exn),_),res) -> ( - let complete_path = path @ [ new_file_name ] in - let concatenated_path = p complete_path in - let match_msg err msg = err = concatenated_path ^ ": " ^ msg in - let match_msgs err = List.exists (match_msg err) in - let msgs_already_exists = ["File exists"; "Permission denied"] - (* Permission denied: seen (sometimes?) on Windows *) - and msgs_non_existent_dir = ["No such file or directory"; - "Invalid argument"; - "Permission denied"] - (* Invalid argument: seen on macOS - Permission denied: seen on Windows *) - and msg_path_not_dir = - match Sys.os_type with - | "Cygwin" - | "Unix" -> "Not a directory" - | "Win32" -> "No such file or directory" - | v -> failwith ("Sys tests not working with " ^ v) - in - match res with - | Error err -> ( - match err with - | Sys_error s -> - (mem_model fs complete_path && match_msgs s msgs_already_exists) - || (not (mem_model fs path) && match_msgs s msgs_non_existent_dir) - || (not (path_is_a_dir fs path) && match_msg s msg_path_not_dir) - | _ -> false) - | Ok () -> path_is_a_dir fs path && not (mem_model fs complete_path)) + = List.sort String.compare (Array.to_list array_of_subdir)) + | Error (Sys_error _) -> + (not (Model.mem fs path)) || (not (Model.path_is_a_dir fs path)) + | Error _ -> false) + | Mkfile (path, new_file_name), Res ((Result (Unit,Exn),_),res) -> + let full_path = path @ [new_file_name] in + (match res with + | Ok () -> Model.path_is_a_dir fs path && not (Model.mem fs full_path) + | Error (Sys_error _) -> + Model.mem fs full_path || (not (Model.mem fs path)) || (not (Model.path_is_a_dir fs path)) + | Error _ -> false) | _,_ -> false end -let run_cmd cmd = - let ic = Unix.open_process_in cmd in - let os = In_channel.input_line ic in - ignore (Unix.close_process_in ic); - os - -let uname_os () = run_cmd "uname -s" - module Sys_seq = STM_sequential.Make(SConf) module Sys_dom = STM_domain.Make(SConf) -;; -QCheck_base_runner.run_tests_main [ - Sys_seq.agree_test ~count:1000 ~name:"STM Sys test sequential"; - if Sys.unix && uname_os () = Some "Linux" - then Sys_dom.agree_test_par ~count:200 ~name:"STM Sys test parallel" - else Sys_dom.neg_agree_test_par ~count:2500 ~name:"STM Sys test parallel"; - Sys_dom.stress_test_par ~count:1000 ~name:"STM Sys stress test parallel"; +let _ = + QCheck_base_runner.run_tests_main [ + Sys_seq.agree_test ~count:1000 ~name:"STM Sys test sequential"; + Sys_dom.stress_test_par ~count:1000 ~name:"STM Sys stress test parallel"; ]