diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 2940c2df55..3104b97805 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -70,5 +70,7 @@ jobs: opam switch ${{ matrix.version }} eval $(opam env --switch=${{ matrix.version }}) cd tests; USE_OPAM='' ./run-ci.sh + USE_OPAM='' ./run-save-to-where.sh ./diff-prog.py cerberus bytes/elab.json ./diff-prog.py cerberus bytes/exec.json + ./diff-prog.py where/filter_debug.sh where/debug.json diff --git a/CLAUDE.md b/CLAUDE.md new file mode 100644 index 0000000000..56f4fc3874 --- /dev/null +++ b/CLAUDE.md @@ -0,0 +1,161 @@ +# Cerberus + +Cerberus is a C semantics tool written in OCaml with a Dune build system. + +## Build & run + +```sh +make && make installl # buid everything and install it to the opam path + +# Common invocations +cerberus file.c # parse + elaborate only +cerberus --exec --batch file.c # execute and print result +cerberus --pp core file.c # pretty-print Core IR +cerberus --typecheck-core file.c # typecheck the Core IR +cerberus --sw mem2reg file.c # enable a switch +``` + +Always use `make && make install` for building instead of dune commands. + +## Architecture + +| Library / binary | Path | Role | +|---|---|---| +| `cerb_frontend` | `ocaml_frontend/` | C→AIL→Core elaboration, rewriters, switches | +| `cerb_backend` | `backend/common/` | Pipeline orchestration (`pipeline.ml`) | +| `cerberus` binary | `backend/driver/main.ml` | CLI entry point | + +The pipeline in `backend/common/pipeline.ml`: +1. C source → Cabs (C parser) +2. Cabs → AIL (`Cabs_to_ail.desugar`) +3. AIL → Core (`Translation.translate`) +4. `core_passes` — per-file Core transforms, then typechecking + +## Important: generated code + +`ocaml_frontend/generated/` is auto-generated from Lem specs in +`frontend/model/`. **Do not edit those files directly.** Read them only to +understand translation output; the authoritative sources are the `.lem` files. + +The `ocaml_frontend/dune` file uses `(include_subdirs unqualified)`, so any +`.ml` file added anywhere under `ocaml_frontend/` (including subdirs) is +automatically compiled into `cerb_frontend`. + +## How to add a Cerberus switch + +1. Add a constructor to `cerb_switch` in `ocaml_frontend/switches.ml` and + `ocaml_frontend/switches.mli`. +2. Add a `| "name" -> Some SW_name` case in `read_switch` (before `| _ -> None`). +3. For a simple boolean switch, add `| SW_name` to the equality arm of `pred` + (lines ~115–126 of `switches.ml`). + +## How to add a Core pass + +1. Create `ocaml_frontend/rewriters/my_pass.ml` — see `remove_unspecs.ml` for + a minimal example. Expose `val transform_file`. +2. In `backend/common/pipeline.ml`, inside `core_passes`, add after the + `Remove_unspecs` block: + ```ocaml + let core_file = + if Switches.(has_switch SW_my_pass) then + My_pass.transform_file core_file + else core_file in + ``` + +## Tests + +```sh +cd tests +USE_OPAM='' bash run.sh # full suite (parsing, ci, tcc, gcc-torture) +USE_OPAM='' bash run-ci.sh # CI subset only +``` + +Always set `USE_OPAM=''`; without it, `common.sh` invokes cerberus via +`dune exec`, which emits deprecation warnings and timing lines on stderr that +pollute output comparisons for `*.error.c` and `*.syntax-only.c` tests. + +CI tests live in `tests/ci/`. Each test is a `.c` file run with +`cerberus --exec --batch`; expected output is in `tests/ci/expected/*.expected`. +Instructions to Claude for writing OCaml code: + +# Writing Code + +0. When writing code, do these things first: + + 1. Write a plan with high-level architectural decisions. Analyze this plan for defects, + and keep fixing them until no obvious deficiencies remain. + + 2. Write a detailed design document, with design choices for each module. Again, before + proceeding to implementaiton, analyze the design for obvious flaws before proceeding. + If there is a fundamental design problem, DO NOT try to smooth it over. Instead, consult + the user about how to proceed, giving them the key options. + + 3. If the detailed design reveals a key flaw, consider whether the high-level plan needs + to be revised. Consult the user about how to proceed, and give them some options. + + 4. Copy each design document to a file `doc/history/YYYY-MM-DD_PLAN-NAME.md`, so the user can + read it, and new sessions can understand the changes. + + 5. Write the plan FIRST before writing any code. Leave a "Post implementation addendum" + placeholder section and after the implementation and testing is done, and the user's + feedback on the code incorporated, append any changes from the plan to that section. + +# Writing OCaml code specifically + +1. Programs should be composed of small modules, each implementing a single concern or + data structure. However, mutual recursion between functions is a good reason to + place them in the same module — prefer a single larger module with `and`-linked + mutually recursive functions over separate modules connected by callbacks or + recursive module declarations. + +2. Write .mli files first, before writing any part of a module. + + - .mli files should emphasize the algebraic structure of the data structure. + + - Name the primary type of an .mli file as `t`, so that clients can refer to it as + `Foo.t`, or `'a Foo.t`. + + - Unless otherwise necessary, hide the implementation type. + + - Parameterized types of the form `'a t` should expose a `map : ('a -> 'b) -> 'a t -> 'b t` + primitive in their interface. + + - If a type constructor has monadic structure, then define `return : 'a -> 'a t` and + `(let+) : 'a -> ('a -> 'b t) -> 'b t` operations. + + - If a type can be ordered, then expose a `compare : t -> t > int` primitive. + + - If a type can be printed, expose a `print : Format.formatter -> t -> unit` method in the + interface. Use the Format module's indentation directives to ensure that print methods are + nicely laid out. + + - If a module exposes a parameterized type, give parameterized comparison and printing + functions. + +3. Here are some bad language features to avoid: + + - NEVER use Obj.magic, or any other feature which can break type safety. + + - NEVER use generic equality, since this violates data abstraction. Always use a + type-specific `compare` operation. + +3. Unless explicitly instructed otherwise, DO NOT write code which uses effects. + + - Use a monad with a result type instead of exceptions. + + - Prefer monadic state-passing to mutable data structures. + + - Permission to use mutable data structures is granted on a per-module basis, and + permission in one module does not grant it in any other. + + - Do not perform IO operations, except for debugging, and in any top-level main-like functions. + +3. Write programs by pattern matching over data structures. Avoid + using partial accessors or incomplete patterns matches. + +4. Higher-order functions should be used sparingly, in idiomatic ways. + + - Introducing monadic code to eliminate repeated nested pattern matches is acceptable. + - Use of map, filter, and other algebraically well-behaved functions is acceptable. + - Avoid the use of folds, because they offer no reasoning advantages over explicit + structural recursion. diff --git a/backend/common/pipeline.ml b/backend/common/pipeline.ml index 5d1afaa274..84cb66a674 100644 --- a/backend/common/pipeline.ml +++ b/backend/common/pipeline.ml @@ -468,6 +468,11 @@ let untype_file (file: 'a Core.typed_file) : 'a Core.file = Esave (sym_bTy, List.map (fun (sym, (bTy, pe)) -> (sym, (bTy, untype_pexpr pe))) xs, untype_expr e) | Erun (a, sym, pes) -> Erun (a, sym, List.map untype_pexpr pes) + | Ejump (a, sym, pes) -> + Ejump (a, sym, List.map untype_pexpr pes) + | Ewhere (e, defs) -> + Ewhere (untype_expr e, + List.map (fun (sym_bTy, params, body) -> (sym_bTy, params, untype_expr body)) defs) | Epar es -> Epar (List.map untype_expr es) | Ewait tid -> @@ -567,6 +572,11 @@ let core_passes (conf, io) ~filename core_file = Copy_propagation.transform_file ~unwrap_loaded:rm_unspecs core_file else core_file in + let core_file = + if Switches.(has_switch SW_save_to_where) then + Save_to_where.transform_file core_file + else + core_file in Core_indet.hackish_order <$> begin if conf.sequentialise_core || conf.typecheck_core then typed_core_passes (conf, io) core_file >>= fun (core_file, typed_core_file) -> diff --git a/doc/ewhere-ejump-plan.md b/doc/ewhere-ejump-plan.md new file mode 100644 index 0000000000..66d5815db7 --- /dev/null +++ b/doc/ewhere-ejump-plan.md @@ -0,0 +1,660 @@ +Resume session with +``` +claude --resume "add-ewhere-ejump-core-ir" +``` + +# Plan: Add `Ewhere` / `Ejump` to Core IR + +## Context + +The user added two new constructors to `generic_expr_` in `frontend/model/core.lem`: + +- **`Ejump`** – identical to `Erun` in every pass (same field layout, same semantics) +- **`Ewhere`** – similar to `Esave` but defines a **block of mutually recursive labels** + +The type definition had two bugs discovered during planning: +1. `Ewhere`'s field 2 `('sym * core_base_type)` was a mistake and must be **removed** +2. Each element of `Ewhere`'s list must include its own `('sym * core_base_type)`, i.e. become `list (('sym * core_base_type) * params_list * generic_expr)` + +The generated `ocaml_frontend/generated/core.ml` was regenerated already (from the pre-fix `core.lem`), so it has the *wrong* type. After fixing `core.lem`, all generated files must be regenerated via `make`. + +Build fails with exhaustiveness-check errors (`-w @8`) on these files: +- `ocaml_frontend/generated/core_sequentialise.ml` +- `ocaml_frontend/generated/core_linking.ml` +- `ocaml_frontend/generated/core_aux.ml` (9 functions) +- `ocaml_frontend/rewriters/core_rewriter.ml` +- `ocaml_frontend/rewriters/copy_propagation.ml` +- `ocaml_frontend/pprinters/pp_core.ml` + +Additional files will fail once the above are fixed (dune stops at first errors due to dependency order): +- `ocaml_frontend/generated/core_rewrite.ml`, `core_run.ml`, `core_reduction.ml`, `core_typing.ml`, `core_indet.ml`, `core_run_aux.ml` +- `ocaml_frontend/rewriters/core_peval.ml` +- `ocaml_frontend/milicore.ml` + +--- + +## Corrected type definitions + +### `frontend/model/core.lem` + +Replace (lines 336-337): +```lem +| Ewhere of (generic_expr 'a 'bty 'sym) * ('sym * core_base_type) * list (list ('sym * (core_base_type * maybe (Ctype.ctype * pass_by_value_or_pointer))) * (generic_expr 'a 'bty 'sym)) +| Ejump of 'a * 'sym * list (generic_pexpr 'bty 'sym) +``` + +With: +```lem +| Ewhere of (generic_expr 'a 'bty 'sym) * list (('sym * core_base_type) * list ('sym * (core_base_type * maybe (Ctype.ctype * pass_by_value_or_pointer))) * (generic_expr 'a 'bty 'sym)) +| Ejump of 'a * 'sym * list (generic_pexpr 'bty 'sym) +``` + +--- + +## Step-by-step implementation + +### Phase 1 – Fix Lem sources (regenerated automatically by `make`) + +**Pattern to apply everywhere:** + +- `Ejump` cases are **identical to `Erun`** cases (same signature, same structure) +- `Ewhere e defs` cases recurse into `e` and each `body` in `defs`; bind `params` of each def like `Esave` binds its param list + +#### `frontend/model/core_sequentialise.lem` + +After the `Erun` case (line 57), add: +```lem +| Ewhere e cases -> + Ewhere (sequentialise_expr e) + (List.map (fun (sym_ty, params, body) -> (sym_ty, params, sequentialise_expr body)) cases) +| Ejump () sym es -> + expr_ +``` + +#### `frontend/model/core_aux.lem` (9 functions) + +Each function gets `Ejump` like its `Erun` case and `Ewhere` like an `Esave`-over-list. +Any functions looking for Eruns/Esaves should skip Ejump/Ewhere - they will be mutually exclusive: programs with the former will be transformed into the latter by a future Core rewriter. + +| Function (line) | `Ejump` | `Ewhere` | +|---|---|---| +| `subst_sym_expr` (1030) | `Ejump annot lab_sym (List.map (subst_sym_pexpr sym cval) pes)` | subst into `e` + each body; skip body if param shadows sym | +| `unsafe_subst_sym_expr` (1299) | same with `unsafe_subst_sym_pexpr` | same | +| `to_pure` (1574) | `Nothing` | `Nothing` | +| `subst_wait` (1649) | `expr_` | recurse `e` and each body | +| `find_labeled_continuation` (1748) | `Nothing` | `Nothing` (Ejump/Ewhere and Erun/Esave will be mutually exclusive) | +| `find_labeled_continuation2_aux` (1827) | `acc` | `acc` | +| `collect_labeled_continuations` (1911) | `Map.empty` | `Map.empty` | +| `collect_saves_aux` (2240) | `st` | `st` | +| `m_collect_saves_aux` (2352) | `st` | `st` | + +Specific code for `subst_sym_expr` Ewhere: +```lem +| Ewhere e cases -> + let cases' = List.map (fun (sym_ty, params, body) -> + (sym_ty, params, + if List.any (fun (z, _) -> sym = z) params then body + else subst_sym_expr sym cval body) + ) cases in + Ewhere (subst_sym_expr sym cval e) cases' +``` + +#### `frontend/model/core_linking.lem` (after line 215) + +```lem +| Ewhere _ _ -> + error ("TODO: free_expr Ewhere") +| Ejump _ _ _ -> + error ("TODO: free_expr Ejump") +``` + +#### `frontend/model/core_indet.lem` + +`indet_hack` (after `Erun` case, line 436): +```lem +| Core.Ewhere e defs -> + Core.Expr annot (Core.Ewhere (indet_hack e) + (List.map (fun (sym_ty, params, body) -> (sym_ty, params, indet_hack body)) defs)) +| Core.Ejump _ _ _ -> + expr +``` + +`import_expr` (after `Erun` case, line 153): +```lem +| Core.Ewhere _ _ -> error "import_expr: Ewhere not supported in indet" +| Core.Ejump _ _ _ -> error "import_expr: Ejump not supported in indet" +``` + +#### `frontend/model/core_rewrite.lem` (8 active functions) + +All follow the same pattern. For functions that **transform pexprs** (e.g. `remove_conv_int`): +```lem +| Ewhere e cases -> + Ewhere (remove_conv_int e) + (List.map (fun (sym_ty, params, body) -> + (sym_ty, params, remove_conv_int body)) cases) +| Ejump annot sym pes -> + Ejump annot sym (List.map remove_conv_int_pexpr pes) +``` + +For functions that **just traverse** (e.g. `remove_skips`, `remove_unseqs`, `sequentialise_creates_kills`, `pure_propagation2`, `simpl_case`): +```lem +| Ewhere e cases -> + Ewhere (f e) (List.map (fun (sym_ty, params, body) -> (sym_ty, params, f body)) cases) +| Ejump _ _ _ -> + expr_ +``` +where `f` is the recursive function and `expr_` is returned unchanged for `Ejump`. + +Note: `remove_seqs` and `pure_propagation` are commented out in the source — no changes needed there. + +Note: The `rewriter` record type has dead `save_rwter`/`run_rwter` fields that are never called. Do **not** add `where_rwter`/`jump_rwter` fields — the existing pattern-match functions handle constructors directly without the record. + +#### `frontend/model/core_rewrite2.lem` + +Add to the `alg_type` record (after `a_Erun`, line 314): +```lem +; a_Ewhere : 'expr -> list (('sym * core_base_type) * list ('sym * (core_base_type * maybe (Ctype.ctype * pass_by_value_or_pointer))) * 'expr) -> exceptM 'expr_ msg +; a_Ejump : 'a -> 'sym -> list 'pexpr -> exceptM 'expr_ msg +``` + +Add to `fold_expr` (after `Erun` case, line 386): +```lem +| Ewhere e defs -> + (fold_expr alg e) >>= fun e -> + (mapM (fun (sym_ty, params, body) -> + fold_expr alg body >>= fun body' -> return (sym_ty, params, body') + ) defs) >>= fun defs -> + wrap (alg.a_Ewhere e defs) +| Ejump a s pes -> + (mapM (fold_pexpr alg.pexpr_alg) pes) >>= fun pes -> + wrap (alg.a_Ejump a s pes) +``` + +Add to both default algebra records (after `a_Erun`, lines 501 and 676): +```lem +; a_Ewhere = fun e defs -> return (Ewhere e defs) +; a_Ejump = fun a b c -> return (Ejump a b c) +``` + +#### `frontend/model/core_unstruct.lem` (after `Erun`, line 332) + +```lem +| Ewhere _ _ -> + expr +| Ejump _ _ _ -> + expr +``` + +#### `frontend/model/core_typing.lem` + +Keep the labs field in the env record for saves only, add a separate one for where-labels. +Explain the context and then ask the user how to proceed for this. + +`collect_labels` (after `Erun`, line 1643): +`typecheck_expr` (after `Erun`, line 1838): + +#### `frontend/model/core_run_aux.lem` (3 locations) + +`add_to_sb` (after `Erun`, line 350): +```lem +| Ewhere e cases -> + Ewhere (add_to_sb p_aids e) + (List.map (fun (sym_ty, params, body) -> (sym_ty, params, add_to_sb p_aids body)) cases) +| Ejump annots sym pes -> + Ejump <| annots with sb_before= (Set.map snd p_aids) union annots.sb_before |> sym pes +``` + +`add_to_asw` (after `Erun`, line 435): +```lem +| Ewhere e cases -> + Ewhere (add_to_asw aids e) + (List.map (fun (sym_ty, params, body) -> (sym_ty, params, add_to_asw aids body)) cases) +| Ejump annots sym pes -> + Ejump <| annots with asw_before= aids union annots.asw_before |> sym pes +``` + +`convert_expr` (after `Erun`, line 600): +```lem +| Ewhere e cases -> + Ewhere (convert_expr e) + (List.map (fun (sym_ty, params, body) -> (sym_ty, params, convert_expr body)) cases) +| Ejump _ sym pes -> + Ejump empty_annotation sym (List.map convert_pexpr pes) +``` + +#### `frontend/model/core_run.lem` + +In the big `(arena_expr_, stack)` pattern match (after `Erun`, line 1530). +Explain the context and then ask the user how to proceed for all of these. + +```lem +| (Ewhere e _, _) -> + (* explain and ask *) + one $ Step_tau "Ewhere" TSK_Misc begin + E.return <| th_st with arena= e |> + end + +| (Ejump _ _ _, Stack_empty) -> + (* explain and ask *) + error "reached empty stack with an Ejump" + +| (Ejump _ _ _, Stack_cons Nothing _ _) -> + (* explain and ask *) + error "found a Ejump outside of a procedure" + +| (Ejump annots sym pes, Stack_cons (Just current_proc) cont sk) -> + (* explain and ask *) +``` + +#### `frontend/model/core_reduction.lem` + +The dynamics of the where-expressions are informally captured by the +following rules. The semantics are reminiscent of checked exceptions: +`Ejump` propagates outward through let-strong continuations until caught +by a matching `Ewhere`, or escapes entirely. + +``` +pe => val +---------------------------------- [Where-Pure] +pure(pe) where [..] --> pure(val) + + +exists k . l = lk +pe => val +--------------------------------------------------- [Jump-Sub] +run l(pe) where [l1 (x1) . E1, .., ln (xn) . En] -> + {val/xk} Ek where [l1 (x1) . E1, .., ln (xn) . En] + + +forall k . l <> lk +--------------------------------------------------- [Jump-Where] +run l(pe) where [l1 (x1) . E1, .., ln (xn) . En] -> + run l(pe) + + +--------------------------------------------- [Jump-Let] +let strong pat = run l(pe) in E --> run l(pe) +``` + +Also add to `has_ccall` (after `Erun`, ~line 476): +```lem +| Ejump _ _ _ -> false +| Ewhere e defs -> has_ccall e || List.any (fun (_, _, body) -> has_ccall body) defs +``` + +#### `frontend/model/core_typing.lem` + +Explain the context and then ask the user how to proceed. + +--- + +### Phase 2 – Regenerate generated files + +Run `make` from the repo root. This runs Lem on all `$(LEM_SRC)` and regenerates `ocaml_frontend/generated/*.ml`. The Lem tool itself will only warn on non-exhaustive patterns (`-wl_pat_exh warn`), but the regenerated `.ml` files will now have the correct type and all the new cases added above. + +--- + +### Phase 3 – Update non-generated OCaml files + +These match on `Core.*` types directly and must be updated **after** the type is regenerated. + +#### `ocaml_frontend/rewriters/core_rewriter.ml` (after `Erun`, line 397) + +```ocaml +| Ewhere (e, defs) -> + mapM (fun (sym_ty, params, body) -> + aux body >>= fun body' -> + return (sym_ty, params, body') + ) defs >>= fun defs' -> + aux e >>= fun e' -> + return_wrap (Ewhere (e', defs')) +| Ejump ((), sym, pes) -> + mapM aux_pexpr pes >>= fun pes' -> + return_wrap (Ejump ((), sym, pes')) +``` + +#### `ocaml_frontend/rewriters/copy_propagation.ml` (after `Erun`, line 416) + +```ocaml +| Ewhere (e, defs) -> + Expr (annots, Ewhere (propagate env e, + List.map (fun (sym_ty, params, body) -> (sym_ty, params, propagate env body)) defs)) +| Ejump (a, lbl, pes) -> + Expr (annots, Ejump (a, lbl, List.map pp pes)) +``` + +#### `ocaml_frontend/pprinters/pp_core.ml` (after `Erun`, line 660) + +```ocaml +| Ewhere (e, defs) -> + pp_keyword "where" ^^^ + P.nest 2 (P.break 1 ^^ pp e) ^^^ + pp_control "with" ^^^ + P.nest 2 (P.break 1 ^^ comma_list (fun ((sym, bTy), sym_bTy_pes, body) -> + pp_keyword "label" ^^^ pp_symbol sym ^^ P.colon ^^^ pp_core_base_type bTy ^^^ + P.parens (comma_list (fun (sym, (bTy, _)) -> + pp_symbol sym ^^ P.colon ^^^ pp_core_base_type bTy + ) sym_bTy_pes) ^^^ + pp_control "in" ^^^ + P.nest 2 (P.break 1 ^^ pp body) + ) defs) +| Ejump (_, sym, pes) -> + pp_keyword "jump" ^^^ pp_symbol sym ^^ P.parens (comma_list pp_pexpr pes) +``` + +#### `ocaml_frontend/milicore.ml` (after `Erun`, line 82) + +```ocaml +| Ewhere (e, _defs) -> + (* Labels from defs are pre-registered via m_collect_saves; just process body *) + remove_save e +| Ejump _ -> expr +``` + +#### `ocaml_frontend/rewriters/core_peval.ml` (after `Erun`, line 379) + +```ocaml +| Ewhere (e, defs) -> + let defs' = List.map (fun (sym_ty, params, body) -> + (sym_ty, params, + if List.exists (fun (z, _) -> sym = z) params then body + else subst_sym_expr2 sym z body) + ) defs in + Ewhere (subst_sym_expr2 sym z e, defs') +| Ejump (annot, lab_sym, pes) -> + Ejump (annot, lab_sym, List.map (subst_sym_pexpr2 sym z) pes) +``` + +#### `ocaml_frontend/core_remove_unused_functions.ml` + +The existing `| _ -> Traverse` catch-all already covers new cases — **no change needed**. (For correctness, `Ejump` should record a dep on its sym like `Erun` does, but that is a quality-of-life improvement, not required for the build.) + +#### `ocaml_frontend/pprinters/pp_core_ast.ml` (after `Esave`, ~line 397) + +```ocaml +| Ewhere (e, defs) -> + Dnode (pp_ctor "Ewhere", + self e :: List.map (fun ((sym, bTy), _, body) -> + Dnode (pp_ctor "def" ^^^ pp_symbol sym ^^ P.colon ^^^ Pp_core.Basic.pp_core_base_type bTy, + [self body]) + ) defs) +| Ejump (_, sym, _) -> + Dleaf (pp_ctor "Ejump" ^^^ pp_symbol sym) +``` + +Note: `milicore_label_inline.ml` already has `| _ -> Traverse` — **no change needed**. + +--- + +### Phase 4 – Regeneration and build + +```bash +make # regenerates ocaml_frontend/generated/*.ml from .lem sources +dune build # should now succeed (ignoring unrelated absint/coq errors) +``` + +--- + +## Verification + +1. `dune build 2>&1 | grep "warning 8\|partial-match"` — should be empty (for cerberus targets) +2. Run the copy_prop tests (`tests/ci/0366–0373`) to verify no regressions +3. Check that a simple C file with a `while` loop runs through the elaboration pipeline without crashing + +--- + +## Implementation sequence + +### Workflow + +Make sure to `make && make install` to build and `cd tests && ./run-ci.sh && cd ..` too. +After reviewing each change (but **before** committing): update the **Change log** section at the bottom of this document to note any deviations from the plan above. + +Each commit message header should be 50 characters wide or less. +Each commit message body should be wrapped to lines of length 72 characters. +Each commit should end with "Assisted-By: Claude Sonnet 4.6 ". + +--- + +### Commit 1 — Type fix + exhaustive stubs (build gate) + +**Goal**: Fix the `Ewhere` type in `core.lem`, add minimal stub cases to every file that pattern-matches on `generic_expr_`, run `make` to regenerate, and verify `dune build` passes. + +Every new case uses an error stub. +- `.lem`: `| Ewhere _ _ -> error "TODO Ewhere"` / `| Ejump _ _ _ -> error "TODO Ejump"` +- `.ml`: `| Ewhere _ -> failwith "TODO Ewhere"` / `| Ejump _ -> failwith "TODO Ejump"` + +`frontend/model/core_sequentialise.lem` adds `import Utils` (unqualified import, not `open`); stubs use `Utils.error`. + +**Files touched**: +- `frontend/model/core.lem` — type fix +- `frontend/model/core_sequentialise.lem` — add `import Utils`; stubs via `Utils.error` +- `frontend/model/core_aux.lem` — stubs (all 9 functions) +- `frontend/model/core_linking.lem` — stubs +- `frontend/model/core_indet.lem` — stubs +- `frontend/model/core_rewrite.lem` — stubs (all active functions) +- `frontend/model/core_rewrite2.lem` — stubs (alg_type fields added; fold_expr + default algebras are error stubs) +- `frontend/model/core_unstruct.lem` — stubs +- `frontend/model/core_typing.lem` — stubs +- `frontend/model/core_run_aux.lem` — stubs +- `frontend/model/core_run.lem` — stubs +- `frontend/model/core_reduction.lem` — stubs +- `parsers/core/core_parser.mly` — stubs (Commit 14; two match blocks) +- `backend/common/pipeline.ml` — stubs (Commit 15; `untype_expr`) +- `make` — regenerate `ocaml_frontend/generated/*.ml` +- All non-generated `.ml` files listed in Phase 3 — stubs + +**Review checklist**: +- `dune build 2>&1 | grep -c "Error"` returns 0 +- No `-w @8` partial-match warnings remain + +--- + +### Commits 2–20 — Implementations (one file per commit) + +Easy commits first; typing and execution last. Each commit: implement the +file, run `make && make install`, check the CI with `cd tests && ./run-ci.sh`, +log deviations. + +| Commit | File | Notes | +|--------|------|-------| +| 2 | `frontend/model/core_sequentialise.lem` | Simple traversal | +| 3 | `frontend/model/core_unstruct.lem` | Simple pass-through | +| 4 | `frontend/model/core_indet.lem` | `indet_hack` traversal + `import_expr` errors | +| 5 | `frontend/model/core_rewrite.lem` | 8 active traversal functions | +| 6 | `frontend/model/core_rewrite2.lem` | `alg_type` fields + real `fold_expr` + real default algebras | +| 7 | `frontend/model/core_aux.lem` | All 9 functions (rows 1–9) | +| 8 | `ocaml_frontend/pprinters/pp_core.ml` | | +| 9 | `ocaml_frontend/pprinters/pp_core_ast.ml` | | +| 10 | `ocaml_frontend/rewriters/core_rewriter.ml` | | +| 11 | `ocaml_frontend/rewriters/copy_propagation.ml` | | +| 12 | `ocaml_frontend/rewriters/core_peval.ml` | | +| 13 | `ocaml_frontend/milicore.ml` | | +| 14 | `parsers/core/core_parser.mly` | `symbolify_expr` + `register_labels` | +| 15 | `backend/common/pipeline.ml` | `untype_expr` | +| 16 | `frontend/model/core_linking.lem` | Explain and ask | +| 17 | `frontend/model/core_run_aux.lem` | 3 functions | +| 18 | `frontend/model/core_run.lem` | Explain and ask | +| 19 | `frontend/model/core_reduction.lem` | Explain and ask | +| 20 | `frontend/model/core_typing.lem` | Explain and ask | + +--- + +## Change log + +*(Updated after each review, before each commit.)* + +### Commit 1 deviations + +- **`core_sequentialise.lem`**: `error` is not in scope by default (only `Core` is opened). Added `import Utils` (not `open`) so stubs can use `Utils.error`; the real implementation will be added in Commit 2. +- **`parsers/core/core_parser.mly`**: Not in the original plan; added as Commit 14. Has two match blocks on `generic_expr_`; added `| Ejump _ -> failwith "TODO Ejump"` + `| Ewhere _ -> failwith "TODO Ewhere"` to `symbolify_expr`, and added `| Ejump _ | Ewhere _` to the no-op group in `register_labels`. +- **`backend/common/pipeline.ml`**: Not in the original plan; added as Commit 15. Has an `untype_expr` function that pattern-matches exhaustively; added stubs there. +- **`core_aux.lem` rows 5–9** (`find_labeled_continuation`, `find_labeled_continuation2_aux`, `collect_labeled_continuations`, `collect_saves_aux`, `m_collect_saves_aux`): originally planned as trivial returns (correct by mutual-exclusivity invariant), now uniformly use error stubs like all other cases. + +### Commit 2 (core_sequentialise.lem) deviations + +- Removed the temporary `import Utils` added in Commit 1 (no longer needed once real implementation is in place; `error` is not called). + +### Commit 3 (core_unstruct.lem) deviations + +- `explode_expr` is dead code — `explode_file` is never called from the pipeline. The code also appears incomplete or potentially incorrect for `Esave` (whose arguments are always pointers to local variables, thus could be pointers to structs). Both new cases return `expr` unchanged, consistent with how `Esave` and `Erun` are handled. + +### Commit 4 (core_indet.lem) — SKIPPED + +- `core_indet.lem` is almost entirely commented out; only ~11 lines are live and `hackish_order` (the pipeline entry point) is a no-op stub. There is nothing meaningful to implement. The Commit 1 stubs already satisfy the exhaustiveness requirement. Skipped entirely; no implementation commit for this file. + +### Commit 5 (core_rewrite.lem) deviations + +- `remove_dead_aux` turned out to be dead code — it is commented out of `rewrite_expr` along with four other functions (`remove_skips`, `remove_unseqs`, `sequentialise_creates_kills`, `simpl_case`). Only `flatten_seqs` and `pure_propagation2` are actually called from the pipeline. All 8 functions were implemented regardless (the dead ones still need to compile), but the commit message documents which are live vs. dead. +- For `remove_dead_aux`, `Ejump` returns `Left expr` (like `Erun`) and `Ewhere` determines `Left`/`Right` based on its main expression `e`, with label bodies traversed in both branches. + +### Commit 6 (core_rewrite2.lem) deviations + +- The entire file is dead: `Core_rewrite2.rw_file` is commented out in `pipeline.ml` and nothing else calls `fold_expr`, `id_expr_alg`, or `pfp_expr_alg`. The plan did not note this; all three locations were implemented regardless (the file still needs to compile). +- The plan described adding `a_Ewhere` / `a_Ejump` fields to the `alg_type` record type. This was done correctly. The plan's code snippets for `id_expr_alg` and `pfp_expr_alg` used the name `pfp_expr_alg`; the actual names in the file match. + +### Commit 7 (core_aux.lem) deviations + +- Rows 5–9 (`find_labeled_continuation`, `find_labeled_continuation2_aux`, `collect_labeled_continuations`, `collect_saves_aux`, `m_collect_saves_aux`) were changed from error stubs (added in Commit 1) to proper error messages explaining that those cases should not be see in the programs where `Esave/Erun` exist. They could be implemented with the trivial "no match" returns originally planned if need be/required later. + +### Commit 8 (pp_core.ml) deviations + +- The plan's proposed layout (`pp_keyword "where" ^^^ ... pp_control "with" ^^^ ...`) was rejected after review. The final format was redesigned based on user feedback through several iterations: + - `e` appears first (not inside a `where` wrapper) + - The first label definition uses `where` as its keyword, indented on a new line (via `P.nest 2 (P.hardline ^^ ...)`) + - Subsequent definitions use `and` (like OCaml's `let rec ... and ...`) + - No surrounding `[` `]` brackets, no `pp_control "with"`, no `eff` keyword before the return type +- A local helper `pp_def` was introduced to avoid repeating the per-definition layout. + +### Commit 9 (pp_core_ast.ml) deviations + +- The plan said to add after `Esave` (~line 397). In practice, `pp_core_ast.ml` was not modified in Commit 1 (no stubs were added because the existing `| _ -> Dleaf (TODO_expr ...)` catch-all kept the file buildable). The new cases were added immediately before that catch-all. + +### Commit 10 (core_rewriter.ml) deviations + +- The plan's description implied `core_rewriter` was used by `copy_propagation.ml`; it is not. `core_rewriter.ml` is used only by `remove_unspecs.ml` and `core_peval.ml`. The commit message was corrected to reflect the actual callers. + +### Commit 11 (copy_propagation.ml) deviations + +- A comment and `assert` were added to the `Esave` case explaining why + passing `env` unchanged into the body is safe: the elaboration re-uses + local var syms across `Esave` binder boundaries, but those syms are + never re-bound to a different pure value, so they are never present in + `env`. The `assert` checks this at runtime. +- `Ewhere` mirrors the pattern exactly, including its own `assert` on + each def's params. Whether the invariant is guaranteed to hold for + `Ewhere` label parameters has not been confirmed; both the comment and + assert are intentionally tentative. + +### Commit 12 (core_peval.ml) deviations + +- `core_peval.ml` is only called from `backend/playground/main.ml`; it + is not part of the main pipeline. Implemented anyway. +- `Ejump` mirrors `Erun` exactly. +- `Ewhere` mirrors `Esave`: skip body substitution if `sym` is shadowed + by that def's params. Unlike `Esave`, `Ewhere` params carry no pexprs + (no initial values), so there is nothing to substitute in the params + themselves. + +### Commit 13 (milicore.ml) deviations + +- The plan proposed `remove_save e` for `Ewhere`, treating label defs as + pre-registered via `m_collect_saves`. This is incorrect: our + `m_collect_saves_aux` returns `st` (no-op) for `Ewhere` because + `Ewhere`/`Ejump` and `Esave`/`Erun` are mutually exclusive. +- The Commit 1 stub had `Ejump _ -> expr` (pass-through) and + `Ewhere _ -> failwith "TODO Ewhere"` as separate cases. Both were + replaced with a single combined case at the end of the match: + `| Ejump _ | Ewhere _ -> failwith "should not have Ejump/Ewhere in + same program has Erun/Esave"`, making the mutual-exclusivity + invariant explicit. + +### Commit 14 (core_parser.mly) deviations + +- The original plan described two match blocks (`symbolify_expr` and + `register_labels`) with stubs. The actual commit went further and + added full surface syntax so that `--pp core` output can round-trip + through the parser. +- Three new tokens added to `core_parser_util.ml` and exer: `JUMP`, + `WHERE`, `AND`. Keywords: `"jump"`, `"where"`, `"and"`. +- One new precedence level: `%nonassoc WHERE` before `%nonassoc ELSE`, + so `WHERE` terminates any if-then-else or let-in before attaching. +- Two new non-terminals: `where_def` and `where_param`. Params use + `None` for the `ctype` annotation field (no surface syntax for it). +- The `Ewhere` grammar closes the def list with `END` (reusing the + existing token from `case...of...end`), eliminating the SR ambiguity + that arises from `AND` appearing at multiple nesting levels. No new + conflicts; count matches the pre-existing baseline. +- `pp_core.ml` updated: `pp_keyword "end"` appended after the defs list + so the printed form round-trips correctly. +- `register_labels`: `Ewhere _` is extracted from the no-op group and + given its own case that recurses into `_e` and each def's body, with + a TODO comment matching the `Eunseq` style: "save/run and jump/where + should not occur in the same program". Label syms for Ewhere are not + registered here (no `register_label` call); they are registered in + `symbolify_expr` via `under_scope` + `register_sym`. +- `symbolify_expr` for `Ewhere`: opens an outer `under_scope` for all + where-labels (visible to `e` and all bodies, out of scope outside the + block). Two passes: (1) register all label syms so mutual/forward + references resolve; (2) for each def, inner `under_scope` for params, + then symbolify body. +- `symbolify_expr` for `Ejump`: uses `lookup_sym` (not `lookup_label`) + since where-labels live in `sym_scopes`, not the flat `st.labels` map. + +### Commit 15 (pipeline.ml) deviations + +- `untype_expr` for `Ejump`: same as `Erun` — annotate unchanged, map + `untype_pexpr` over `pes`. +- `untype_expr` for `Ewhere`: recurse `untype_expr` on `e` and each + def's body; `params` have no pexprs so they are copied unchanged. + +### Commit 16 (core_linking.lem) deviations + +Globals cannot contain Esave/Erun, so Ejump/Ewhere are treated similarly. + +### Commit 17 (core_run_aux.lem) deviations + +No deviations from plan; though it should be noted that this code is dead. +(Kayvan please delete or move dead code, it costs me and Claude too much +time and effort). + +### Commit 18 (core_run.lem) deviations + +- core\_run.lem is dead code - noted in error strings explicitly + "Core_run is dead code" so future readers are not confused. + +### Commit 19a (core_run_aux.lem + core_reduction.lem helpers) deviations + +- Planned commit 19 was split in two: this commit covers the `Cwhere` + context type and all helper-function updates; the operational reduction + rules (Ewhere-Pure, Ejump-Sub/Where/Let) follow in commit 19b. +- `apply_ctx` and `get_ctx` are straightforward +- `has_ccall` and `is_unseq_with_ccall_aux` (latter calls former) cases are + also straightforward, but should be impossible for a C program (no wheres + inside an unseq) and so are commented as such +- Next 3 are simple context traversals: recurse and reconstruct + - `break_at_sseq`: locates the innermost `Csseq` in a context chain + - `break_at_bound_and_sseq`: uses `break_at_seq`, locates the nearest + `Cbound` and optionally a `Csseq` within it + - `pull_dyn_annotations` is dead: strips `Cannot` nodes from the context, + returning the annotations and a cleaned context +- `add_exclusion`: adds an exclusion ID to every `Cannot` node in the + context. `Cwhere` case recurses into the inner context and reconstructs. + That being said, the function should never see this case for a C program: + no `where` inside `bound`, and exclusions are only added inside `bound`s + +### Commit 19b (core_reduction.lem reductions) deviations + +- The plan described Ejump reductions as explicit arms in `step_ctx` + matching on `ctx` (`| Cwhere ...`, `| Csseq ...`). The actual + implementation uses one-level patterns in `one_step` instead, matching + on expression structure like the existing `Esseq(pure value)` cases. +- A new `is_ejump` predicate drives `get_ctx` to treat `Esseq pat (Ejump) + e2` and `Ewhere (Ejump) defs` as atomic redexes, so `ctx = CTX` for all + three rules. The existing `TAU` and `TAU_WITH_RUNSTATE` constructors + suffice — no new constructors or ctx parameter were needed. + +### Commit 20 (core_typing.lem) deviations + +No surprises. diff --git a/doc/history/2026-05-26_save-to-where.md b/doc/history/2026-05-26_save-to-where.md new file mode 100644 index 0000000000..2c3521d9a5 --- /dev/null +++ b/doc/history/2026-05-26_save-to-where.md @@ -0,0 +1,73 @@ +# Plan: `save_to_where` Core pass — Phase 1: scaffold + +## Context + +`Ewhere`/`Ejump` constructors are now fully wired into the Core IR, typing, +and all passes. The next step is a new rewriter `save_to_where` that will +transform procedures using `Esave`/`Erun` into ones using `Ewhere`/`Ejump`. +Phase 1 is purely structural: add the switch, create a no-op pass, and wire +it into the pipeline so the scaffold builds and runs cleanly before any +transformation logic is added. + +--- + +## Files to modify + + +### 0. Save plan + +Save this plan with an appropriate name to the `doc/` directory. + +### 1. `ocaml_frontend/switches.mli` + +Add after `SW_copy_prop`: +```ocaml +| SW_save_to_where +``` + +### 2. `ocaml_frontend/switches.ml` + +Three locations, mirroring `SW_copy_prop`: + +**Constructor** (after `SW_copy_prop`): +```ocaml +| SW_save_to_where +``` + +**`read_switch`** (after the `"copy_prop"` case, before `| _ -> None`): +```ocaml +| "save_to_where" -> Some SW_save_to_where +``` + +**Simple-equality arm of `pred`** (add to the list ending with `SW_copy_prop`): +```ocaml +| SW_save_to_where as y -> +``` + +### 3. `ocaml_frontend/rewriters/save_to_where.ml` — new file + +No-op pass, pattern identical to `remove_unspecs.ml` / `copy_propagation.ml`: +```ocaml +let transform_file core_file = core_file +``` + +### 4. `backend/common/pipeline.ml` + +After the `copy_prop` block (line ~574), add: +```ocaml +let core_file = + if Switches.(has_switch SW_save_to_where) then + Save_to_where.transform_file core_file + else + core_file in +``` + +--- + +## Verification + +```sh +make && make install +cerberus --exec --batch tests/ci/0001.c # baseline still works +cerberus --sw save_to_where --exec --batch tests/ci/0001.c # no-op, same output +``` diff --git a/frontend/model/core.lem b/frontend/model/core.lem index 952184883f..4da1cc850f 100644 --- a/frontend/model/core.lem +++ b/frontend/model/core.lem @@ -333,6 +333,8 @@ type generic_expr_ 'a 'bty 'sym = (* (effectful) expression *) | Esave of ('sym * core_base_type) * list ('sym * ((core_base_type * maybe (Ctype.ctype * pass_by_value_or_pointer)) * generic_pexpr 'bty 'sym)) * (generic_expr 'a 'bty 'sym) (* save label *) | Erun of 'a * 'sym * list (generic_pexpr 'bty 'sym) (* run from label *) | Epar of list (generic_expr 'a 'bty 'sym) (* cppmem-like thread creation *) + | Ewhere of (generic_expr 'a 'bty 'sym) * list (('sym * core_base_type) * list ('sym * (core_base_type * maybe (Ctype.ctype * pass_by_value_or_pointer))) * (generic_expr 'a 'bty 'sym)) + | Ejump of 'a * 'sym * list (generic_pexpr 'bty 'sym) (* This two only exists during the execution *) | Ewait of Mem_common.thread_id (* wait for thread termination *) diff --git a/frontend/model/core_aux.lem b/frontend/model/core_aux.lem index ef06607704..4569fa52f7 100644 --- a/frontend/model/core_aux.lem +++ b/frontend/model/core_aux.lem @@ -1029,6 +1029,15 @@ let rec subst_sym_expr sym cval (Expr annot expr_) = Esave lab_sym sym_bTy_pes' (subst_sym_expr sym cval e) | Erun annot lab_sym pes -> Erun annot lab_sym (List.map (subst_sym_pexpr sym cval) pes) + | Ejump annot lab_sym pes -> + Ejump annot lab_sym (List.map (subst_sym_pexpr sym cval) pes) + | Ewhere e defs -> + let defs' = List.map (fun (sym_ty, params, body) -> + (sym_ty, params, + if List.any (fun (z, _) -> sym = z) params then body + else subst_sym_expr sym cval body) + ) defs in + Ewhere (subst_sym_expr sym cval e) defs' | End es -> End (List.map (subst_sym_expr sym cval) es) | Epar es -> @@ -1298,6 +1307,15 @@ let rec unsafe_subst_sym_expr sym pe' (Expr annot expr_) = Esave lab_sym sym_bTy_pes' (unsafe_subst_sym_expr sym pe' e) | Erun annot lab_sym pes -> Erun annot lab_sym (List.map (unsafe_subst_sym_pexpr sym pe') pes) + | Ejump annot lab_sym pes -> + Ejump annot lab_sym (List.map (unsafe_subst_sym_pexpr sym pe') pes) + | Ewhere e defs -> + let defs' = List.map (fun (sym_ty, params, body) -> + (sym_ty, params, + if List.any (fun (z, _) -> sym = z) params then body + else unsafe_subst_sym_expr sym pe' body) + ) defs in + Ewhere (unsafe_subst_sym_expr sym pe' e) defs' | End es -> End (List.map (unsafe_subst_sym_expr sym pe') es) | Epar es -> @@ -1573,6 +1591,10 @@ let rec to_pure (Expr annot expr_) (*(expr : expr 'a)*) = Nothing | Erun _ _ _ -> Nothing + | Ejump _ _ _ -> + Nothing + | Ewhere _ _ -> + Nothing | End _ -> Nothing | Epar _ -> @@ -1648,6 +1670,11 @@ let rec subst_wait tid v (Expr annot expr_) = Esave sym sym_bTys (subst_wait tid v e) | Erun _ _ _ -> expr_ + | Ejump _ _ _ -> + expr_ + | Ewhere e defs -> + Ewhere (subst_wait tid v e) + (List.map (fun (sym_ty, params, body) -> (sym_ty, params, subst_wait tid v body)) defs) | End es -> End (List.map (subst_wait tid v) es) | Epar es -> @@ -1747,6 +1774,10 @@ let rec find_labeled_continuation sym (Expr annot expr_) = find_labeled_continuation sym e | Erun annot sym pes -> Nothing + | Ejump _ _ _ -> + error "Core_aux.find_labeled_continuation: should not have Ejump/Ewhere in same program as Erun/Esave" + | Ewhere _ _ -> + error "Core_aux.find_labeled_continuation: should not have Ejump/Ewhere in same program as Erun/Esave" | Epar es -> let () = Debug.warn [] (fun () -> "Core_aux.find_labeled_continuation assumes there are no Esave inside par()") in Nothing @@ -1826,6 +1857,10 @@ let rec find_labeled_continuation2_aux acc sym (Expr annot expr_) = find_labeled_continuation2_aux (Map.insert sym' (List.map fst sym_bTys, e) acc) sym e | Erun annot sym pes -> acc + | Ejump _ _ _ -> + error "Core_aux.find_labeled_continuation2_aux: should not have Ejump/Ewhere in same program as Erun/Esave" + | Ewhere _ _ -> + error "Core_aux.find_labeled_continuation2_aux: should not have Ejump/Ewhere in same program as Erun/Esave" | Epar es -> let () = Debug.warn [] (fun () -> "Core_aux.find_labeled_continuation2_aux assumes there are no Esave inside par()") in acc @@ -1910,6 +1945,10 @@ let rec collect_labeled_continuations (Expr annot expr_) = Map.insert sym_lab (List.map fst sym_bTys, e) $ collect_labeled_continuations e | Erun _ _ _ -> Map.empty + | Ejump _ _ _ -> + error "Core_aux.collect_labeled_continuations: should not have Ejump/Ewhere in same program as Erun/Esave" + | Ewhere _ _ -> + error "Core_aux.collect_labeled_continuations: should not have Ejump/Ewhere in same program as Erun/Esave" | End _ -> (* TODO: check *) Map.empty @@ -2239,6 +2278,10 @@ let rec collect_saves_aux st (Expr annots expr_) = e | Erun _ _ _ -> st + | Ejump _ _ _ -> + st + | Ewhere _ _ -> + st | Epar es -> let acc = List.foldl collect_saves_aux empty_saves es in @@ -2351,6 +2394,10 @@ let rec m_collect_saves_aux st (Expr annots expr_) = e | Erun _ _ _ -> st + | Ejump _ _ _ -> + error "Core_aux.m_collect_saves_aux: should not have Ejump/Ewhere in same program as Erun/Esave" + | Ewhere _ _ -> + error "Core_aux.m_collect_saves_aux: should not have Ejump/Ewhere in same program as Erun/Esave" | Epar es -> let acc = List.foldl m_collect_saves_aux m_empty_saves es in diff --git a/frontend/model/core_indet.lem b/frontend/model/core_indet.lem index 0061b517f4..e6576a68a5 100644 --- a/frontend/model/core_indet.lem +++ b/frontend/model/core_indet.lem @@ -151,6 +151,8 @@ let rec import_expr e = | Core.Ebound e -> Ebound (import_expr e) | Core.Esave k a_tys e -> Esave k a_tys (import_expr e) | Core.Erun _ k a_vs -> Erun k (map (fun (a, v) -> (a, import_expr v)) a_vs) + | Core.Ewhere _ _ -> error "import_expr: Ewhere not supported in indet" + | Core.Ejump _ _ _ -> error "import_expr: Ejump not supported in indet" | Core.Eshift e1 e2 -> Eshift (import_expr e1) (import_expr e2) end @@ -435,6 +437,10 @@ let rec indet_hack (Core.Expr annot expr_ as expr) = Core.Expr annot (Core.Esave sym sym_bTys (indet_hack e)) | Core.Erun bs sym pes -> expr + | Core.Ewhere _ _ -> + error "TODO indet_hack Ewhere" + | Core.Ejump _ _ _ -> + error "TODO indet_hack Ejump" | Core.End es -> Core.Expr annot (Core.End (map indet_hack es)) | Core.Epar es -> diff --git a/frontend/model/core_linking.lem b/frontend/model/core_linking.lem index c7960397e8..ee0e973a31 100644 --- a/frontend/model/core_linking.lem +++ b/frontend/model/core_linking.lem @@ -213,6 +213,12 @@ let rec free_expr acc (Expr _ e) = | Erun _ _ _ -> (* globals should not depend on Erun *) error ("TODO: free_expr Erun") + | Ewhere _ _ -> + (* globals should not depend on Ewhere *) + error ("TODO: free_expr Ewhere") + | Ejump _ _ _ -> + (* globals should not depend on Ejump *) + error ("TODO: free_expr Ejump") | Epar es -> List.foldl free_expr acc es | Ewait _ -> diff --git a/frontend/model/core_reduction.lem b/frontend/model/core_reduction.lem index 054e99acdf..d50829b299 100644 --- a/frontend/model/core_reduction.lem +++ b/frontend/model/core_reduction.lem @@ -193,6 +193,12 @@ let is_irreducible = function false end +let is_ejump = function + | Expr _ (Eannot _ (Expr _ (Ejump _ _ _))) -> true + | Expr _ (Ejump _ _ _) -> true + | _ -> false +end + import Debug @@ -434,6 +440,49 @@ let one_step eval_pexpr full_eval_pexpr env (Expr annots expr_ as expr) = (* reduction: ND *) Just (ND es) + | Ewhere (Expr _ (Eannot _ (Expr _ (Ejump jump_annots sym pes) as ejump_e))) defs -> + Just match List.find (fun ((sym', _), _, _) -> sym = sym') defs with + | Just ((_, _), params, body) -> + (* [Jump-Sub]: evaluate args, update env, continue in where context *) + TAU_WITH_RUNSTATE "Ejump-Sub" begin + E.foldlM (fun acc ((psym, (bTy, _)), pe) -> + full_eval_pexpr pe >>= fun cval -> + E.return (update_env (Caux.mk_sym_pat psym bTy) cval acc) + ) env (List.zip params pes) >>= fun env' -> + E.return (env', Expr annots (Ewhere body defs)) + end + | Nothing -> + (* [Jump-Where]: label not in defs, jump escapes where block *) + TAU "Ejump-Where" env ejump_e + end + + | Ewhere (Expr _ (Ejump jump_annots sym pes) as ejump_e) defs -> + Just match List.find (fun ((sym', _), _, _) -> sym = sym') defs with + | Just ((_, _), params, body) -> + (* [Jump-Sub]: evaluate args, update env, continue in where context *) + TAU_WITH_RUNSTATE "Ejump-Sub" begin + E.foldlM (fun acc ((psym, (bTy, _)), pe) -> + full_eval_pexpr pe >>= fun cval -> + E.return (update_env (Caux.mk_sym_pat psym bTy) cval acc) + ) env (List.zip params pes) >>= fun env' -> + E.return (env', Expr annots (Ewhere body defs)) + end + | Nothing -> + (* [Jump-Where]: label not in defs, jump escapes where block *) + TAU "Ejump-Where" env ejump_e + end + + | Ewhere e _ -> + (* [Where-Pure]: e is a value — guaranteed by get_ctx *) + Just (TAU "Ewhere-Pure" env e) + + | Esseq _ (Expr _ (Eannot _ (Expr _ (Ejump _ _ _ ) as ejump_e))) _ -> + (* [Jump-Let]: jump discards let-strong continuation *) + Just (TAU "Ejump-Let" env ejump_e) + | Esseq _ (Expr _ (Ejump _ _ _) as ejump_e) _ -> + (* [Jump-Let]: jump discards let-strong continuation *) + Just (TAU "Ejump-Let" env ejump_e) + | _ -> Nothing end @@ -474,6 +523,11 @@ let rec has_ccall (Expr _ expr_) = has_ccall e (* NOTE: this function should never see this case (for a C program) *) | Erun _ _ _ -> false (* NOTE: this function should never see this case (for a C program) *) + | Ejump _ _ _ -> + false + | Ewhere e defs -> + (* NOTE: this function should never see this case (for a C program) *) + has_ccall e || List.any (fun (_, _, body) -> has_ccall body) defs | Epar _ -> false (* because any ccall is in the body of another thread *) | Ewait _ -> @@ -498,6 +552,10 @@ let rec is_unseq_with_ccall_aux acc = function is_unseq_with_ccall_aux acc ctx' | Cbound _ ctx' -> is_unseq_with_ccall_aux false ctx' + | Cwhere _ _ ctx' -> + (* NOTE: this function should never see this case (for a C program): + no `where` inside `unseq` *) + is_unseq_with_ccall_aux acc ctx' end val is_unseq_with_ccall: Core_run.context -> bool @@ -540,7 +598,7 @@ let rec get_ctx (Expr annot expr_ as expr) = (Cwseq annot pat ctx e2, e) ) (get_ctx e1) | Esseq pat e1 e2 -> - if is_irreducible e1 then + if is_irreducible e1 || is_ejump e1 then [(CTX, expr)] else List.map (fun (ctx, e) -> @@ -559,6 +617,15 @@ let rec get_ctx (Expr annot expr_ as expr) = [(CTX, expr)] | Erun _ _ _ -> [(CTX, expr)] + | Ejump _ _ _ -> + [(CTX, expr)] + | Ewhere e defs -> + if is_irreducible e || is_ejump e then + [(CTX, expr)] + else + List.map (fun (ctx, e') -> + (Cwhere annot defs ctx, e') + ) (get_ctx e) | Epar _ -> [(CTX, expr)] | Ewait _ -> @@ -603,6 +670,8 @@ let rec apply_ctx ctx expr = Expr annot (Eannot xs (apply_ctx ctx' expr)) | Cbound annot ctx' -> Expr annot (Ebound (apply_ctx ctx' expr)) + | Cwhere annot defs ctx' -> + Expr annot (Ewhere (apply_ctx ctx' expr) defs) end @@ -844,6 +913,13 @@ let rec break_at_sseq ctx = Just (Cbound annots ctxA, sseq_pat, ctxB, sseq_e2) end *) + | Cwhere annots defs ctx' -> + match break_at_sseq ctx' with + | Nothing -> + Nothing + | Just (ctxA, sseq_pat, ctxB, sseq_e2) -> + Just (Cwhere annots defs ctxA, sseq_pat, ctxB, sseq_e2) + end end type break = @@ -898,6 +974,15 @@ let rec break_at_bound_and_sseq ctx = | Just (ctxA, sseq_pat, ctxB, sseq_e2) -> BOUND_WITH_SSEQ (Cbound annots CTX) ctxA sseq_pat ctxB sseq_e2 end + | Cwhere annots defs ctx' -> + match break_at_bound_and_sseq ctx' with + | NO_BOUND -> + NO_BOUND + | BOUND_NO_SSEQ ctxA ctxB -> + BOUND_NO_SSEQ (Cwhere annots defs ctxA) ctxB + | BOUND_WITH_SSEQ ctxA ctxB sseq_pat ctxC e2_sseq -> + BOUND_WITH_SSEQ (Cwhere annots defs ctxA) ctxB sseq_pat ctxC e2_sseq + end end @@ -920,6 +1005,9 @@ let rec pull_dyn_annotations z = | Cbound annots ctx -> let (acc, ctx') = pull_dyn_annotations ctx in (acc, Cbound annots ctx') + | Cwhere annots defs ctx -> + let (acc, ctx') = pull_dyn_annotations ctx in + (acc, Cwhere annots defs ctx') end let rec add_exclusion n = function @@ -941,6 +1029,10 @@ let rec add_exclusion n = function Cannot annots xs' (add_exclusion n ctx') | Cbound annots ctx' -> Cbound annots (add_exclusion n ctx') + | Cwhere annots defs ctx' -> + (* NOTE: this function should never see this case (for a C program): + no `where` inside `bound`, and exclusions are only added inside `bound`s *) + Cwhere annots defs (add_exclusion n ctx') end diff --git a/frontend/model/core_rewrite.lem b/frontend/model/core_rewrite.lem index e439a60edd..190e842d7d 100644 --- a/frontend/model/core_rewrite.lem +++ b/frontend/model/core_rewrite.lem @@ -208,6 +208,11 @@ let rec remove_skips (Expr annot expr_ as expr) = | Erun _ _ _ -> (* unchanged *) expr + | Ejump _ _ _ -> + expr + | Ewhere e defs -> + Expr annot (Ewhere (remove_skips e) + (List.map (fun (sym_ty, params, body) -> (sym_ty, params, remove_skips body)) defs)) | Epar es -> (* just traversing *) Expr annot (Epar (List.map remove_skips es)) @@ -327,6 +332,11 @@ let rec remove_unseqs (Expr annot expr_ as expr) = | Erun _ _ _ -> (* unchanged *) expr + | Ejump _ _ _ -> + expr + | Ewhere e defs -> + Expr annot (Ewhere (remove_unseqs e) + (List.map (fun (sym_ty, params, body) -> (sym_ty, params, remove_unseqs body)) defs)) | Epar es -> (* just traversing *) Expr annot (Epar (List.map remove_unseqs es)) @@ -527,6 +537,16 @@ let rec remove_dead_aux (Expr annot expr_ as expr) = end | Erun _ _ _ -> Left expr + | Ejump _ _ _ -> + Left expr + | Ewhere e defs -> + let defs' = List.map (fun (sym_ty, params, body) -> + (sym_ty, params, extract_either (remove_dead_aux body)) + ) defs in + match remove_dead_aux e with + | Left e' -> Left (Expr annot (Ewhere e' defs')) + | Right e' -> Right (Expr annot (Ewhere e' defs')) + end | Epar es -> let _rev_es' = List.foldl (fun _acc _e' -> match (_e', _acc) with @@ -620,6 +640,11 @@ let rec flatten_seqs (Expr annot expr_ as expr) = Expr annot (Esave sym sym_bTys (flatten_seqs e)) | Erun _ _ _ -> expr + | Ejump _ _ _ -> + expr + | Ewhere e defs -> + Expr annot (Ewhere (flatten_seqs e) + (List.map (fun (sym_ty, params, body) -> (sym_ty, params, flatten_seqs body)) defs)) | Epar es -> Expr annot (Epar (List.map flatten_seqs es)) | Ewait _ -> @@ -804,6 +829,11 @@ let rec remove_conv_int (Expr annot expr_) = end (remove_conv_int e) | Erun annot sym pes -> Erun annot sym (List.map remove_conv_int_pexpr pes) + | Ejump annot sym pes -> + Ejump annot sym (List.map remove_conv_int_pexpr pes) + | Ewhere e defs -> + Ewhere (remove_conv_int e) + (List.map (fun (sym_ty, params, body) -> (sym_ty, params, remove_conv_int body)) defs) | Epar es -> Epar (List.map remove_conv_int es) | Ewait _ -> @@ -927,6 +957,11 @@ let rec sequentialise_creates_kills (Expr annot expr_) = Esave sym_bTy sym_bTy_pes (sequentialise_creates_kills e) | Erun _ _ _ -> expr_ + | Ejump _ _ _ -> + expr_ + | Ewhere e defs -> + Ewhere (sequentialise_creates_kills e) + (List.map (fun (sym_ty, params, body) -> (sym_ty, params, sequentialise_creates_kills body)) defs) | Epar es -> Epar (List.map sequentialise_creates_kills es) | Ewait _ -> @@ -1234,6 +1269,11 @@ let rec pure_propagation2 (Expr annot expr_ as expr) = Expr annot (Esave sym sym_tys (pure_propagation2 e)) | Erun _ _ _ -> expr + | Ejump _ _ _ -> + expr + | Ewhere e defs -> + Expr annot (Ewhere (pure_propagation2 e) + (List.map (fun (sym_ty, params, body) -> (sym_ty, params, pure_propagation2 body)) defs)) | Epar es -> Expr annot (Epar (List.map pure_propagation2 es)) | Ewait _ -> @@ -1430,6 +1470,11 @@ let rec simpl_case (Expr annot expr_ as expr) = wrap $ Esave sym_bTy xs (simpl_case e) | Erun _ _ _ -> expr + | Ejump _ _ _ -> + expr + | Ewhere e defs -> + wrap $ Ewhere (simpl_case e) + (List.map (fun (sym_ty, params, body) -> (sym_ty, params, simpl_case body)) defs) | Epar es -> wrap $ Epar (List.map simpl_case es) | Ewait _ -> diff --git a/frontend/model/core_rewrite2.lem b/frontend/model/core_rewrite2.lem index 374fda2d34..7e3544603f 100644 --- a/frontend/model/core_rewrite2.lem +++ b/frontend/model/core_rewrite2.lem @@ -312,6 +312,8 @@ type expr_alg 'sym 'bty 'ov 'lv 'value 'pexpr 'a 'action_ 'action 'paction 'expr ; a_End : list 'expr -> exceptM 'expr_ msg ; a_Esave : ('sym * core_base_type) -> list ('sym * (core_base_type * generic_pexpr 'bty 'sym)) -> 'expr -> exceptM 'expr_ msg ; a_Erun : 'a -> 'sym -> list 'pexpr -> exceptM 'expr_ msg + ; a_Ewhere : 'expr -> list (('sym * core_base_type) * list ('sym * (core_base_type * maybe (Ctype.ctype * pass_by_value_or_pointer))) * 'expr) -> exceptM 'expr_ msg + ; a_Ejump : 'a -> 'sym -> list 'pexpr -> exceptM 'expr_ msg ; a_Epar : list 'expr -> exceptM 'expr_ msg ; a_Ewait : Mem_common.thread_id -> exceptM 'expr_ msg ; a_Epack : Symbol.identifier -> list 'pexpr -> exceptM 'expr_ msg @@ -384,6 +386,15 @@ let rec fold_expr alg e = | Erun a s pes -> (mapM (fold_pexpr alg.pexpr_alg) pes) >>= fun pes -> wrap (alg.a_Erun a s pes) + | Ewhere e defs -> + (fold_expr alg e) >>= fun e -> + (mapM (fun (sym_ty, params, body) -> + fold_expr alg body >>= fun body' -> return (sym_ty, params, body') + ) defs) >>= fun defs' -> + wrap (alg.a_Ewhere e defs') + | Ejump a s pes -> + (mapM (fold_pexpr alg.pexpr_alg) pes) >>= fun pes -> + wrap (alg.a_Ejump a s pes) | Epar es -> (mapM (fold_expr alg) es) >>= fun es -> wrap (alg.a_Epar es) @@ -499,6 +510,8 @@ let id_expr_alg action_alg pexpr_alg = ; a_End = fun a -> return (End a) ; a_Esave = fun a b c -> return (Esave a b c) ; a_Erun = fun a b c -> return (Erun a b c) + ; a_Ewhere = fun e defs -> return (Ewhere e defs) + ; a_Ejump = fun a b c -> return (Ejump a b c) ; a_Epar = fun a -> return (Epar a) ; a_Ewait = fun a -> return (Ewait a) ; a_Epack = fun id es -> return (Epack id es) @@ -674,6 +687,8 @@ let pfp_expr_alg action_alg pexpr_alg = ; a_End = fun a -> return (End a) ; a_Esave = fun a b c -> return (Esave a b c) ; a_Erun = fun a b c -> return (Erun a b c) + ; a_Ewhere = fun e defs -> return (Ewhere e defs) + ; a_Ejump = fun a b c -> return (Ejump a b c) ; a_Epar = fun a -> return (Epar a) ; a_Ewait = fun a -> return (Ewait a) ; a_Epack = fun id es -> return (Epack id es) diff --git a/frontend/model/core_run.lem b/frontend/model/core_run.lem index 0c628d2370..c622de6a62 100644 --- a/frontend/model/core_run.lem +++ b/frontend/model/core_run.lem @@ -1500,12 +1500,16 @@ BEFORE EVAL_PEXPR2 E.return <| th_st with arena= e' |> ) + | (Ewhere _ _, _) -> + error "Core_run.core_thread_step2: Ewhere not implemented (was dead code)" + | (Ejump _ _ _, _) -> + error "Core_run.core_thread_step2: Ejump not implemented (was dead code)" | (Erun _ _ _, Stack_empty) -> error "reached empty stack with an Erun" - + | (Erun _ _ _, Stack_cons Nothing _ _) -> error "found a Erun outside of a procedure" - + | (Erun annots sym pes, Stack_cons (Just current_proc) cont sk) -> one $ Step_tau "Erun" TSK_Misc begin SEU.read (fun st -> diff --git a/frontend/model/core_run_aux.lem b/frontend/model/core_run_aux.lem index 5f5c35e98f..edeafd5b5a 100644 --- a/frontend/model/core_run_aux.lem +++ b/frontend/model/core_run_aux.lem @@ -32,6 +32,11 @@ type context (* core_run_annotation unit Symbol.sym *) = | Csseq of list Annot.annot * Core.pattern * context * Core.expr core_run_annotation | Cannot of list Annot.annot * list Core.dyn_annotation * context | Cbound of list Annot.annot * context + | Cwhere of list Annot.annot + * list ((Symbol.sym * core_base_type) + * list (Symbol.sym * (core_base_type * maybe (Ctype.ctype * pass_by_value_or_pointer))) + * Core.expr core_run_annotation) + * context let rec stringFromContext ctx = match ctx with @@ -47,6 +52,8 @@ let rec stringFromContext ctx = "Cannot[" ^ stringFromContext ctx' ^ "]" | Cbound _ ctx' -> "Cbound[" ^ stringFromContext ctx' ^ "]" + | Cwhere _ _ ctx' -> + "Cwhere[" ^ stringFromContext ctx' ^ "]" end instance (Show context) let show ctx = stringFromContext ctx @@ -348,6 +355,12 @@ let rec add_to_sb p_aids (Expr annot expr_ as expr) = Esave sym_bTy xs (add_to_sb p_aids e) | Erun annots sym pes -> Erun <| annots with sb_before= (Set.map snd p_aids) union annots.sb_before |> sym pes + | Ejump annots sym pes -> + Ejump <| annots with sb_before= (Set.map snd p_aids) union annots.sb_before |> sym pes + | Ewhere e defs -> + Ewhere (add_to_sb p_aids e) + (List.map (fun (sym_ty, params, body) -> + (sym_ty, params, add_to_sb p_aids body)) defs) | Epar es -> Epar (List.map (add_to_sb p_aids) es) | Ewait _ -> @@ -433,6 +446,12 @@ let rec add_to_asw aids (Expr annot expr_ as expr) = Esave sym_bTy xs (add_to_asw aids e) | Erun annots sym pes -> Erun <| annots with asw_before= aids union annots.asw_before |> sym pes + | Ejump annots sym pes -> + Ejump <| annots with asw_before= aids union annots.asw_before |> sym pes + | Ewhere e defs -> + Ewhere (add_to_asw aids e) + (List.map (fun (sym_ty, params, body) -> + (sym_ty, params, add_to_asw aids body)) defs) | End es -> End (List.map (add_to_asw aids) es) | Epar es -> @@ -598,6 +617,12 @@ let rec convert_expr (Expr annot expr_) = Esave sym (List.map (fun (sym, (bTy, pe)) -> (sym, (bTy, convert_pexpr pe))) xs) (convert_expr e) | Erun _ sym pes -> Erun empty_annotation sym (List.map convert_pexpr pes) + | Ejump _ sym pes -> + Ejump empty_annotation sym (List.map convert_pexpr pes) + | Ewhere e defs -> + Ewhere (convert_expr e) + (List.map (fun (sym_ty, params, body) -> + (sym_ty, params, convert_expr body)) defs) | End es -> End (List.map convert_expr es) | Epar es -> diff --git a/frontend/model/core_sequentialise.lem b/frontend/model/core_sequentialise.lem index 98902df093..6e977a7bee 100644 --- a/frontend/model/core_sequentialise.lem +++ b/frontend/model/core_sequentialise.lem @@ -55,6 +55,11 @@ let rec sequentialise_expr (Expr annot expr_) = Esave sym_ty xs (sequentialise_expr e) | Erun () sym es -> expr_ + | Ejump () sym es -> + expr_ + | Ewhere e cases -> + Ewhere (sequentialise_expr e) + (List.map (fun (sym_ty, params, body) -> (sym_ty, params, sequentialise_expr body)) cases) | Epar es -> Epar (List.map sequentialise_expr es) | Ewait _ -> diff --git a/frontend/model/core_typing.lem b/frontend/model/core_typing.lem index 398c099873..e078da3e3e 100644 --- a/frontend/model/core_typing.lem +++ b/frontend/model/core_typing.lem @@ -1599,6 +1599,108 @@ let memop_signature = function end +type expr_style = + | ExprStyle_save + | ExprStyle_where + +val merge_styles: Loc.t -> maybe expr_style -> maybe expr_style -> E.eff (maybe expr_style) +let merge_styles loc s1 s2 = + match (s1, s2) with + | (Nothing, _) -> E.return s2 + | (_, Nothing) -> E.return s1 + | (Just ExprStyle_save, Just ExprStyle_save) -> E.return (Just ExprStyle_save) + | (Just ExprStyle_where, Just ExprStyle_where) -> E.return (Just ExprStyle_where) + | _ -> E.fail loc MixedLabelStyles + end + +val check_label_style_aux: forall 'a 'bty. bool -> Core.generic_expr 'a 'bty Symbol.sym -> E.eff (maybe expr_style) +let rec check_label_style_aux in_ctx (Expr annots expr_) = + let loc = Annot.get_loc_ annots in + match expr_ with + | Epure _ -> + E.return Nothing + | Ememop _ _ -> + E.return Nothing + | Eaction _ -> + E.return Nothing + | Eccall _ _ _ _ -> + E.return Nothing + | Eproc _ _ _ -> + E.return Nothing + | Ewait _ -> + E.return Nothing + | Eexcluded _ _ -> + E.return Nothing + | Eannot _ e -> + check_label_style_aux in_ctx e + | Eif _ e1 e2 -> + check_label_style_aux in_ctx e1 >>= fun s1 -> + check_label_style_aux in_ctx e2 >>= fun s2 -> + merge_styles loc s1 s2 + | Esseq _ e1 e2 -> + check_label_style_aux in_ctx e1 >>= fun s1 -> + check_label_style_aux in_ctx e2 >>= fun s2 -> + merge_styles loc s1 s2 + | Elet _ _ e -> + check_label_style_aux false e + | Ewseq _ e1 e2 -> + check_label_style_aux false e1 >>= fun s1 -> + check_label_style_aux false e2 >>= fun s2 -> + merge_styles loc s1 s2 + | Ecase _ cases -> + E.foldlM (fun acc (_, e) -> + check_label_style_aux in_ctx e >>= fun s -> + merge_styles loc acc s + ) Nothing cases + | Ebound e -> + check_label_style_aux false e + | End es -> + E.foldlM (fun acc e -> + check_label_style_aux false e >>= fun s -> + merge_styles loc acc s + ) Nothing es + | Eunseq es -> + E.foldlM (fun acc e -> + check_label_style_aux false e >>= fun s -> + merge_styles loc acc s + ) Nothing es + | Epar es -> + E.foldlM (fun acc e -> + check_label_style_aux false e >>= fun s -> + merge_styles loc acc s + ) Nothing es + | Erun _ _ _ -> + if not in_ctx then + E.fail loc (LabelOutsideContext "Erun") + else + E.return (Just ExprStyle_save) + | Esave _ _ e -> + if not in_ctx then + E.fail loc (LabelOutsideContext "Esave") + else + check_label_style_aux true e >>= fun s -> + merge_styles loc (Just ExprStyle_save) s + | Ejump _ _ _ -> + if not in_ctx then + E.fail loc (LabelOutsideContext "Ejump") + else + E.return (Just ExprStyle_where) + | Ewhere e defs -> + if not in_ctx then + E.fail loc (LabelOutsideContext "Ewhere") + else + check_label_style_aux true e >>= fun s -> + E.foldlM (fun acc (_, _, body) -> + check_label_style_aux true body >>= fun s' -> + merge_styles loc acc s' + ) s defs >>= fun s_defs -> + merge_styles loc (Just ExprStyle_where) s_defs + end + +val check_label_style: forall 'a 'bty. Core.generic_expr 'a 'bty Symbol.sym -> E.eff (maybe expr_style) +let check_label_style e = check_label_style_aux true e + + val collect_labels: forall 'bty 'a. typing_env -> Core.generic_expr 'a 'bty Symbol.sym -> E.eff typing_env let rec collect_labels env (Expr _ expr_) = match expr_ with @@ -1641,6 +1743,10 @@ let rec collect_labels env (Expr _ expr_) = collect_labels <| env with labs= Map.insert sym (bTy, List.map (fun (_, ((z,_), _)) -> z) sym_bTy_pes) env.labs |> e | Erun _ _ _ -> E.return env + | Ejump _ _ _ -> + E.return env + | Ewhere _ _ -> + E.return env | Epar es -> E.foldlM (fun env' e -> collect_labels env' e @@ -1834,8 +1940,28 @@ and typecheck_expr callconv tagDefs (env: typing_env) expected_bTy (Expr annot e ) (List.zip bTys pes) end | Nothing -> - E.fail loc (CoreTyping_TODO "Erun, undeclared label") + E.fail loc (UndeclaredLabel sym) + end + | Ejump annot sym pes -> + match Map.lookup sym env.labs with + | Just (_, bTys) -> + Ejump annot sym <$> E.mapM (fun (bTy, pe) -> + typecheck_pexpr tagDefs env bTy pe >>= export_pexpr + ) (List.zip bTys pes) + | Nothing -> + E.fail loc (UndeclaredLabel sym) end + | Ewhere e defs -> + let labs_env = List.foldl (fun acc ((sym, bTy), params, _) -> + <| acc with labs= Map.insert sym (bTy, List.map (fun (_, (z, _)) -> z) params) acc.labs |> + ) env defs in + E.mapM (fun ((sym, bTy), params, body) -> + let params_decls = List.map (fun (z, (z_bTy, _)) -> (Sym z, TDsym z_bTy)) params in + let env' = <| labs_env with decls= Map.(union) (Map.fromList params_decls) labs_env.decls |> in + typecheck_expr env' bTy body >>= fun body' -> + E.return ((sym, bTy), params, body') + ) defs >>= fun defs' -> + Ewhere <$> typecheck_expr labs_env expected_bTy e <*> E.return defs' | Epar es -> if List.length es < 2 then E.fail loc (CoreTyping_TODO "Epar must have at least 2 operands") @@ -1907,7 +2033,11 @@ let typecheck_program file = E.return (BuiltinDecl loc bTy bTys) | Proc loc mrk bTy sym_bTys e -> let env' = List.foldr (fun (sym, bTy) acc -> insert_tdecl (Sym sym) (TDsym bTy) acc) env sym_bTys in - collect_labels env' e >>= fun env' -> + check_label_style e >>= fun style -> + (match style with + | Just ExprStyle_where -> E.return env' + | _ -> collect_labels env' e + end) >>= fun env' -> Proc loc mrk bTy sym_bTys <$> typecheck_expr env' bTy e end) file.stdlib >>= fun stdlib' -> @@ -1925,7 +2055,11 @@ let typecheck_program file = E.foldlM (fun (env_acc, acc) (sym, decl) -> match decl with | GlobalDef (bTy, ct) e -> - collect_labels env_acc e >>= fun env_acc' -> + check_label_style e >>= fun style -> + (match style with + | Just ExprStyle_where -> E.return env_acc + | _ -> collect_labels env_acc e + end) >>= fun env_acc' -> typecheck_expr env_acc' bTy e >>= fun te -> E.return (insert_tdecl (Sym sym) (TDsym bTy) env_acc', (sym, GlobalDef (bTy, ct) te) :: acc) | GlobalDecl (bTy, ct) -> @@ -1960,7 +2094,11 @@ let typecheck_program file = E.return (BuiltinDecl loc bTy bTys) | Proc loc mrk bTy sym_bTys e -> let env' = List.foldr (fun (sym, bTy) acc -> insert_tdecl (Sym sym) (TDsym bTy) acc) env sym_bTys in - collect_labels env' e >>= fun env' -> + check_label_style e >>= fun style -> + (match style with + | Just ExprStyle_where -> E.return env' + | _ -> collect_labels env' e + end) >>= fun env' -> Proc loc mrk bTy sym_bTys <$> typecheck_expr env' bTy e end) file.funs >>= fun funs' -> diff --git a/frontend/model/core_unstruct.lem b/frontend/model/core_unstruct.lem index 3fbf8fbe00..9699f1e33f 100644 --- a/frontend/model/core_unstruct.lem +++ b/frontend/model/core_unstruct.lem @@ -331,6 +331,10 @@ let rec explode_expr env (Expr annot expr_ as expr) = expr | Erun _ _ _ -> expr + | Ejump _ _ _ -> + expr + | Ewhere _ _ -> + expr | Epar es -> wrap (Epar (List.map self es)) | Ewait _ -> diff --git a/frontend/model/errors.lem b/frontend/model/errors.lem index f3d26090c7..4c19df5cac 100644 --- a/frontend/model/errors.lem +++ b/frontend/model/errors.lem @@ -35,6 +35,9 @@ type core_typing_cause = | CFunctionReturnType | TooGeneral | CoreTyping_TODO of string (* TODO: get rid of this constructor eventually *) + | UndeclaredLabel of Symbol.sym + | MixedLabelStyles + | LabelOutsideContext of string (* construct name *) (* NOTE: I cannot fire these errors *) | HeterogenousList of core_base_type (* expected *) * core_base_type (* found *) | InvalidTag of Symbol.sym diff --git a/ocaml_frontend/milicore.ml b/ocaml_frontend/milicore.ml index 686aec52dc..355be891cb 100644 --- a/ocaml_frontend/milicore.ml +++ b/ocaml_frontend/milicore.ml @@ -86,6 +86,8 @@ let rec remove_save expr = | Eexcluded _ -> expr | End es -> wrap (End (List.map remove_save es)) + | Ejump _ | Ewhere _ -> + failwith "should not have Ejump/Ewhere in same program has Erun/Esave" let core_to_micore__funmap_decl update_loc = function diff --git a/ocaml_frontend/pprinters/pp_core.ml b/ocaml_frontend/pprinters/pp_core.ml index 23f2838952..a012368a1c 100644 --- a/ocaml_frontend/pprinters/pp_core.ml +++ b/ocaml_frontend/pprinters/pp_core.ml @@ -544,6 +544,8 @@ let pp_pexpr pe = end end in pp None pe +let pp_argument (sym, bTy) = + pp_symbol sym ^^ P.colon ^^^ pp_core_base_type bTy let rec pp_expr expr = let rec pp (*is_semi prec*) (Expr (annot, e)) = @@ -658,6 +660,40 @@ let rec pp_expr expr = P.nest 2 (P.break 1 ^^ pp e) | Erun (_, sym, pes) -> pp_keyword "run" ^^^ pp_symbol sym ^^ P.parens (comma_list pp_pexpr pes) + | Ejump (_, sym, pes) -> + pp_keyword "jump" ^^^ pp_symbol sym ^^ P.parens (comma_list pp_pexpr pes) + | Ewhere (e, defs) -> + (* "where" keyword binds tightest to exprs *) + let needs_paren = + let (Expr (_, expr_)) = e in + match expr_ with + | Eif _ | Esseq _ | Ewseq _ | Esave _ | Elet _ -> + (* end with an expr *) + true + | Epure _ | Ememop _ | Eaction _ | Ecase _ | Eccall _ + | Eproc _ | Eunseq _ | Ebound _ | End _ | Erun _ | Epar _ + | Ewhere _ | Ejump _ | Ewait _ | Eannot _ | Eexcluded _ -> + (* end with a token *) + false in + let pp_def kw ((sym, bTy), params, body) = + kw ^^^ pp_symbol sym ^^^ + P.parens (comma_list (fun (s, (sBTy, _)) -> pp_argument (s, sBTy)) params) ^^^ + P.colon ^^^ pp_core_base_type bTy ^^^ + P.colon ^^ P.equals ^^ + P.nest 2 (P.break 1 ^^ pp body) + in + (match defs with + | [] -> assert false + | first :: rest -> + (if needs_paren then P.parens else Fun.id) (pp e) ^^ + P.nest 2 ( + P.hardline ^^ pp_def (pp_control "where") first ^^ + P.concat (List.map (fun def -> + P.hardline ^^ pp_def (pp_keyword "and") def + ) rest) ^^ + P.hardline ^^ pp_keyword "end" + ) + ) | Epar es -> with_grouped_args (pp_keyword "par") (List.map pp es) | Ewait tid -> @@ -766,9 +802,6 @@ let pp_tagDefinitions tagDefs = ^^ P.nest 2 (P.break 1 ^^ P.separate_map (P.break 1) pp_tag tags) in P.separate_map (P.break 1 ^^ P.break 1) pp tagDefs -let pp_argument (sym, bTy) = - pp_symbol sym ^^ P.colon ^^^ pp_core_base_type bTy - let pp_params params = P.parens (comma_list pp_argument params) diff --git a/ocaml_frontend/pprinters/pp_core_ast.ml b/ocaml_frontend/pprinters/pp_core_ast.ml index 644d5f6c14..6ab4333ccb 100644 --- a/ocaml_frontend/pprinters/pp_core_ast.ml +++ b/ocaml_frontend/pprinters/pp_core_ast.ml @@ -400,6 +400,14 @@ let dtree_of_expr expr = | Epar of ('a, 'bty, 'sym) generic_expr list | Ewait of Mem_common.thread_id *) + | Ejump (_, sym, _) -> + Dleaf (pp_ctor "Ejump" ^^^ pp_symbol sym) + | Ewhere (e, defs) -> + Dnode (pp_ctor "Ewhere", + self e :: List.map (fun ((sym, bTy), _, body) -> + Dnode (pp_ctor "label" ^^^ pp_symbol sym ^^ P.colon ^^^ + Pp_core.Basic.pp_core_base_type bTy, [self body]) + ) defs) | _ -> Dleaf (pp_ctor ("TODO_expr ==> " ^ String_core.string_of_expr expr)) in diff --git a/ocaml_frontend/pprinters/pp_errors.ml b/ocaml_frontend/pprinters/pp_errors.ml index 2d02b5e504..6bad032e73 100644 --- a/ocaml_frontend/pprinters/pp_errors.ml +++ b/ocaml_frontend/pprinters/pp_errors.ml @@ -484,6 +484,12 @@ let string_of_core_typing_cause = function "InvalidTag(" ^ Pp_symbol.to_string tag_sym ^ ")" | InvalidMember (tag_sym, Symbol.Identifier (_, memb_str)) -> "InvalidMember(" ^ Pp_symbol.to_string tag_sym ^ ", " ^ memb_str ^ ")" + | UndeclaredLabel0 sym -> + "undeclared label '" ^ string_of_sym sym ^ "'" + | MixedLabelStyles -> + "procedure body mixes Erun/Esave and Ejump/Ewhere label styles" + | LabelOutsideContext construct -> + construct ^ " appears outside its allowed context" | CoreTyping_TODO str -> "CoreTyping_TODO(" ^ str ^ ")" diff --git a/ocaml_frontend/rewriters/copy_propagation.ml b/ocaml_frontend/rewriters/copy_propagation.ml index 30dbef8d0c..4db0ebe973 100644 --- a/ocaml_frontend/rewriters/copy_propagation.ml +++ b/ocaml_frontend/rewriters/copy_propagation.ml @@ -409,11 +409,24 @@ let rec propagate_expr ~unwrap_loaded env (Expr (annots, e_) as expr) = | Eunseq es -> Expr (annots, Eunseq (List.map (propagate env) es)) | Esave (sym_bty, args, body) -> + (* This is correct, but for subtle reasons. The elaboration re-uses local + var syms across the Esave binder boundary, but as a result, those + symbols are never re-bound to any other value, i.e. the parameters of + Esave will never be in env. *) + assert (List.for_all (fun (sym, _) -> not (Pmap.mem sym env)) args); Expr (annots, Esave (sym_bty, List.map (fun (s, (type_info, pe1)) -> (s, (type_info, pp pe1))) args, propagate env body)) | Erun (a, lbl, pes) -> Expr (annots, Erun (a, lbl, List.map pp pes)) + | Ejump (a, lbl, pes) -> + Expr (annots, Ejump (a, lbl, List.map pp pes)) + | Ewhere (e, defs) -> + (* Same sym-reuse caveat as Esave above applies to label bodies. *) + Expr (annots, Ewhere (propagate env e, + List.map (fun (sym_ty, params, body) -> + assert (List.for_all (fun (sym, _) -> not (Pmap.mem sym env)) params); + (sym_ty, params, propagate env body)) defs)) | Ebound e -> Expr (annots, Ebound (propagate env e)) | Eannot (fps, e) -> diff --git a/ocaml_frontend/rewriters/core_peval.ml b/ocaml_frontend/rewriters/core_peval.ml index 84c1056347..efb1fef63c 100644 --- a/ocaml_frontend/rewriters/core_peval.ml +++ b/ocaml_frontend/rewriters/core_peval.ml @@ -377,6 +377,16 @@ let rec subst_sym_expr2 sym z (Expr (annot, expr_)) = Esave (lab_sym, sym_bTy_pes', subst_sym_expr2 sym z e) | Erun (annot, lab_sym, pes) -> Erun (annot, lab_sym, List.map (subst_sym_pexpr2 sym z) pes) + | Ejump (annot, lab_sym, pes) -> + Ejump (annot, lab_sym, List.map (subst_sym_pexpr2 sym z) pes) + | Ewhere (e, defs) -> + let defs' = List.map (fun (sym_ty, params, body) -> + (sym_ty, params, + (* TODO: revisit when scoping is clearer (ideally labels are closed) *) + if List.exists (fun (s, _) -> sym = s) params then body + else subst_sym_expr2 sym z body) + ) defs in + Ewhere (subst_sym_expr2 sym z e, defs') | End es -> End (List.map (subst_sym_expr2 sym z) es) | Epar es -> diff --git a/ocaml_frontend/rewriters/core_rewriter.ml b/ocaml_frontend/rewriters/core_rewriter.ml index 16176244eb..828dcc2bb3 100644 --- a/ocaml_frontend/rewriters/core_rewriter.ml +++ b/ocaml_frontend/rewriters/core_rewriter.ml @@ -395,6 +395,16 @@ module Rewriter = functor (Eff: Monad) -> struct | Erun ((), sym, pes) -> mapM aux_pexpr pes >>= fun pes' -> return_wrap (Erun ((), sym, pes')) + | Ejump ((), sym, pes) -> + mapM aux_pexpr pes >>= fun pes' -> + return_wrap (Ejump ((), sym, pes')) + | Ewhere (e, defs) -> + mapM (fun (sym_ty, params, body) -> + aux body >>= fun body' -> + return (sym_ty, params, body') + ) defs >>= fun defs' -> + aux e >>= fun e' -> + return_wrap (Ewhere (e', defs')) | Epar es -> mapM aux es >>= fun es' -> return_wrap (Epar es') diff --git a/ocaml_frontend/rewriters/save_to_where.ml b/ocaml_frontend/rewriters/save_to_where.ml new file mode 100644 index 0000000000..07e219a383 --- /dev/null +++ b/ocaml_frontend/rewriters/save_to_where.ml @@ -0,0 +1,679 @@ +(* This file is for transforming Core programs which use run/save, into Core + programs which use a jump/where, a more compositional construct with the + following semantics (plus context reduction, omitted). + + [Where-Pure] + pe => val + --------------------------------- + pure(pe) where defs end --> pure(val) + + [Jump-Sub] + pe => val + defs(l) = x . E + ---------------------------------------------- + jump l(pe) where defs end --> {val/x} E where defs + + [Jump-Where] + pe => val + l not in defs + ------------------------------------ + jump l(pe) where defs end --> jump l(val) + + [Jump-Let] + pe => val + --------------------------------------- + lets _ = jump l(pe) in E --> jump l(val) + + Semantics are reminiscent of checked exceptions: jump + propagates out through let-strong continuations until caught + by an enclosing where. + + We do this in 2 stages: + 1. Annotate the AST with dominator context for each label. + - First, a bottom-up pass which annotates each node with a map from labels + to number of children which refer to that label. + - Second, a top-down pass uses that information to find the tightest node + which encloses all uses of a label. + 2. Start from a label, and capture its context outwards. + Since labels can share contexts, multiple can be capturing + at the same time, and this is tracked. + At each dominator context, remove the dominated labels from + the tracked set. + When the set of live labels is empty, that is where we place a + where-expression. + + We simplifiy the problem by observing (in the absence of GCC statement + expressions) labels only occur inside some combination of Esseq, + Eif, Ecase, Esave. *) + +open Core + +open Cerb_colour +open Cerb_pp_prelude + +type pattern = Symbol.sym generic_pattern + +type pexpr = (unit, Symbol.sym) generic_pexpr + +type expr = (unit, unit, Symbol.sym) generic_expr + +type 'a param = { + name : Symbol.sym; + bTy : core_base_type; + optCTy : (Ctype.ctype * pass_by_value_or_pointer) option; + pexpr : 'a; +} + +let param_map f { name; bTy; optCTy; pexpr } = + { name; bTy; optCTy; pexpr = f pexpr } + +type 'info where = { + info : 'info; + annot : Annot.annot list; + node : 'info where_ +} + +and 'info where_ = + | Base of (unit, unit, Symbol.sym) generic_expr_ + | If of pexpr * 'info where * 'info where + | Sseq of pattern * 'info where * 'info where + | Case of pexpr * (pattern * 'info where) list + | Run of Symbol.sym * pexpr list + | Jump of Symbol.sym * pexpr list + | Where of 'info where * ('info, unit) label_def list + | Save of ('info, pexpr) label_def + +and ('info, 'pexpr) label_def = { + label : Symbol.sym; + ret_bTy : core_base_type; + params : 'pexpr param list; + body : 'info where +} + +let pp_sym s = !^ (Pp_symbol.to_string_pretty s) + +let pp_where pp_info w = + let open Cerb_pp_prelude in + let pp_keyword w = pp_ansi_format [Bold; Magenta] (fun () -> !^ w) in + let pp_control w = pp_ansi_format [Bold; Blue] (fun () -> !^ w) in + let pp_pexpr pe = Pp_core.All.pp_pexpr pe in + let pp_pat pat = Pp_core.All.pp_pattern pat in + let pp_bty bTy = Pp_core.Basic.pp_core_base_type bTy in + let rec pp w = + let info = pp_info w.info in + let some x = pp_ansi_format [Green] (fun () -> P.enclose P.space P.space (P.brackets x)) in + let info = Option.fold ~none:P.space ~some info in + match w.node with + | Base _ -> + !^ "..." + | If (pe, w1, w2) -> + pp_control "if" ^^ info ^^ pp_pexpr pe ^^^ pp_control "then" ^^ + P.nest 2 (P.break 1 ^^ pp w1) ^^ P.break 1 ^^ + pp_control "else" ^^ P.nest 2 (P.break 1 ^^ pp w2) + | Sseq (pat, w1, w2) -> + P.group begin + (pp_control "let" ^^ info ^^ pp_pat pat ^^^ P.equals) ^//^ + (pp w1 ^^^ pp_control "in") + end ^^ P.hardline ^^ pp w2 + | Case (pe, cases) -> + pp_control "case" ^^ info ^^ pp_pexpr pe ^^^ pp_control "of" ^^ + P.nest 2 ( + P.hardline ^^ + P.separate_map P.hardline (fun (pat, wc) -> + P.bar ^^^ pp_pat pat ^^^ P.equals ^^ P.rangle ^^ + P.nest 4 (P.hardline ^^ pp wc) + ) cases ^^ + P.hardline ^^ pp_keyword "end") + | Run (sym, pes) -> + pp_keyword "run" ^^ info ^^ pp_sym sym ^^ P.parens (comma_list pp_pexpr pes) + | Jump (sym, pes) -> + pp_keyword "jump" ^^ info ^^ pp_sym sym ^^ P.parens (comma_list pp_pexpr pes) + | Save ld -> + pp_keyword "save" ^^ info ^^ pp_sym ld.label ^^ P.colon ^^^ pp_bty ld.ret_bTy ^^^ + P.parens (comma_list (fun p -> + pp_sym p.name ^^ P.colon ^^^ pp_bty p.bTy ^^ + P.colon ^^ P.equals ^^^ !^ ".." + ) ld.params) ^^^ + pp_control "in" ^^^ + P.nest 2 (P.break 1 ^^ pp ld.body) + | Where (body, defs) -> + (* "where" keyword binds tightest to exprs *) + let needs_paren = + let { info = _; annot = _; node } = body in + let base = function + | Eif _ | Esseq _ | Ewseq _ | Esave _ | Elet _ -> + (* end with an expr *) + true + | Epure _ | Ememop _ | Eaction _ | Ecase _ | Eccall _ + | Eproc _ | Eunseq _ | Ebound _ | End _ | Erun _ | Epar _ + | Ewhere _ | Ejump _ | Ewait _ | Eannot _ | Eexcluded _ -> + (* end with a token *) + false in + match node with + | If _ | Sseq _ | Save _ -> + true + | Base expr -> base expr + | Case (_, _) | Run (_, _) | Jump (_, _) | Where (_, _) -> + false in + let pp_def kw ld = + kw ^^ info ^^ pp_sym ld.label ^^^ + P.parens (comma_list (fun p -> + pp_sym p.name ^^ P.colon ^^^ pp_bty p.bTy + ) ld.params) ^^^ + P.colon ^^^ pp_bty ld.ret_bTy ^^^ + P.colon ^^ P.equals ^^ + P.nest 2 (P.break 1 ^^ pp ld.body) + in + begin match defs with + | [] -> assert false + | first :: rest -> + (if needs_paren then P.parens else Fun.id) (pp body) ^^ + P.nest 2 ( + P.hardline ^^ pp_def (pp_control "where") first ^^ + P.concat (List.map (fun d -> + P.hardline ^^ pp_def (pp_keyword "and") d + ) rest) + ^^ P.hardline ^^ pp_keyword "end") + end + in + pp w + +type count_labels = (Symbol.sym, int) Pmap.map + +let pp_int x = !^ (string_of_int x) + +let pp_count_map map = + if Pmap.is_empty map then + None + else + let pp_bind (sym, count) = pp_sym sym ^^ P.colon ^^ pp_int count in + Some (P.separate_map (P.comma ^^ P.space) pp_bind @@ Pmap.bindings_list map) + +let add_counts sym int_opt1 int_opt2 = + match int_opt1, int_opt2 with + | None, None -> assert false + | Some _, None + | None, Some _ -> Some 1 + | Some _, Some _ -> Some 2 + +let merge_counts count1 count2 = Pmap.merge add_counts count1 count2 + +let empty_map = Pmap.empty Symbol.compare_sym + +let singleton_count sym = Pmap.add sym 1 empty_map + +let rec count_labels (Expr (annot, expr_) : expr) : count_labels where = + match expr_ with + | Eif (pe, e1, e2) -> + let w1 = count_labels e1 in + let w2 = count_labels e2 in + { info = merge_counts w1.info w2.info; annot; node = If (pe, w1, w2) } + | Esseq (pat, e1, e2) -> + let w1 = count_labels e1 in + let w2 = count_labels e2 in + { info = merge_counts w1.info w2.info; annot; node = Sseq (pat, w1, w2) } + | Ecase (pe, cases) -> + let wcases = List.map (fun (pat, e) -> (pat, count_labels e)) cases in + let info = List.fold_left + (fun acc (_, w) -> merge_counts acc w.info) + empty_map wcases in + { info; annot; node = Case (pe, wcases) } + | Erun ((), sym, pes) -> + { info = singleton_count sym; annot; node = Run (sym, pes) } + | Esave ((sym, ret_bTy), params_list, body) -> + let wbody = count_labels body in + let params = List.map (fun (name, ((bTy, optCTy), pe)) -> + { name; bTy; optCTy; pexpr = pe } + ) params_list in + { info = merge_counts wbody.info (singleton_count sym); + annot; + node = Save { label = sym; ret_bTy; params; body = wbody } } + | Ejump _ -> assert false + | Ewhere _ -> assert false + | _ -> + { info = empty_map; annot; node = Base expr_ } + +(* We could skip this and just use plain [Symbol.sym Pset.set], + but this will allow us to tidy up unused, auto-generated nodes. *) +type usage = Used | Unused +type dominates = (Symbol.sym, usage) Pmap.map + +let pp_dom_map map = + if Pmap.is_empty map then + None + else + let pp_bind (sym, used) = + (match used with + | Used -> P.empty + | Unused -> P.bang) + ^^ pp_sym sym in + Some (P.separate_map (P.comma ^^ P.space) pp_bind @@ Pmap.bindings_list map) + +let union_dom sym int_opt1 int_opt2 = + match int_opt1, int_opt2 with + | None, None -> assert false + | Some _, Some _ -> + (* A label is dominated exactly once, so this case is impossible *) + assert false + | Some x, None + | None, Some x -> + Some x + +let union_dom = Pmap.merge union_dom + +let singleton_dom sym used = Pmap.add sym used empty_map + +let rec dominates dominated ({ info; annot; node } : count_labels where) : dominates where = + let ones, manys = + info + |> Pmap.filter (fun sym _ -> not (Pmap.mem sym dominated)) + |> Pmap.partition (fun _ count -> count = 1) in + let info = Pmap.map (fun _ -> Used) manys in + let dominated = union_dom dominated info in + let wrap node = { info; annot; node } in + match node with + | If (pexpr, true_, false_) -> + let true_ = dominates dominated true_ in + let false_ = dominates dominated false_ in + wrap (If (pexpr, true_, false_)) + | Sseq (pat, e1, e2) -> + let e1 = dominates dominated e1 in + let e2 = dominates dominated e2 in + wrap (Sseq (pat, e1, e2)) + | Case (pexpr, branches) -> + let dom_snd (pat, e) = (pat, dominates dominated e) in + wrap (Case (pexpr, List.map dom_snd branches)) + | Run (label, pexprs) -> + assert (Pmap.is_empty info); + wrap (Run (label, pexprs)) + | Save { label; ret_bTy; params; body } -> + let info = + if not (Pmap.mem label dominated) then + (* At this point we know: + 1. Label was not used outside of the save + (shadowed [dominated] value). + 2. Label was not used inside the save + (otherwise it would have been in [manys]). + Hence, the label is [Unused] (in [ones]). *) + (assert (Pmap.mem label ones); + Pmap.add label Unused info) + else + info in + let body = dominates dominated body in + let node = Save { label; ret_bTy; params; body } in + { info; annot; node } + | Base expr -> + assert (Pmap.is_empty info); + wrap (Base expr) + | Jump (_, _) -> assert false + | Where _ -> assert false + +module Helper = struct + let pat ?sym bTy = Pattern ([], CaseBase (sym, bTy)) + + let epure pe = Expr ([], Epure pe) + + let pe_sym sym = Pexpr ([], (), PEsym sym) + + let pe_val v = Pexpr ([], (), PEval v) + + let wrap_sseq1 bTy expr = + Expr ([], Esseq (pat bTy, expr, epure (pe_val Vunit))) + + let wrap_sseq2 _bty expr = + Expr ([], Esseq (pat BTy_unit, epure (pe_val Vunit), expr)) + + let wrap_if1 bTy expr = + Expr ([], Eif (pe_val Vtrue, wrap_sseq1 bTy expr, Expr ([], Epure (Pexpr ([], (), PEval Vunit))))) + + let wrap_if2 bTy expr = + Expr ([], Eif (pe_val Vfalse, epure (pe_val Vunit), wrap_sseq1 bTy expr)) +end + +let bTy_of_pat pat = + let inferred = Core_typing.infer_pattern pat in + let to_cbt (_, inferred, _) = Core_typing_aux.toCoreBaseType inferred in + match Exception.except_fmap to_cbt inferred with + | Exception.Result (Some bty) -> bty + | _ -> assert false (* elaboration guarantee *) + +(* The function can be thought of first transforming saves as follows: + + save l (x := pe) in E ~> jump l(pe) where l(x) := E end + + and then bubbling this outward, capturing (moving inside a label definition) + the continuation (layers of enclosing let strong pat = _ in E) of that + expression until it reaches the dominating context of l. + + In reality, labels may overlap this happens when we goto _inside_ C blocks, + so more than one label may be "live" (capturing) at the same time. + + To handle this we need to keep track of not just the labels definitions, but + also the "live" labels being captured. Loops and gotos which only jump out + of scopes will only capture the continuation of exactly one label at a time + (and would not need to track "live" labels). + + The implementation is essentially a rewrite rule of the form: + + E ~> (E', None) or E ~> (E' where defs, live) + + For the latter, case, when we reach a node with non-empty dominators, we + transform it as so: + + dominators(E) = labels + (E' where defs, live) ~> (E' where defs, live \ labels). + + If the set of live labels being captured is empty, we stop capturing and place + a where-expression at that point: + + (E' where defs, {}) ~> (E' where defs, None). + + Note that by convention, the first def in defs is will always be the one + capturing the continuation. In E where (def :: defs), E can be thought of as + an "entry block" and def as the "exit" block. There is always exactly one + because we synthesise join-point labels for any capturing if-expressions. + + NOTE: the analysis doesn't take into account free and bound variables when + moving expressions around, but this doesn't seem to matter much because the + "free" variables in saves are re-used for function local variables (across + different lifetimes). They are introduced upfront, before any runs/saves + (and so are always part of the dominator frame, I think). *) +let rec to_where bTy ({ info; annot; node } : dominates where) = + let dominators = Pmap.domain info in + let empty_set = Pset.empty Symbol.compare_sym in + let singleton sym = Pset.singleton Symbol.compare_sym sym in + let labels_info defs = + List.map (fun def -> (def.label, def.body.info)) defs + |> List.fold_left (fun (defs, bodies) (label, used) -> (Pset.add label defs, Pset.union bodies used)) (empty_set, empty_set) in + let new_ info node = { info; annot = []; node } in + let wrap info node = { info; annot; node} in + let unwrap_set_defs capturing = + let default = (Pset.empty Symbol.symbol_compare, []) in + Option.value ~default capturing in + let map_e_or_fst_def f e capturing = + let (live, defs) = unwrap_set_defs capturing in + match defs with + | [] -> (f e, live, defs) + | def :: defs -> (e, live, { def with body = f def.body } :: defs) in + begin match node with + | If (pexpr, true_, false_) -> + let (true_, capturing_t) = to_where bTy true_ in + let (false_, capturing_f) = to_where bTy false_ in + begin match capturing_t, capturing_f with + | None, None -> + let info = Pset.union true_.info false_.info in + (wrap info (If (pexpr, true_, false_)), None) + | _, _ -> + (* Approximately (not to be taken too literally) here is what's + happening: + + E1 ~> E1' where t(xt) := Et and defs1 end + E2 ~> E2' where f(xt) := Ef and defs2 end + --------------------------------------- + if pe1 then E1 else E2 ~> + if pe1 then E1' else E2' + where join(x) := pure(x) + and t(xt) := let strong yt = Et in jump join(yt) + and defs1 + and f(xf) := lef sfrong yf = Ef in jump join(yf) + and defs2 end + + Note that join is first, so that any continuations captured will + thus be place inside its body. *) + let label = Symbol.fresh_pretty "join" in + let sseq_jump body = + let sym = Symbol.fresh () in + let pat = Helper.pat ~sym bTy in + let jump = new_ (singleton label) (Jump (label, [Helper.pe_sym sym])) in + new_ (Pset.add label body.info) (Sseq (pat, body, jump)) in + let (true_j, live_t, defs_t) = + map_e_or_fst_def sseq_jump true_ capturing_t in + let (false_j, live_f, defs_f) = + map_e_or_fst_def sseq_jump false_ capturing_f in + let def = + let param = { + name = Symbol.fresh (); + bTy; + optCTy = None; + pexpr = (); + } in { + label; + ret_bTy = bTy; + params = [ param ]; + body = new_ empty_set (Base (Epure (Helper.pe_sym param.name))); + } in + let live = + let unioned = Pset.union live_t live_f in + assert (Pset.subset dominators unioned); + Pset.diff unioned dominators in + let defs = defs_t @ defs_f in + if Pset.is_empty live then + (* We don't add the join-point def here because we're not capturing + any more continuations. *) + let (labels, used) = labels_info defs in + let if_info = Pset.union true_.info false_.info in + let where_info = Pset.diff (Pset.union used if_info) labels in + (new_ where_info (Where (wrap if_info (If (pexpr, true_, false_)), defs)), None) + else + let info = Pset.union true_j.info false_j.info in + (wrap info (If (pexpr, true_j, false_j)), Some (live, def :: defs)) + end + | Sseq (pat, e1, e2) -> + let inner_bTy = bTy_of_pat pat in + let (e2, capturing2) = to_where bTy e2 in + let (e1, capturing1) = to_where inner_bTy e1 in + begin match capturing1, capturing2 with + | None, None -> + (wrap (Pset.union e1.info e2.info) (Sseq (pat, e1, e2)), None) + | _, _ -> + (* Approximately (not to be taken too literally) here is what's + happening: + + E1 ~> E1' where def1(x) := E and defs1 end + E2 ~> E2' where defs2 end + --------------------------------------- + let strong pat = E1 in E2 ~> + E1' where defs2 + and def1(x) := let strong pat = E in E2' + and defs1 end + + Note that defs2 is first, so that any continuations captured will + be place inside the head of its body. *) + let sseq_e2 body = wrap (Pset.union body.info e2.info) (Sseq (pat, body, e2)) in + let (e, live1, defs1) = map_e_or_fst_def sseq_e2 e1 capturing1 in + let (live2, defs2) = unwrap_set_defs capturing2 in + let live = + let unioned = Pset.union live1 live2 in + assert (Pset.subset dominators unioned); + Pset.diff unioned dominators in + let defs = defs2 @ defs1 in + let (labels, used) = labels_info defs in + if Pset.is_empty live then + let info = Pset.diff (Pset.union used e.info) labels in + (wrap info (Where (e, defs)), None) + else + (e, Some (live, defs)) + end + | Case (pexpr, branches) -> + let do_branch (pat, body) = + let (body, capturing) = to_where bTy body in + (* Case expressions can have runs inside them, but not saves, + so they'll never capture any continuations *) + assert (Option.is_none capturing); + (pat, body) in + let branches = List.map do_branch branches in + let info = List.fold_left (fun acc (_, body) -> Pset.union acc body.info) empty_set branches in + (wrap info (Case (pexpr, branches)), None) + | Run (label, pexprs) -> + (wrap (singleton label) (Jump (label, pexprs)), None) + | Save { label; ret_bTy; params; body } -> + let (body, capturing) = to_where ret_bTy body in + begin match Pmap.lookup label info with + | Some Unused -> + (* This is basically + + ---------------------------------------------- + save unused (x := pe) in E ~> let x = pe in E *) + let pat, expr = + let tuple { name; bTy; optCTy; pexpr } = ((name, bTy), pexpr) in + let syms, pexprs = List.split @@ List.map tuple params in + let mk_pat (sym, bTy) = Helper.pat ~sym bTy in + let pat = Pattern ([], CaseCtor (Ctuple, List.map mk_pat syms)) in + (pat, Epure (Pexpr ([], (), PEctor (Ctuple, pexprs)))) in + (wrap body.info (Sseq (pat, new_ empty_set (Base expr), body)), capturing) + | Some Used | None -> + (* Approximately (not to be taken too literally) here is + what's happening: + + E ~> E' where defs + ------------------------------------------------- + save l (x := pe) in E ~> + jump l(pe) where defs and l(x) := E' end *) + let pexprs = List.map (fun x -> x.pexpr) params in + let params = List.map (param_map (fun _ -> ())) params in + let jump = new_ (singleton label) (Jump (label, pexprs)) in + let def = { + label; + ret_bTy = bTy; + params; + body; + } in + let (live, defs) = unwrap_set_defs capturing in + let live = + let added = Pset.add label live in + assert (Pset.subset dominators added); + Pset.diff added dominators in + let defs = defs @ [ def ] in + let (labels, used) = labels_info defs in + if Pset.is_empty live then + let info = Pset.diff (Pset.union used body.info) labels in + (wrap info (Where (jump, defs)), None) + else + (jump, Some (live, defs)) + end + | Base expr -> + (wrap empty_set (Base expr), None) + | Jump (_, _) -> assert false + | Where _ -> assert false + end + +let to_where bTy dominated = + let (whered, capturing) = to_where bTy dominated in + match capturing with + | None -> whered + | Some _ -> assert false + +let pp_sym_set set = + if Pset.is_empty set then + None + else + Some (P.separate_map (P.comma ^^ P.space) pp_sym (Pset.elements set)) + +let apply_ctx e ctxs = + List.fold_right (fun (annot, pat, e2) e1 -> + let info = Pset.union e1.info e2.info in + { info; annot; node = Sseq (pat, e1, e2) }) ctxs e + +(* Works mostly, but needs to track free-variables to work fully. *) +let rec tighten_exit set bTy ({ info; annot; node } as expr) = + let no_uses info = Pset.is_empty (Pset.inter info set) in + let wrap node = { info; annot; node } in + match node with + | Case _ | Jump _ | Base _ -> + (expr, bTy, []) + | If (pe, e1, e2) -> + let (e1', _, e1'_ctx) = tighten_exit set bTy e1 in + let (e2', _, e2'_ctx) = tighten_exit set bTy e2 in + (wrap (If (pe, apply_ctx e1' e1'_ctx, apply_ctx e2' e2'_ctx)), bTy, []) + | Sseq (pat, e1, e2) -> + let (e1', bTy1', e1'_ctx) = tighten_exit set (bTy_of_pat pat) e1 in + if no_uses e2.info then + (e1', bTy1', (annot, pat, e2) :: e1'_ctx) + else + let (e2', bTy2', e2'_ctx) = tighten_exit set bTy e2 in + begin match pat with + | Pattern (_, CaseBase (None, _)) -> + (wrap (Sseq (pat, apply_ctx e1' e1'_ctx, e2')), bTy2', e2'_ctx) + | _ -> + (wrap (Sseq (pat, apply_ctx e1' e1'_ctx, apply_ctx e2' e2'_ctx)), bTy, []) + end + | Where (body, defs) -> + let set = + List.map (fun def -> def.label) defs + |> Pset.from_list Symbol.compare_sym in + let (exit, rest) = List.hd defs, List.tl defs in + let (body', _, body'_ctx) = tighten_exit set bTy body in + let rest' = List.map (fun def -> + let (def_body', _, def_body'_ctx) = tighten_exit set def.ret_bTy def.body in + { def with body = apply_ctx def_body' def_body'_ctx }) rest in + let (exit', exit_bTy, exit_ctx) = + let (exit_body', bTy_body', exit_body'_ctx) = tighten_exit set exit.ret_bTy exit.body in + ({ exit with body = exit_body' ; ret_bTy = bTy_body' }, bTy_body', exit_body'_ctx) in + let where = wrap (Where (apply_ctx body' body'_ctx, exit' :: rest')) in + (apply_ctx where exit_ctx, exit_bTy, []) + | Run _ | Save _ -> assert false + +let rec to_expr { info; annot; node } = + let wrap expr = Expr (annot, expr) in + wrap @@ + begin match node with + | If (pexpr, true_, false_) -> + Eif (pexpr, to_expr true_, to_expr false_) + | Sseq ((Pattern ([], CaseCtor (Ctuple, pats)) as pat), + { info; annot = []; + node = Base (Epure (Pexpr ([], (), PEctor (Ctuple, pexprs)) as pexpr)) }, + e2) -> + (* Tidy up the unused label case *) + let pat, pexpr = + match pats, pexprs with + | [ pat ], [ pexpr ] -> (pat, pexpr) + | _ -> (pat, pexpr) in + Elet (pat, pexpr, to_expr e2) + | Sseq (pat, e1, e2) -> + Esseq (pat, to_expr e1, to_expr e2) + | Case (pexpr, branches) -> + Ecase (pexpr, List.map (fun (pat, e) -> (pat, to_expr e)) branches) + | Base expr -> + expr + | Jump (label, pexprs) -> + Ejump ((), label, pexprs) + | Where (e, defs) -> + let def { label; ret_bTy; params; body } = + let param { name; bTy; optCTy; pexpr = () } = + (name, (bTy, optCTy)) in + ((label, ret_bTy), List.map param params, to_expr body) in + Ewhere (to_expr e, List.map def defs) + | Run _ + | Save _ -> + assert false + end + +let tighten_exit bTy e = + let info = Pset.empty Symbol.compare_sym in + let (tightened, _, ctx) = tighten_exit info bTy e in + apply_ctx tightened ctx + +let transform_expr bTy expr = + let counted = count_labels expr in + let () = Cerb_debug.print_debug 1 [] + (fun () -> "\n" ^ Pp_utils.to_plain_pretty_string + (pp_where pp_count_map counted)) in + let dominated = dominates empty_map counted in + let () = Cerb_debug.print_debug 1 [] + (fun () -> "\n" ^ Pp_utils.to_plain_pretty_string + (pp_where pp_dom_map dominated)) in + let whered = to_where bTy dominated in + let () = Cerb_debug.print_debug 1 [] + (fun () -> "\n" ^ Pp_utils.to_plain_pretty_string + (pp_where pp_sym_set whered)) in + let tightened = tighten_exit bTy whered in + let () = Cerb_debug.print_debug 1 [] + (fun () -> "\n" ^ Pp_utils.to_plain_pretty_string + (pp_where pp_sym_set tightened)) in + to_expr whered + +let transform_file file = + let rewrite_fun_map_decl = function + | Proc (loc, mrk, bTy, args, e) -> Proc (loc, mrk, bTy, args, transform_expr bTy e) + | decl -> decl in + { file with funs = Pmap.map rewrite_fun_map_decl file.funs } diff --git a/ocaml_frontend/switches.ml b/ocaml_frontend/switches.ml index b5fb99bbff..a2827b8c9c 100644 --- a/ocaml_frontend/switches.ml +++ b/ocaml_frontend/switches.ml @@ -43,6 +43,9 @@ type cerb_switch = (* eliminate pure expr rebindings: let pat = C[pure(pexpr)] -> substitute pexpr *) | SW_copy_prop + (* transform procedures from Esave/Erun style to Ewhere/Ejump style *) + | SW_save_to_where + let internal_ref = ref [] @@ -99,6 +102,8 @@ let set strs = Some (SW_magic_comment_char_dollar) | "copy_prop" -> Some SW_copy_prop + | "save_to_where" -> + Some SW_save_to_where | _ -> None in let pred x = function @@ -128,7 +133,8 @@ let set strs = | SW_zero_initialised | SW_at_magic_comments | SW_magic_comment_char_dollar - | SW_copy_prop as y -> + | SW_copy_prop + | SW_save_to_where as y -> x = y in List.iter (fun str -> match read_switch str with diff --git a/ocaml_frontend/switches.mli b/ocaml_frontend/switches.mli index bba98f841a..9e2fa95fbe 100644 --- a/ocaml_frontend/switches.mli +++ b/ocaml_frontend/switches.mli @@ -43,6 +43,9 @@ type cerb_switch = (* eliminate pure symbol rebindings: let alias = pure(sym) → substitute sym *) | SW_copy_prop + (* transform procedures from Esave/Erun style to Ewhere/Ejump style *) + | SW_save_to_where + val get_switches: unit -> cerb_switch list val has_switch: cerb_switch -> bool val has_switch_pred: (cerb_switch -> bool) -> cerb_switch option diff --git a/parsers/core/core_lexer.mll b/parsers/core/core_lexer.mll index 859542a544..0796f040d2 100644 --- a/parsers/core/core_lexer.mll +++ b/parsers/core/core_lexer.mll @@ -102,6 +102,9 @@ let keywords = ("strong", T.STRONG ); ("save", T.SAVE ); ("run", T.RUN ); + ("jump", T.JUMP ); + ("where", T.WHERE ); + ("and", T.AND ); ("bound", T.BOUND ); ("nd", T.ND ); ("par", T.PAR ); diff --git a/parsers/core/core_parser.mly b/parsers/core/core_parser.mly index 7b70f530fe..3c2ed880bd 100644 --- a/parsers/core/core_parser.mly +++ b/parsers/core/core_parser.mly @@ -734,6 +734,40 @@ let rec symbolify_expr ((Expr (annot, expr_)) : parsed_expr) : (unit expr) Eff.t Eff.mapM symbolify_pexpr _pes >>= fun pes -> Eff.return (Erun ((), sym, pes)) end + | Ejump ((), _sym, _pes) -> + (* Labels from Ewhere are in sym_scopes (not st.labels), so use + lookup_sym rather than lookup_label. *) + lookup_sym _sym >>= begin function + | None -> + Eff.fail (Cerb_location.(region (snd _sym) NoCursor)) (Core_parser_unresolved_symbol (fst _sym)) + | Some (sym, _) -> + Eff.mapM symbolify_pexpr _pes >>= fun pes -> + Eff.return (Ejump ((), sym, pes)) + end + | Ewhere (_e, _defs) -> + (* Open a scope for all where-labels so they are mutually visible + within the block (including from e) but out of scope outside. *) + under_scope begin + (* Pass 1: register all label syms before processing any body, + so forward and mutual references resolve correctly. *) + Eff.mapM (fun ((_sym, bTy), _xs, _body) -> + register_sym _sym >>= fun sym -> + Eff.return ((sym, bTy), _xs, _body) + ) _defs >>= fun _defs' -> + (* Pass 2: process each body under its own scope for params. *) + Eff.mapM (fun ((sym, bTy), _xs, _body) -> + under_scope begin + Eff.mapM (fun (_psym, bTy_mct) -> + register_sym _psym >>= fun psym -> + Eff.return (psym, bTy_mct) + ) _xs >>= fun xs -> + symbolify_expr _body >>= fun body -> + Eff.return ((sym, bTy), xs, body) + end + ) _defs' >>= fun defs -> + symbolify_expr _e >>= fun e -> + Eff.return (Ewhere (e, defs)) + end | Epar _es -> Eff.mapM symbolify_expr _es >>= fun es -> Eff.return (Epar es) @@ -839,9 +873,14 @@ let rec register_labels ((Expr (_, expr_)) : parsed_expr) : unit Eff.t = | Eccall _ | Eproc _ | Erun _ + | Ejump _ | Ewait _ -> Eff.return () + | Ewhere (_e, _defs) -> + (* TODO: save/run and jump/where should not occur in the same program *) + Eff.mapM_ (fun (_, _, _body) -> register_labels _body) _defs >>= fun () -> + register_labels _e | Ecase (_, _pat_es) -> Eff.mapM_ (fun (_, _e) -> register_labels _e @@ -1132,6 +1171,7 @@ let mk_file decls = (* SEMICOLON has higher priority than IN *) %nonassoc IN %right SEMICOLON +%nonassoc WHERE @@ -1153,7 +1193,7 @@ let mk_file decls = %token CREATE CREATE_READONLY ALLOC STORE STORE_LOCK LOAD SEQ_RMW SEQ_RMW_WITH_FORWARD KILL FREE RMW FENCE (* COMPARE_EXCHANGE_STRONG *) (* continuation operators *) -%token SAVE RUN +%token SAVE RUN JUMP WHERE AND (* binder patterns *) %token UNDERSCORE @@ -1693,6 +1733,12 @@ expr: | RUN _sym= SYM _pes= delimited(LPAREN, separated_list(COMMA, pexpr), RPAREN) { Expr ( [Aloc (region ($startpos, $endpos) NoCursor)] , Erun ((), _sym, _pes) ) } +| JUMP _sym= SYM _pes= delimited(LPAREN, separated_list(COMMA, pexpr), RPAREN) + { Expr ( [Aloc (region ($startpos, $endpos) NoCursor)] + , Ejump ((), _sym, _pes) ) } +| _e= expr WHERE _defs= separated_nonempty_list(AND, where_def) END + { Expr ( [Aloc (region ($startpos, $endpos) NoCursor)] + , Ewhere (_e, _defs) ) } | ND _es= delimited(LPAREN, separated_list(COMMA, expr), RPAREN) { Expr ( [Aloc (region ($startpos, $endpos) NoCursor)] , End _es ) } @@ -1701,6 +1747,18 @@ expr: , Epar _es ) } ; +where_param: +| _sym= SYM COLON _bTy= core_base_type + { (_sym, (_bTy, None)) } +; + +where_def: +| _sym= SYM + _xs= delimited(LPAREN, separated_list(COMMA, where_param), RPAREN) + COLON _bTy= core_base_type COLON_EQ _body= expr + { ((_sym, _bTy), _xs, _body) } +; + action: | CREATE LPAREN _pe1= pexpr COMMA _pe2= pexpr RPAREN { Create (_pe1, _pe2, Symbol.PrefOther "Core") } diff --git a/parsers/core/core_parser_util.ml b/parsers/core/core_parser_util.ml index 6521941183..dc5f085529 100644 --- a/parsers/core/core_parser_util.ml +++ b/parsers/core/core_parser_util.ml @@ -89,6 +89,9 @@ type token = | STRONG | SAVE (* TODO *) | RUN (* TODO *) + | JUMP + | WHERE + | AND (* | TRY | WITH diff --git a/tests/diff-prog.py b/tests/diff-prog.py index d326f2b089..15f233202c 100755 --- a/tests/diff-prog.py +++ b/tests/diff-prog.py @@ -1,6 +1,6 @@ #!/usr/bin/env python3 -import os, sys, re, subprocess, json, difflib, argparse, concurrent.futures, math, multiprocessing +import os, sys, re, subprocess, json, difflib, argparse, concurrent.futures, math, multiprocessing, time def eprint(*args, then_exit=True, **kwargs): print('Error:', *args, file=sys.stderr, **kwargs) @@ -21,7 +21,7 @@ def __init__(self, opts, config): self.name = config['name'] def run(self, test_rel_path): - cmd = time_cmd([self.prog] + self.args + [test_rel_path]) + cmd = [self.prog] + self.args + [test_rel_path] if self.print_cmd: print(' '.join(cmd)) if self.run_cmd: @@ -31,10 +31,11 @@ def run(self, test_rel_path): def output(self, test_rel_path): try: + start_time = time.monotonic() completed = self.run(test_rel_path); + elapsed_time = time.monotonic() - start_time lines = completed.stdout.splitlines(True) - time = float(lines[-3].split()[1]) - return { 'time': time, 'lines' : [("return code: %d\n" % completed.returncode)] + lines[:-3] } + return { 'time': elapsed_time, 'lines' : [("return code: %d\n" % completed.returncode)] + lines } except subprocess.TimeoutExpired: return { 'time': float(self.timeout), 'lines': ["TIMEOUT\n"] } diff --git a/tests/run-save-to-where.sh b/tests/run-save-to-where.sh new file mode 100755 index 0000000000..5db19ff979 --- /dev/null +++ b/tests/run-save-to-where.sh @@ -0,0 +1,103 @@ +#!/bin/bash +# Verifies that --switches save_to_where does not change output of existing CI tests + +TESTSDIR=$(cd "$(dirname "${BASH_SOURCE[0]}")" &>/dev/null && pwd) +cd "$TESTSDIR" + +source ./tests.sh # citests, skip +source ./common.sh # set_cerberus_exec + +mkdir -p tmp + +pass=0 +fail=0 + +function doSkip { + for f in "${skip[@]}"; do [[ $f == $1 ]] && return 0; done + return 1 +} + +# report +function report { + local label=$1 + local file=$2 + local ret=$3 + local res=$ret + + if [[ $file == *.error.c || $file == *.undef.c ]]; then + res=$((1 - ret)) + fi + + if [[ $file == *.unsup.c ]]; then + cat tmp/result tmp/stderr | grep -q "feature not yet supported" + res=$? + fi + + if [[ "$((res))" -eq "0" ]]; then + res="\033[1m\033[32mPASSED!\033[0m" + pass=$((pass+1)) + else + res="\033[1m\033[31mFAILED!\033[0m" + fail=$((fail+1)) + cat tmp/result tmp/stderr + fi + + echo -e "Test $label: $res" +} + +if [[ $# == 1 ]]; then + citests=("$(basename "$1")") +fi + +set_cerberus_exec "cerberus" + +for file in "${citests[@]}"; do + if [[ ! -f ./ci/$file ]]; then + echo -e "Test $file: \033[1m\033[33mNOT FOUND\033[0m" + fail=$((fail+1)) + continue + fi + + if doSkip "$file"; then + echo -e "Test $file: \033[1m\033[33mSKIPPING\033[0m" + continue + fi + + if [[ $file == *.syntax-only.c ]]; then + $CERB --nolibc --typecheck-core --switches save_to_where ci/$file > tmp/result 2> tmp/stderr + else + $CERB --nolibc --typecheck-core --exec --batch --switches save_to_where ci/$file > tmp/result 2> tmp/stderr + fi + ret=$? + + if [[ -f ./ci/expected/$file.expected ]]; then + if [[ $file == *.error.c || $file == *.syntax-only.c ]]; then + if [ "$(uname)" == "Linux" ]; then + sed -i '$ d' tmp/stderr + else + sed -i '' -e '$ d' tmp/stderr + fi + if ! cmp --silent tmp/stderr ci/expected/$file.expected; then + ret=0 + fi + else + if ! cmp --silent tmp/result ci/expected/$file.expected; then + if [[ $file == *.undef.c ]]; then + ret=0 + else + ret=1 + fi + fi + fi + else + echo -e "Test $file: \033[1m\033[33mMISSING .expected FILE\033[0m" + continue + fi + + report "$file [+save_to_where]" "$file" "$ret" +done + +echo "" +echo "SAVE TO WHERE PASSED: $pass" +echo "SAVE TO WHERE FAILED: $fail" +[ $fail -eq 0 ] diff --git a/tests/where/0126-duff_device.c b/tests/where/0126-duff_device.c new file mode 100644 index 0000000000..8eddf37549 --- /dev/null +++ b/tests/where/0126-duff_device.c @@ -0,0 +1,25 @@ +#include + +void send(char *to, char *from, int count) +{ + int n = (count + 7) / 8; + switch (count % 8) { + case 0: do { *to++ = *from++; + case 7: *to++ = *from++; + case 6: *to++ = *from++; + case 5: *to++ = *from++; + case 4: *to++ = *from++; + case 3: *to++ = *from++; + case 2: *to++ = *from++; + case 1: *to++ = *from++; + } while (--n > 0); + } +} + +int main() +{ + char * from = "hello"; + char to[10]; + send(to, from, 6); + printf("%s\n", to); +} diff --git a/tests/where/0126-duff_device.c.debug b/tests/where/0126-duff_device.c.debug new file mode 100644 index 0000000000..14b4258b43 --- /dev/null +++ b/tests/where/0126-duff_device.c.debug @@ -0,0 +1,524 @@ +return code: 0 +let [ret_724:1, break_726:1, continue_727:1, break_728:1, case_752:1, case_753:1, case_754:1, case_755:1, case_756:1, case_757:1, case_758:1, case_759:1, do_761:1] _: unit = + let [break_726:1, continue_727:1, break_728:1, case_752:1, case_753:1, case_754:1, case_755:1, case_756:1, case_757:1, case_758:1, case_759:1, do_761:1] n: pointer = + ... in + let [break_726:1, continue_727:1, break_728:1, case_752:1, case_753:1, case_754:1, case_755:1, case_756:1, case_757:1, case_758:1, case_759:1, do_761:1] _: unit = + let a_729: loaded integer = ... in + ... in + let [break_726:1, continue_727:1, break_728:1, case_752:1, case_753:1, case_754:1, case_755:1, case_756:1, case_757:1, case_758:1, case_759:1, do_761:1] _: unit = + let [break_726:2, continue_727:1, break_728:1, case_752:1, case_753:1, case_754:1, case_755:1, case_756:1, case_757:1, case_758:1, case_759:1, do_761:1] _: unit = + let [break_726:1, continue_727:1, break_728:1, case_752:1, case_753:1, case_754:1, case_755:1, case_756:1, case_757:1, case_758:1, case_759:1, do_761:1] a_749: loaded integer = + ... in + case [break_726:1, continue_727:1, break_728:1, case_752:1, case_753:1, case_754:1, case_755:1, case_756:1, case_757:1, case_758:1, case_759:1, do_761:1] a_749 of + | Specified(a_750: integer) => + let [break_726:1, continue_727:1, break_728:1, case_752:1, case_753:1, case_754:1, case_755:1, case_756:1, case_757:1, case_758:1, case_759:1, do_761:1] a_751: integer = + ... in + let [break_726:1, continue_727:1, break_728:1, case_752:1, case_753:1, case_754:1, case_755:1, case_756:1, case_757:1, case_758:1, case_759:2, do_761:1] _: unit = + if [case_759:1] a_751 = 0 then + run [case_759:1] case_759(n) + else + ... in + let [break_726:1, continue_727:1, break_728:1, case_752:1, case_753:1, case_754:1, case_755:1, case_756:1, case_757:1, case_758:2, case_759:1, do_761:1] _: unit = + if [case_758:1] a_751 = 7 then + run [case_758:1] case_758(n) + else + ... in + let [break_726:1, continue_727:1, break_728:1, case_752:1, case_753:1, case_754:1, case_755:1, case_756:1, case_757:2, case_758:1, case_759:1, do_761:1] _: unit = + if [case_757:1] a_751 = 6 then + run [case_757:1] case_757(n) + else + ... in + let [break_726:1, continue_727:1, break_728:1, case_752:1, case_753:1, case_754:1, case_755:1, case_756:2, case_757:1, case_758:1, case_759:1, do_761:1] _: unit = + if [case_756:1] a_751 = 5 then + run [case_756:1] case_756(n) + else + ... in + let [break_726:1, continue_727:1, break_728:1, case_752:1, case_753:1, case_754:1, case_755:2, case_756:1, case_757:1, case_758:1, case_759:1, do_761:1] _: unit = + if [case_755:1] a_751 = 4 then + run [case_755:1] case_755(n) + else + ... in + let [break_726:1, continue_727:1, break_728:1, case_752:1, case_753:1, case_754:2, case_755:1, case_756:1, case_757:1, case_758:1, case_759:1, do_761:1] _: unit = + if [case_754:1] a_751 = 3 then + run [case_754:1] case_754(n) + else + ... in + let [break_726:1, continue_727:1, break_728:1, case_752:1, case_753:2, case_754:1, case_755:1, case_756:1, case_757:1, case_758:1, case_759:1, do_761:1] _: unit = + if [case_753:1] a_751 = 2 then + run [case_753:1] case_753(n) + else + ... in + let [break_726:1, continue_727:1, break_728:1, case_752:2, case_753:1, case_754:1, case_755:1, case_756:1, case_757:1, case_758:1, case_759:1, do_761:1] _: unit = + if [case_752:1] a_751 = 1 then + run [case_752:1] case_752(n) + else + ... in + let [break_726:1, continue_727:1, break_728:1, case_752:1, case_753:1, case_754:1, case_755:1, case_756:1, case_757:1, case_758:1, case_759:1, do_761:1] _: unit = + ... in + let [break_726:1, continue_727:1, break_728:1, case_752:1, case_753:1, case_754:1, case_755:1, case_756:1, case_757:1, case_758:1, case_759:1, do_761:1] _: unit = + run [break_726:1] break_726(n) in + let [continue_727:1, break_728:1, case_752:1, case_753:1, case_754:1, case_755:1, case_756:1, case_757:1, case_758:1, case_759:1, do_761:1] _: unit = + let [continue_727:1, break_728:1, case_752:1, case_753:1, case_754:1, case_755:1, case_756:1, case_757:1, case_758:1, case_759:1, do_761:1] _: unit = + save [continue_727:1, break_728:1, case_752:1, case_753:1, case_754:1, case_755:1, case_756:1, case_757:1, case_758:1, case_759:1, do_761:1] case_759: unit (n: pointer:= ..) in + let [continue_727:1, break_728:1, case_752:1, case_753:1, case_754:1, case_755:1, case_756:1, case_757:1, case_758:1, do_761:1] _: unit = + save [continue_727:1, case_752:1, case_753:1, case_754:1, case_755:1, case_756:1, case_757:1, case_758:1, do_761:2] do_761: unit (n: pointer:= ..) in + let [continue_727:1, case_752:1, case_753:1, case_754:1, case_755:1, case_756:1, case_757:1, case_758:1, do_761:1] _: unit = + let [continue_727:1, case_752:1, case_753:1, case_754:1, case_755:1, case_756:1, case_757:1, case_758:1] _: unit = + let [case_752:1, case_753:1, case_754:1, case_755:1, case_756:1, case_757:1, case_758:1] _: unit = + let _: loaded integer = ... in + ... in + let [case_752:1, case_753:1, case_754:1, case_755:1, case_756:1, case_757:1, case_758:1] _: unit = + save [case_758:1] case_758: unit (n: pointer:= ..) in + let _: loaded integer = ... in + ... in + let [case_752:1, case_753:1, case_754:1, case_755:1, case_756:1, case_757:1] _: unit = + save [case_757:1] case_757: unit (n: pointer:= ..) in + let _: loaded integer = ... in + ... in + let [case_752:1, case_753:1, case_754:1, case_755:1, case_756:1] _: unit = + save [case_756:1] case_756: unit (n: pointer:= ..) in + let _: loaded integer = ... in + ... in + let [case_752:1, case_753:1, case_754:1, case_755:1] _: unit = + save [case_755:1] case_755: unit (n: pointer:= ..) in + let _: loaded integer = ... in + ... in + let [case_752:1, case_753:1, case_754:1] _: unit = + save [case_754:1] case_754: unit (n: pointer:= ..) in + let _: loaded integer = ... in + ... in + let [case_752:1, case_753:1] _: unit = + save [case_753:1] case_753: unit (n: pointer:= ..) in + let _: loaded integer = ... in + ... in + let [case_752:1] _: unit = + save [case_752:1] case_752: unit (n: pointer:= ..) in + let _: loaded integer = ... in + ... in + ... in + let [continue_727:1] _: unit = save [continue_727:1] continue_727: unit (n: pointer:= ..) in ... in + ... in + let [do_761:1] a_763: loaded integer = ... in + case [do_761:1] a_763 of + | Specified(a_762: integer) => + if [do_761:1] not(a_762 = 0) then + run [do_761:1] do_761(n) + else + ... + | Unspecified(_: ctype) => + ... + end in + let [break_728:1] _: unit = save [break_728:1] break_728: unit (n: pointer:= ..) in ... in + ... in + ... in + ... + | Unspecified(_: ctype) => + ... + end in + let [break_726:1] _: unit = save [break_726:1] break_726: unit (n: pointer:= ..) in ... in + ... in + let _: unit = ... in + ... in +save [ret_724:1] ret_724: unit (a_897: unit:= ..) in + ... +let _: unit = + let n: pointer = ... in + let _: unit = + let a_729: loaded integer = ... in + ... in + let _: unit = + let [break_726] _: unit = + let a_749: loaded integer = ... in + case a_749 of + | Specified(a_750: integer) => + let a_751: integer = ... in + let [case_759] _: unit = if a_751 = 0 then run case_759(n) else ... in + let [case_758] _: unit = if a_751 = 7 then run case_758(n) else ... in + let [case_757] _: unit = if a_751 = 6 then run case_757(n) else ... in + let [case_756] _: unit = if a_751 = 5 then run case_756(n) else ... in + let [case_755] _: unit = if a_751 = 4 then run case_755(n) else ... in + let [case_754] _: unit = if a_751 = 3 then run case_754(n) else ... in + let [case_753] _: unit = if a_751 = 2 then run case_753(n) else ... in + let [case_752] _: unit = if a_751 = 1 then run case_752(n) else ... in + let _: unit = ... in + let _: unit = run break_726(n) in + let _: unit = + let _: unit = + save case_759: unit (n: pointer:= ..) in + let _: unit = + save [do_761] do_761: unit (n: pointer:= ..) in + let _: unit = + let _: unit = + let _: unit = + let _: loaded integer = ... in + ... in + let _: unit = + save case_758: unit (n: pointer:= ..) in + let _: loaded integer = ... in + ... in + let _: unit = + save case_757: unit (n: pointer:= ..) in + let _: loaded integer = ... in + ... in + let _: unit = + save case_756: unit (n: pointer:= ..) in + let _: loaded integer = ... in + ... in + let _: unit = + save case_755: unit (n: pointer:= ..) in + let _: loaded integer = ... in + ... in + let _: unit = + save case_754: unit (n: pointer:= ..) in + let _: loaded integer = ... in + ... in + let _: unit = + save case_753: unit (n: pointer:= ..) in + let _: loaded integer = ... in + ... in + let _: unit = + save case_752: unit (n: pointer:= ..) in + let _: loaded integer = ... in + ... in + ... in + let _: unit = save [!continue_727] continue_727: unit (n: pointer:= ..) in ... in + ... in + let a_763: loaded integer = ... in + case a_763 of + | Specified(a_762: integer) => + if not(a_762 = 0) then + run do_761(n) + else + ... + | Unspecified(_: ctype) => + ... + end in + let _: unit = save [!break_728] break_728: unit (n: pointer:= ..) in ... in + ... in + ... in + ... + | Unspecified(_: ctype) => + ... + end in + let _: unit = save break_726: unit (n: pointer:= ..) in ... in + ... in + let _: unit = ... in + ... in +save [!ret_724] ret_724: unit (a_897: unit:= ..) in + ... +let _: unit = + let n: pointer = ... in + let _: unit = + let a_729: loaded integer = ... in + ... in + let _: unit = + (let [break_726] _: unit = + let [break_726] a_749: loaded integer = ... in + case [break_726] a_749 of + | Specified(a_750: integer) => + let [break_726] a_751: integer = ... in + (let [break_726, case_752, case_753, case_754, case_755, case_756, case_757, case_758, case_759] _: unit = + if [case_759] a_751 = 0 then + jump [case_759] case_759(n) + else + ... in + let [break_726, case_752, case_753, case_754, case_755, case_756, case_757, case_758, case_759] _: unit = + if [case_758] a_751 = 7 then + jump [case_758] case_758(n) + else + ... in + let [break_726, case_752, case_753, case_754, case_755, case_756, case_757, case_759] _: unit = + if [case_757] a_751 = 6 then + jump [case_757] case_757(n) + else + ... in + let [break_726, case_752, case_753, case_754, case_755, case_756, case_759] _: unit = + if [case_756] a_751 = 5 then + jump [case_756] case_756(n) + else + ... in + let [break_726, case_752, case_753, case_754, case_755, case_759] _: unit = + if [case_755] a_751 = 4 then + jump [case_755] case_755(n) + else + ... in + let [break_726, case_752, case_753, case_754, case_759] _: unit = if [case_754] a_751 = 3 then jump [case_754] case_754(n) else ... in + let [break_726, case_752, case_753, case_759] _: unit = if [case_753] a_751 = 2 then jump [case_753] case_753(n) else ... in + let [break_726, case_752, case_759] _: unit = if [case_752] a_751 = 1 then jump [case_752] case_752(n) else ... in + let [break_726, case_759] _: unit = ... in + let [break_726, case_759] _: unit = jump [break_726] break_726(n) in + jump [case_759] case_759(n)) + where [break_726] case_752 (n: pointer) : unit := + let [do_761] _: unit = + let [do_761] _: unit = + let [do_761] _: unit = + let [do_761] _: unit = + let _: unit = + let _: unit = + let _: loaded integer = ... in + ... in + ... in + let _: unit = + let (n: pointer) = ... in + ... in + ... in + let [do_761] a_763: loaded integer = ... in + case [do_761] a_763 of + | Specified(a_762: integer) => + if [do_761] not(a_762 = 0) then + jump [do_761] do_761(n) + else + ... + | Unspecified(_: ctype) => + ... + end in + let _: unit = + let (n: pointer) = ... in + ... in + ... in + ... in + ... + and [break_726] case_753 (n: pointer) : unit := + let [case_752] _: unit = + let _: loaded integer = ... in + ... in + jump [case_752] case_752(n) + and [break_726] case_754 (n: pointer) : unit := + let [case_753] _: unit = + let _: loaded integer = ... in + ... in + jump [case_753] case_753(n) + and [break_726] case_755 (n: pointer) : unit := + let [case_754] _: unit = + let _: loaded integer = ... in + ... in + jump [case_754] case_754(n) + and [break_726] case_756 (n: pointer) : unit := + let [case_755] _: unit = + let _: loaded integer = ... in + ... in + jump [case_755] case_755(n) + and [break_726] case_757 (n: pointer) : unit := + let [case_756] _: unit = + let _: loaded integer = ... in + ... in + jump [case_756] case_756(n) + and [break_726] case_758 (n: pointer) : unit := + let [case_757] _: unit = + let _: loaded integer = ... in + ... in + jump [case_757] case_757(n) + and [break_726] do_761 (n: pointer) : unit := + let [case_758] _: unit = + let _: loaded integer = ... in + ... in + jump [case_758] case_758(n) + and [break_726] case_759 (n: pointer) : unit := + jump [do_761] do_761(n) + end + | Unspecified(_: ctype) => + ... + end in + jump [break_726] break_726(n)) + where break_726 (n: pointer) : unit := + let _: unit = ... in + ... + end in + let _: unit = ... in + ... in +let (a_897: unit) = ... in +... +let _: unit = + let n: pointer = ... in + let _: unit = + let a_729: loaded integer = ... in + ... in + let _: unit = + (let [break_726] _: unit = + let [break_726] a_749: loaded integer = ... in + case [break_726] a_749 of + | Specified(a_750: integer) => + let [break_726] a_751: integer = ... in + (let [break_726, case_752, case_753, case_754, case_755, case_756, case_757, case_758, case_759] _: unit = + if [case_759] a_751 = 0 then + jump [case_759] case_759(n) + else + ... in + let [break_726, case_752, case_753, case_754, case_755, case_756, case_757, case_758, case_759] _: unit = + if [case_758] a_751 = 7 then + jump [case_758] case_758(n) + else + ... in + let [break_726, case_752, case_753, case_754, case_755, case_756, case_757, case_759] _: unit = + if [case_757] a_751 = 6 then + jump [case_757] case_757(n) + else + ... in + let [break_726, case_752, case_753, case_754, case_755, case_756, case_759] _: unit = + if [case_756] a_751 = 5 then + jump [case_756] case_756(n) + else + ... in + let [break_726, case_752, case_753, case_754, case_755, case_759] _: unit = + if [case_755] a_751 = 4 then + jump [case_755] case_755(n) + else + ... in + let [break_726, case_752, case_753, case_754, case_759] _: unit = if [case_754] a_751 = 3 then jump [case_754] case_754(n) else ... in + let [break_726, case_752, case_753, case_759] _: unit = if [case_753] a_751 = 2 then jump [case_753] case_753(n) else ... in + let [break_726, case_752, case_759] _: unit = if [case_752] a_751 = 1 then jump [case_752] case_752(n) else ... in + let [break_726, case_759] _: unit = ... in + let [break_726, case_759] _: unit = jump [break_726] break_726(n) in + jump [case_759] case_759(n)) + where [break_726] case_752 (n: pointer) : unit := + let [do_761] _: unit = + let [do_761] _: unit = + let [do_761] _: unit = + let [do_761] _: unit = + let _: unit = + let _: unit = + let _: loaded integer = ... in + ... in + ... in + let _: unit = + let (n: pointer) = ... in + ... in + ... in + let [do_761] a_763: loaded integer = ... in + case [do_761] a_763 of + | Specified(a_762: integer) => + if [do_761] not(a_762 = 0) then + jump [do_761] do_761(n) + else + ... + | Unspecified(_: ctype) => + ... + end in + let _: unit = + let (n: pointer) = ... in + ... in + ... in + ... in + ... + and [break_726] case_753 (n: pointer) : unit := + let [case_752] _: unit = + let _: loaded integer = ... in + ... in + jump [case_752] case_752(n) + and [break_726] case_754 (n: pointer) : unit := + let [case_753] _: unit = + let _: loaded integer = ... in + ... in + jump [case_753] case_753(n) + and [break_726] case_755 (n: pointer) : unit := + let [case_754] _: unit = + let _: loaded integer = ... in + ... in + jump [case_754] case_754(n) + and [break_726] case_756 (n: pointer) : unit := + let [case_755] _: unit = + let _: loaded integer = ... in + ... in + jump [case_755] case_755(n) + and [break_726] case_757 (n: pointer) : unit := + let [case_756] _: unit = + let _: loaded integer = ... in + ... in + jump [case_756] case_756(n) + and [break_726] case_758 (n: pointer) : unit := + let [case_757] _: unit = + let _: loaded integer = ... in + ... in + jump [case_757] case_757(n) + and [break_726] do_761 (n: pointer) : unit := + let [case_758] _: unit = + let _: loaded integer = ... in + ... in + jump [case_758] case_758(n) + and [break_726] case_759 (n: pointer) : unit := + jump [do_761] do_761(n) + end + | Unspecified(_: ctype) => + ... + end in + jump [break_726] break_726(n)) + where break_726 (n: pointer) : unit := + let _: unit = ... in + ... + end in + let _: unit = ... in + ... in +let (a_897: unit) = ... in +... +let [ret_675:1] _: unit = + let from: pointer = ... in + let to: pointer = ... in + let _: unit = + let a_676: loaded pointer = ... in + ... in + let _: unit = ... in + let _: unit = + let _: unit = ... in + ... in + let _: unit = + let _: loaded integer = ... in + ... in + let _: unit = ... in + let _: unit = ... in + ... in +save [ret_675:1] ret_675: loaded integer (a_720: loaded integer:= ..) in + ... +let _: unit = + let from: pointer = ... in + let to: pointer = ... in + let _: unit = + let a_676: loaded pointer = ... in + ... in + let _: unit = ... in + let _: unit = + let _: unit = ... in + ... in + let _: unit = + let _: loaded integer = ... in + ... in + let _: unit = ... in + let _: unit = ... in + ... in +save [!ret_675] ret_675: loaded integer (a_720: loaded integer:= ..) in + ... +let _: unit = + let from: pointer = ... in + let to: pointer = ... in + let _: unit = + let a_676: loaded pointer = ... in + ... in + let _: unit = ... in + let _: unit = + let _: unit = ... in + ... in + let _: unit = + let _: loaded integer = ... in + ... in + let _: unit = ... in + let _: unit = ... in + ... in +let (a_720: loaded integer) = ... in +... +let _: unit = + let from: pointer = ... in + let to: pointer = ... in + let _: unit = + let a_676: loaded pointer = ... in + ... in + let _: unit = ... in + let _: unit = + let _: unit = ... in + ... in + let _: unit = + let _: loaded integer = ... in + ... in + let _: unit = ... in + let _: unit = ... in + ... in +let (a_720: loaded integer) = ... in +... diff --git a/tests/where/back_inside_loop.c b/tests/where/back_inside_loop.c new file mode 100644 index 0000000000..ed816a6cd1 --- /dev/null +++ b/tests/where/back_inside_loop.c @@ -0,0 +1,20 @@ +int main() { + int x = 3; + int y = 2; + + while (x > 0) { + x--; +l: + x; + } + + int z = 1; + + if (z < y) { + y = 0; + x = -1; + goto l; + } + + return 0; +} diff --git a/tests/where/back_inside_loop.c.debug b/tests/where/back_inside_loop.c.debug new file mode 100644 index 0000000000..786bea0156 --- /dev/null +++ b/tests/where/back_inside_loop.c.debug @@ -0,0 +1,324 @@ +return code: 0 +let [l:1, ret_512:2, continue_513:1, break_514:1, while_516:1] _: unit = + let [l:1, ret_512:1, continue_513:1, break_514:1, while_516:1] x: pointer = ... in + let [l:1, ret_512:1, continue_513:1, break_514:1, while_516:1] y: pointer = ... in + let [l:1, ret_512:1, continue_513:1, break_514:1, while_516:1] z: pointer = ... in + let [l:1, ret_512:1, continue_513:1, break_514:1, while_516:1] _: unit = + let a_518: loaded integer = ... in + ... in + let [l:1, ret_512:1, continue_513:1, break_514:1, while_516:1] _: unit = + let a_519: loaded integer = ... in + ... in + let [l:2, ret_512:1, continue_513:1, break_514:1, while_516:1] _: unit = + let [l:1, continue_513:1, break_514:1, while_516:1] _: unit = + save [l:1, continue_513:1, while_516:2] while_516: unit (x: pointer:= .., y: pointer:= .., z: pointer:= ..) in + let [l:1, continue_513:1, while_516:1] a_520: loaded integer = ... in + let [l:1, continue_513:1, while_516:1] a_517: boolean = + case a_520 of + | Specified(a_521: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [l:1, continue_513:1, while_516:1] a_517 then + let [l:1, continue_513:1, while_516:1] _: unit = + let [l:1, continue_513:1] _: unit = + let [l:1] _: unit = + let _: loaded integer = ... in + ... in + let [l:1] _: unit = + save [l:1] l: unit (x: pointer:= .., y: pointer:= .., z: pointer:= ..) in + let _: loaded integer = ... in + ... in + ... in + let [continue_513:1] _: unit = save [continue_513:1] continue_513: unit (x: pointer:= .., y: pointer:= .., z: pointer:= ..) in ... in + ... in + run [while_516:1] while_516(x, y, z) + else + ... in + let [break_514:1] _: unit = save [break_514:1] break_514: unit (x: pointer:= .., y: pointer:= .., z: pointer:= ..) in ... in + ... in + let [l:1, ret_512:1] _: unit = + let a_537: loaded integer = ... in + ... in + let [l:1, ret_512:1] _: unit = + let [l:1] a_538: loaded integer = ... in + let [l:1] a_515: boolean = + case a_538 of + | Specified(a_539: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [l:1] a_515 then + let [l:1] _: unit = + let _: loaded integer = ... in + ... in + let [l:1] _: unit = + let _: loaded integer = ... in + ... in + let [l:1] _: unit = run [l:1] l(x, y, z) in + ... + else + ... in + let [ret_512:1] _: unit = + let [ret_512:1] a_558: loaded integer = ... in + let [ret_512:1] _: unit = ... in + let [ret_512:1] _: unit = ... in + let [ret_512:1] _: unit = ... in + run [ret_512:1] ret_512(conv_loaded_int('signed int', a_558)) in + let _: unit = ... in + let _: unit = ... in + let _: unit = ... in + ... in +save [ret_512:1] ret_512: loaded integer (a_559: loaded integer:= ..) in + ... +let [ret_512] _: unit = + let x: pointer = ... in + let y: pointer = ... in + let z: pointer = ... in + let _: unit = + let a_518: loaded integer = ... in + ... in + let _: unit = + let a_519: loaded integer = ... in + ... in + let [l] _: unit = + let _: unit = + save [while_516] while_516: unit (x: pointer:= .., y: pointer:= .., z: pointer:= ..) in + let a_520: loaded integer = ... in + let a_517: boolean = + case a_520 of + | Specified(a_521: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if a_517 then + let _: unit = + let _: unit = + let _: unit = + let _: loaded integer = ... in + ... in + let _: unit = + save l: unit (x: pointer:= .., y: pointer:= .., z: pointer:= ..) in + let _: loaded integer = ... in + ... in + ... in + let _: unit = save [!continue_513] continue_513: unit (x: pointer:= .., y: pointer:= .., z: pointer:= ..) in ... in + ... in + run while_516(x, y, z) + else + ... in + let _: unit = save [!break_514] break_514: unit (x: pointer:= .., y: pointer:= .., z: pointer:= ..) in ... in + ... in + let _: unit = + let a_537: loaded integer = ... in + ... in + let _: unit = + let a_538: loaded integer = ... in + let a_515: boolean = + case a_538 of + | Specified(a_539: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if a_515 then + let _: unit = + let _: loaded integer = ... in + ... in + let _: unit = + let _: loaded integer = ... in + ... in + let _: unit = run l(x, y, z) in + ... + else + ... in + let _: unit = + let a_558: loaded integer = ... in + let _: unit = ... in + let _: unit = ... in + let _: unit = ... in + run ret_512(conv_loaded_int('signed int', a_558)) in + let _: unit = ... in + let _: unit = ... in + let _: unit = ... in + ... in +save ret_512: loaded integer (a_559: loaded integer:= ..) in + ... +(let [ret_512] _: unit = + let [ret_512] x: pointer = ... in + let [ret_512] y: pointer = ... in + let [ret_512] z: pointer = ... in + let [ret_512] _: unit = + let a_518: loaded integer = ... in + ... in + let [ret_512] _: unit = + let a_519: loaded integer = ... in + ... in + jump [while_516] while_516(x, y, z) + where [ret_512] join (a_563: unit) : unit := + let [l, ret_512] _: unit = + let _: unit = ... in + let _: unit = + let (x: pointer, y: pointer, z: pointer) = ... in + ... in + ... in + let [l, ret_512] _: unit = + let a_537: loaded integer = ... in + ... in + let [l, ret_512] _: unit = + let [l] a_538: loaded integer = ... in + let [l] a_515: boolean = + case a_538 of + | Specified(a_539: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [l] a_515 then + let [l] _: unit = + let _: loaded integer = ... in + ... in + let [l] _: unit = + let _: loaded integer = ... in + ... in + let [l] _: unit = jump [l] l(x, y, z) in + ... + else + ... in + let [ret_512] _: unit = + let [ret_512] a_558: loaded integer = ... in + let [ret_512] _: unit = ... in + let [ret_512] _: unit = ... in + let [ret_512] _: unit = ... in + jump [ret_512] ret_512(conv_loaded_int('signed int', a_558)) in + let _: unit = ... in + let _: unit = ... in + let _: unit = ... in + ... + and [ret_512] l (x: pointer, y: pointer, z: pointer) : unit := + let [while_516, join] a_561: unit = + let [while_516] _: unit = + let _: unit = + let _: unit = + let _: loaded integer = ... in + ... in + ... in + let _: unit = + let (x: pointer, y: pointer, z: pointer) = ... in + ... in + ... in + jump [while_516] while_516(x, y, z) in + jump [join] join(a_561) + and [ret_512] while_516 (x: pointer, y: pointer, z: pointer) : unit := + let [l, join] a_520: loaded integer = ... in + let [l, join] a_517: boolean = + case a_520 of + | Specified(a_521: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [l, join] a_517 then + let [l] _: unit = + let _: loaded integer = ... in + ... in + jump [l] l(x, y, z) + else + let [join] a_562: unit = ... in + jump [join] join(a_562) + end in +jump [ret_512] ret_512(Specified(0))) + where ret_512 (a_559: loaded integer) : loaded integer := + ... + end +(let [ret_512] _: unit = + let [ret_512] x: pointer = ... in + let [ret_512] y: pointer = ... in + let [ret_512] z: pointer = ... in + let [ret_512] _: unit = + let a_518: loaded integer = ... in + ... in + let [ret_512] _: unit = + let a_519: loaded integer = ... in + ... in + let [ret_512] _: unit = + jump [while_516] while_516(x, y, z) + where [ret_512] join (a_563: unit) : unit := + let [l, ret_512] _: unit = + let _: unit = ... in + let _: unit = + let (x: pointer, y: pointer, z: pointer) = ... in + ... in + ... in + let [l, ret_512] _: unit = + let a_537: loaded integer = ... in + ... in + let [l] a_538: loaded integer = ... in + let [l] a_515: boolean = + case a_538 of + | Specified(a_539: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [l] a_515 then + let [l] _: unit = + let [l] _: unit = + let _: loaded integer = ... in + ... in + let [l] _: unit = + let _: loaded integer = ... in + ... in + jump [l] l(x, y, z) in + ... + else + ... + and [ret_512] l (x: pointer, y: pointer, z: pointer) : unit := + let [while_516, join] a_561: unit = + let [while_516] _: unit = + let _: unit = + let _: unit = + let _: loaded integer = ... in + ... in + ... in + let _: unit = + let (x: pointer, y: pointer, z: pointer) = ... in + ... in + ... in + jump [while_516] while_516(x, y, z) in + jump [join] join(a_561) + and [ret_512] while_516 (x: pointer, y: pointer, z: pointer) : unit := + let [l, join] a_520: loaded integer = ... in + let [l, join] a_517: boolean = + case a_520 of + | Specified(a_521: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [l, join] a_517 then + let [l] _: unit = + let _: loaded integer = ... in + ... in + jump [l] l(x, y, z) + else + let [join] a_562: unit = ... in + jump [join] join(a_562) + end in + let [ret_512] _: unit = + let [ret_512] a_558: loaded integer = ... in + let [ret_512] _: unit = ... in + let [ret_512] _: unit = ... in + let [ret_512] _: unit = ... in + jump [ret_512] ret_512(conv_loaded_int('signed int', a_558)) in + let _: unit = ... in + let _: unit = ... in + let _: unit = ... in + ... in +jump [ret_512] ret_512(Specified(0))) + where ret_512 (a_559: loaded integer) : loaded integer := + ... + end diff --git a/tests/where/cluster_array_double_loop.c b/tests/where/cluster_array_double_loop.c new file mode 100644 index 0000000000..30cbbde26c --- /dev/null +++ b/tests/where/cluster_array_double_loop.c @@ -0,0 +1,21 @@ +typedef struct cluster_t { + int size; // Number in cluster + signed char* chars; // Array in cluster +} cluster_t; + +int tester(cluster_t* clusters) +{ + int total = 0; + for (int k=0; k<10; k++) + { + cluster_t *cluster_k = &clusters[k]; + for (int i = 0; i < cluster_k->size; i++) + { + if (cluster_k->chars[i] < 0) return -1; + total += cluster_k->chars[i]; + } + } + + if (total > 100) total -= 10; + return total; +} diff --git a/tests/where/cluster_array_double_loop.c.debug b/tests/where/cluster_array_double_loop.c.debug new file mode 100644 index 0000000000..c386ecba13 --- /dev/null +++ b/tests/where/cluster_array_double_loop.c.debug @@ -0,0 +1,520 @@ +return code: 0 +let [__cerb_continue0:1, __cerb_continue1:1, ret_519:2, continue_520:1, break_521:1, continue_522:1, break_523:1, while_525:1, while_542:1] _: unit = + let [__cerb_continue0:1, __cerb_continue1:1, ret_519:1, continue_520:1, break_521:1, continue_522:1, break_523:1, while_525:1, while_542:1] total: pointer = + ... in + let [__cerb_continue0:1, __cerb_continue1:1, ret_519:1, continue_520:1, break_521:1, continue_522:1, break_523:1, while_525:1, while_542:1] _: unit = + let a_527: loaded integer = ... in + ... in + let [__cerb_continue0:1, __cerb_continue1:1, ret_519:2, continue_520:1, break_521:1, continue_522:1, break_523:1, while_525:1, while_542:1] _: unit = + let [__cerb_continue0:1, __cerb_continue1:1, ret_519:1, continue_520:1, break_521:1, continue_522:1, break_523:1, while_525:1, while_542:1] k: pointer = + ... in + let [__cerb_continue0:1, __cerb_continue1:1, ret_519:1, continue_520:1, break_521:1, continue_522:1, break_523:1, while_525:1, while_542:1] _: unit = + let a_528: loaded integer = ... in + ... in + let [__cerb_continue0:1, __cerb_continue1:1, ret_519:1, continue_520:1, break_521:1, continue_522:1, break_523:1, while_525:1, while_542:1] _: unit = + let [__cerb_continue0:1, __cerb_continue1:1, ret_519:1, continue_520:1, break_521:1, continue_522:1, break_523:1, while_525:1, while_542:1] _: unit = + save [__cerb_continue0:1, __cerb_continue1:1, ret_519:1, continue_520:1, continue_522:1, break_523:1, while_525:2, while_542:1] while_525: unit (k: pointer:= .., + total: pointer:= ..) in + let [__cerb_continue0:1, __cerb_continue1:1, ret_519:1, continue_520:1, continue_522:1, break_523:1, while_525:1, while_542:1] a_529: loaded integer = + ... in + let [__cerb_continue0:1, __cerb_continue1:1, ret_519:1, continue_520:1, continue_522:1, break_523:1, while_525:1, while_542:1] a_526: boolean = + case a_529 of + | Specified(a_530: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [__cerb_continue0:1, __cerb_continue1:1, ret_519:1, continue_520:1, continue_522:1, break_523:1, while_525:1, while_542:1] a_526 then + let [__cerb_continue0:1, __cerb_continue1:1, ret_519:1, continue_520:1, continue_522:1, break_523:1, while_525:1, while_542:1] _: unit = + let [__cerb_continue0:1, __cerb_continue1:1, ret_519:1, continue_520:1, continue_522:1, break_523:1, while_542:1] _: unit = + let [__cerb_continue0:1, __cerb_continue1:1, ret_519:1, continue_522:1, break_523:1, while_542:1] cluster_k: pointer = ... in + let [__cerb_continue0:1, __cerb_continue1:1, ret_519:1, continue_522:1, break_523:1, while_542:1] _: unit = + let a_544: loaded pointer = ... in + ... in + let [__cerb_continue0:1, __cerb_continue1:1, ret_519:1, continue_522:1, break_523:1, while_542:1] _: unit = + let [__cerb_continue1:1, ret_519:1, continue_522:1, break_523:1, while_542:1] i: pointer = ... in + let [__cerb_continue1:1, ret_519:1, continue_522:1, break_523:1, while_542:1] _: unit = + let a_552: loaded integer = ... in + ... in + let [__cerb_continue1:1, ret_519:1, continue_522:1, break_523:1, while_542:1] _: unit = + let [__cerb_continue1:1, ret_519:1, continue_522:1, break_523:1, while_542:1] _: unit = + save [__cerb_continue1:1, ret_519:1, continue_522:1, while_542:2] while_542: unit (i: pointer:= .., cluster_k: pointer:= .., + k: pointer:= .., total: pointer:= ..) in + let [__cerb_continue1:1, ret_519:1, continue_522:1, while_542:1] a_553: loaded integer = ... in + let [__cerb_continue1:1, ret_519:1, continue_522:1, while_542:1] a_543: boolean = + case a_553 of + | Specified(a_554: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [__cerb_continue1:1, ret_519:1, continue_522:1, while_542:1] a_543 then + let [__cerb_continue1:1, ret_519:1, continue_522:1, while_542:1] _: unit = + let [__cerb_continue1:1, ret_519:1, continue_522:1] _: unit = + let [__cerb_continue1:1, ret_519:1] _: unit = + let [ret_519:1] a_573: loaded integer = ... in + let [ret_519:1] a_572: boolean = + case a_573 of + | Specified(a_574: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [ret_519:1] a_572 then + let [ret_519:1] a_603: loaded integer = ... in + let [ret_519:1] _: unit = ... in + let [ret_519:1] _: unit = ... in + let [ret_519:1] _: unit = ... in + let [ret_519:1] _: unit = ... in + run [ret_519:1] ret_519(conv_loaded_int('signed int', a_603)) + else + ... in + let [__cerb_continue1:1] _: unit = + let _: loaded integer = ... in + ... in + let [__cerb_continue1:1] _: unit = + save [__cerb_continue1:1] __cerb_continue1: unit (i: pointer:= .., cluster_k: pointer:= .., k: pointer:= .., + total: pointer:= ..) in + let _: loaded integer = ... in + ... in + ... in + let [continue_522:1] _: unit = + save [continue_522:1] continue_522: unit (i: pointer:= .., cluster_k: pointer:= .., k: pointer:= .., total: pointer:= ..) in + ... in + ... in + run [while_542:1] while_542(i, cluster_k, k, total) + else + ... in + let [break_523:1] _: unit = + save [break_523:1] break_523: unit (i: pointer:= .., cluster_k: pointer:= .., k: pointer:= .., total: pointer:= ..) in + ... in + ... in + let _: unit = ... in + ... in + let [__cerb_continue0:1] _: unit = + save [__cerb_continue0:1] __cerb_continue0: unit (cluster_k: pointer:= .., k: pointer:= .., total: pointer:= ..) in + let _: loaded integer = ... in + ... in + let _: unit = ... in + ... in + let [continue_520:1] _: unit = save [continue_520:1] continue_520: unit (k: pointer:= .., total: pointer:= ..) in ... in + ... in + run [while_525:1] while_525(k, total) + else + ... in + let [break_521:1] _: unit = save [break_521:1] break_521: unit (k: pointer:= .., total: pointer:= ..) in ... in + ... in + let _: unit = ... in + ... in + let [ret_519:1] _: unit = + let a_634: loaded integer = ... in + let a_524: boolean = + case a_634 of + | Specified(a_635: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if a_524 then + let _: loaded integer = ... in + ... + else + ... in + let [ret_519:1] _: unit = + let [ret_519:1] a_656: loaded integer = ... in + let [ret_519:1] _: unit = ... in + run [ret_519:1] ret_519(conv_loaded_int('signed int', a_656)) in + let _: unit = ... in + ... in +save [ret_519:1] ret_519: loaded integer (a_657: loaded integer:= ..) in + ... +let [ret_519] _: unit = + let total: pointer = ... in + let _: unit = + let a_527: loaded integer = ... in + ... in + let _: unit = + let k: pointer = ... in + let _: unit = + let a_528: loaded integer = ... in + ... in + let _: unit = + let _: unit = + save [while_525] while_525: unit (k: pointer:= .., total: pointer:= ..) in + let a_529: loaded integer = ... in + let a_526: boolean = + case a_529 of + | Specified(a_530: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if a_526 then + let _: unit = + let _: unit = + let cluster_k: pointer = ... in + let _: unit = + let a_544: loaded pointer = ... in + ... in + let _: unit = + let i: pointer = ... in + let _: unit = + let a_552: loaded integer = ... in + ... in + let _: unit = + let _: unit = + save [while_542] while_542: unit (i: pointer:= .., cluster_k: pointer:= .., k: pointer:= .., total: pointer:= ..) in + let a_553: loaded integer = ... in + let a_543: boolean = + case a_553 of + | Specified(a_554: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if a_543 then + let _: unit = + let _: unit = + let _: unit = + let a_573: loaded integer = ... in + let a_572: boolean = + case a_573 of + | Specified(a_574: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if a_572 then + let a_603: loaded integer = ... in + let _: unit = ... in + let _: unit = ... in + let _: unit = ... in + let _: unit = ... in + run ret_519(conv_loaded_int('signed int', a_603)) + else + ... in + let _: unit = + let _: loaded integer = ... in + ... in + let _: unit = + save [!__cerb_continue1] __cerb_continue1: unit (i: pointer:= .., cluster_k: pointer:= .., k: pointer:= .., + total: pointer:= ..) in + let _: loaded integer = ... in + ... in + ... in + let _: unit = + save [!continue_522] continue_522: unit (i: pointer:= .., cluster_k: pointer:= .., k: pointer:= .., total: pointer:= ..) in + ... in + ... in + run while_542(i, cluster_k, k, total) + else + ... in + let _: unit = + save [!break_523] break_523: unit (i: pointer:= .., cluster_k: pointer:= .., k: pointer:= .., total: pointer:= ..) in + ... in + ... in + let _: unit = ... in + ... in + let _: unit = + save [!__cerb_continue0] __cerb_continue0: unit (cluster_k: pointer:= .., k: pointer:= .., total: pointer:= ..) in + let _: loaded integer = ... in + ... in + let _: unit = ... in + ... in + let _: unit = save [!continue_520] continue_520: unit (k: pointer:= .., total: pointer:= ..) in ... in + ... in + run while_525(k, total) + else + ... in + let _: unit = save [!break_521] break_521: unit (k: pointer:= .., total: pointer:= ..) in ... in + ... in + let _: unit = ... in + ... in + let _: unit = + let a_634: loaded integer = ... in + let a_524: boolean = + case a_634 of + | Specified(a_635: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if a_524 then + let _: loaded integer = ... in + ... + else + ... in + let _: unit = + let a_656: loaded integer = ... in + let _: unit = ... in + run ret_519(conv_loaded_int('signed int', a_656)) in + let _: unit = ... in + ... in +save ret_519: loaded integer (a_657: loaded integer:= ..) in + ... +(let [ret_519] _: unit = + let [ret_519] total: pointer = ... in + let [ret_519] _: unit = + let a_527: loaded integer = ... in + ... in + let [ret_519] _: unit = + let [ret_519] k: pointer = ... in + let [ret_519] _: unit = + let a_528: loaded integer = ... in + ... in + let [ret_519] _: unit = + let [ret_519] _: unit = + jump [while_525] while_525(k, total) + where [ret_519] while_525 (k: pointer, total: pointer) : unit := + let [ret_519, while_525] a_529: loaded integer = ... in + let [ret_519, while_525] a_526: boolean = + case a_529 of + | Specified(a_530: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [ret_519, while_525] a_526 then + let [ret_519, while_525] _: unit = + let [ret_519] _: unit = + let [ret_519] cluster_k: pointer = ... in + let [ret_519] _: unit = + let a_544: loaded pointer = ... in + ... in + let [ret_519] _: unit = + let [ret_519] i: pointer = ... in + let [ret_519] _: unit = + let a_552: loaded integer = ... in + ... in + let [ret_519] _: unit = + let [ret_519] _: unit = + jump [while_542] while_542(i, cluster_k, k, total) + where [ret_519] while_542 (i: pointer, cluster_k: pointer, k: pointer, total: pointer) : unit := + let [ret_519, while_542] a_553: loaded integer = ... in + let [ret_519, while_542] a_543: boolean = + case a_553 of + | Specified(a_554: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [ret_519, while_542] a_543 then + let [ret_519, while_542] _: unit = + let [ret_519] _: unit = + let [ret_519] _: unit = + let [ret_519] a_573: loaded integer = ... in + let [ret_519] a_572: boolean = + case a_573 of + | Specified(a_574: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [ret_519] a_572 then + let [ret_519] a_603: loaded integer = ... in + let [ret_519] _: unit = ... in + let [ret_519] _: unit = ... in + let [ret_519] _: unit = ... in + let [ret_519] _: unit = ... in + jump [ret_519] ret_519(conv_loaded_int('signed int', a_603)) + else + ... in + let _: unit = + let _: loaded integer = ... in + ... in + let _: unit = + let (i: pointer, cluster_k: pointer, k: pointer, total: pointer) = ... in + let _: loaded integer = ... in + ... in + ... in + let _: unit = + let (i: pointer, cluster_k: pointer, k: pointer, total: pointer) = ... in + ... in + ... in + jump [while_542] while_542(i, cluster_k, k, total) + else + ... + end in + let _: unit = + let (i: pointer, cluster_k: pointer, k: pointer, total: pointer) = ... in + ... in + ... in + let _: unit = ... in + ... in + let _: unit = + let (cluster_k: pointer, k: pointer, total: pointer) = ... in + let _: loaded integer = ... in + ... in + let _: unit = ... in + ... in + let _: unit = + let (k: pointer, total: pointer) = ... in + ... in + ... in + jump [while_525] while_525(k, total) + else + ... + end in + let _: unit = + let (k: pointer, total: pointer) = ... in + ... in + ... in + let _: unit = ... in + ... in + let [ret_519] _: unit = + let a_634: loaded integer = ... in + let a_524: boolean = + case a_634 of + | Specified(a_635: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if a_524 then + let _: loaded integer = ... in + ... + else + ... in + let [ret_519] _: unit = + let [ret_519] a_656: loaded integer = ... in + let [ret_519] _: unit = ... in + jump [ret_519] ret_519(conv_loaded_int('signed int', a_656)) in + let _: unit = ... in + ... in +jump [ret_519] ret_519(undef(<>))) + where ret_519 (a_657: loaded integer) : loaded integer := + ... + end +(let [ret_519] _: unit = + let [ret_519] total: pointer = ... in + let [ret_519] _: unit = + let [ret_519] _: unit = + let a_527: loaded integer = ... in + ... in + let [ret_519] _: unit = + let [ret_519] k: pointer = ... in + let [ret_519] _: unit = + let [ret_519] _: unit = + let [ret_519] _: unit = + let a_528: loaded integer = ... in + ... in + jump [while_525] while_525(k, total) + where [ret_519] while_525 (k: pointer, total: pointer) : unit := + let [ret_519, while_525] a_529: loaded integer = ... in + let [ret_519, while_525] a_526: boolean = + case a_529 of + | Specified(a_530: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [ret_519, while_525] a_526 then + let [ret_519, while_525] _: unit = + let [ret_519] _: unit = + let [ret_519] cluster_k: pointer = ... in + let [ret_519] _: unit = + let a_544: loaded pointer = ... in + ... in + let [ret_519] _: unit = + let [ret_519] i: pointer = ... in + let [ret_519] _: unit = + let a_552: loaded integer = ... in + ... in + let [ret_519] _: unit = + let [ret_519] _: unit = + jump [while_542] while_542(i, cluster_k, k, total) + where [ret_519] while_542 (i: pointer, cluster_k: pointer, k: pointer, total: pointer) : unit := + let [ret_519, while_542] a_553: loaded integer = ... in + let [ret_519, while_542] a_543: boolean = + case a_553 of + | Specified(a_554: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [ret_519, while_542] a_543 then + let [ret_519, while_542] _: unit = + let [ret_519] _: unit = + let [ret_519] _: unit = + let [ret_519] a_573: loaded integer = ... in + let [ret_519] a_572: boolean = + case a_573 of + | Specified(a_574: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [ret_519] a_572 then + let [ret_519] a_603: loaded integer = ... in + let [ret_519] _: unit = ... in + let [ret_519] _: unit = ... in + let [ret_519] _: unit = ... in + let [ret_519] _: unit = ... in + jump [ret_519] ret_519(conv_loaded_int('signed int', a_603)) + else + ... in + let _: unit = + let _: loaded integer = ... in + ... in + let _: unit = + let (i: pointer, cluster_k: pointer, k: pointer, total: pointer) = ... in + let _: loaded integer = ... in + ... in + ... in + let _: unit = + let (i: pointer, cluster_k: pointer, k: pointer, total: pointer) = ... in + ... in + ... in + jump [while_542] while_542(i, cluster_k, k, total) + else + ... + end in + let _: unit = + let (i: pointer, cluster_k: pointer, k: pointer, total: pointer) = ... in + ... in + ... in + let _: unit = ... in + ... in + let _: unit = + let (cluster_k: pointer, k: pointer, total: pointer) = ... in + let _: loaded integer = ... in + ... in + let _: unit = ... in + ... in + let _: unit = + let (k: pointer, total: pointer) = ... in + ... in + ... in + jump [while_525] while_525(k, total) + else + ... + end in + let _: unit = + let (k: pointer, total: pointer) = ... in + ... in + ... in + let _: unit = ... in + ... in + let [ret_519] _: unit = + let a_634: loaded integer = ... in + let a_524: boolean = + case a_634 of + | Specified(a_635: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if a_524 then + let _: loaded integer = ... in + ... + else + ... in + let [ret_519] a_656: loaded integer = ... in + let [ret_519] _: unit = ... in + jump [ret_519] ret_519(conv_loaded_int('signed int', a_656)) in + let _: unit = ... in + ... in +jump [ret_519] ret_519(undef(<>))) + where ret_519 (a_657: loaded integer) : loaded integer := + ... + end diff --git a/tests/where/cont_break.c b/tests/where/cont_break.c new file mode 100644 index 0000000000..fe3b7bf823 --- /dev/null +++ b/tests/where/cont_break.c @@ -0,0 +1,13 @@ +int main() { + int x = 10; + + while (1) { + if (x < 0) { + break; + } else if (x % 2 == 0) { + --x; + continue; + } + --x; + } +} diff --git a/tests/where/cont_break.c.debug b/tests/where/cont_break.c.debug new file mode 100644 index 0000000000..bc60acf684 --- /dev/null +++ b/tests/where/cont_break.c.debug @@ -0,0 +1,285 @@ +return code: 0 +let [__cerb_continue0:1, ret_509:1, continue_510:1, break_511:1, while_512:1] _: unit = + let [__cerb_continue0:1, continue_510:1, break_511:1, while_512:1] x: pointer = ... in + let [__cerb_continue0:1, continue_510:1, break_511:1, while_512:1] _: unit = + let a_514: loaded integer = ... in + ... in + let [__cerb_continue0:1, continue_510:1, break_511:1, while_512:1] _: unit = + let [__cerb_continue0:1, continue_510:1, break_511:2, while_512:1] _: unit = + save [__cerb_continue0:1, continue_510:1, break_511:1, while_512:2] while_512: unit (x: pointer:= ..) in + let [__cerb_continue0:1, continue_510:1, break_511:1, while_512:1] a_515: loaded integer = ... in + let [__cerb_continue0:1, continue_510:1, break_511:1, while_512:1] a_513: boolean = + case a_515 of + | Specified(a_516: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [__cerb_continue0:1, continue_510:1, break_511:1, while_512:1] a_513 then + let [__cerb_continue0:1, continue_510:1, break_511:1, while_512:1] _: unit = + let [__cerb_continue0:1, continue_510:1, break_511:1] _: unit = + let [__cerb_continue0:2, break_511:1] _: unit = + let [__cerb_continue0:1, break_511:1] _: unit = + let [__cerb_continue0:1, break_511:1] a_523: loaded integer = ... in + let [__cerb_continue0:1, break_511:1] a_522: boolean = + case a_523 of + | Specified(a_524: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [__cerb_continue0:1, break_511:1] a_522 then + let [break_511:1] _: unit = run [break_511:1] break_511(x) in + ... + else + let [__cerb_continue0:1] a_537: loaded integer = ... in + let [__cerb_continue0:1] a_536: boolean = + case a_537 of + | Specified(a_538: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [__cerb_continue0:1] a_536 then + let [__cerb_continue0:1] _: unit = + let _: loaded integer = ... in + ... in + let [__cerb_continue0:1] _: unit = run [__cerb_continue0:1] __cerb_continue0(x) in + ... + else + ... in + let _: unit = + let _: loaded integer = ... in + ... in + ... in + let [__cerb_continue0:1] _: unit = save [__cerb_continue0:1] __cerb_continue0: unit (x: pointer:= ..) in ... in + ... in + let [continue_510:1] _: unit = save [continue_510:1] continue_510: unit (x: pointer:= ..) in ... in + ... in + run [while_512:1] while_512(x) + else + ... in + let [break_511:1] _: unit = save [break_511:1] break_511: unit (x: pointer:= ..) in ... in + ... in + let _: unit = ... in + ... in +save [ret_509:1] ret_509: loaded integer (a_572: loaded integer:= ..) in + ... +let _: unit = + let x: pointer = ... in + let _: unit = + let a_514: loaded integer = ... in + ... in + let _: unit = + let [break_511] _: unit = + save [while_512] while_512: unit (x: pointer:= ..) in + let a_515: loaded integer = ... in + let a_513: boolean = + case a_515 of + | Specified(a_516: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if a_513 then + let _: unit = + let _: unit = + let [__cerb_continue0] _: unit = + let _: unit = + let a_523: loaded integer = ... in + let a_522: boolean = + case a_523 of + | Specified(a_524: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if a_522 then + let _: unit = run break_511(x) in + ... + else + let a_537: loaded integer = ... in + let a_536: boolean = + case a_537 of + | Specified(a_538: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if a_536 then + let _: unit = + let _: loaded integer = ... in + ... in + let _: unit = run __cerb_continue0(x) in + ... + else + ... in + let _: unit = + let _: loaded integer = ... in + ... in + ... in + let _: unit = save __cerb_continue0: unit (x: pointer:= ..) in ... in + ... in + let _: unit = save [!continue_510] continue_510: unit (x: pointer:= ..) in ... in + ... in + run while_512(x) + else + ... in + let _: unit = save break_511: unit (x: pointer:= ..) in ... in + ... in + let _: unit = ... in + ... in +save [!ret_509] ret_509: loaded integer (a_572: loaded integer:= ..) in + ... +let _: unit = + let x: pointer = ... in + let _: unit = + let a_514: loaded integer = ... in + ... in + let _: unit = + (let [break_511] _: unit = + jump [while_512] while_512(x) + where [break_511] while_512 (x: pointer) : unit := + let [break_511, while_512] a_515: loaded integer = ... in + let [break_511, while_512] a_513: boolean = + case a_515 of + | Specified(a_516: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [break_511, while_512] a_513 then + let [break_511, while_512] _: unit = + let [break_511] _: unit = + (let [__cerb_continue0, break_511] _: unit = + let [__cerb_continue0, break_511] _: unit = + let [__cerb_continue0, break_511] a_523: loaded integer = ... in + let [__cerb_continue0, break_511] a_522: boolean = + case a_523 of + | Specified(a_524: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [__cerb_continue0, break_511] a_522 then + let [break_511] _: unit = jump [break_511] break_511(x) in + ... + else + let [__cerb_continue0] a_537: loaded integer = ... in + let [__cerb_continue0] a_536: boolean = + case a_537 of + | Specified(a_538: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [__cerb_continue0] a_536 then + let [__cerb_continue0] _: unit = + let _: loaded integer = ... in + ... in + let [__cerb_continue0] _: unit = jump [__cerb_continue0] __cerb_continue0(x) in + ... + else + ... in + let _: unit = + let _: loaded integer = ... in + ... in + ... in + jump [__cerb_continue0] __cerb_continue0(x)) + where [break_511] __cerb_continue0 (x: pointer) : unit := + let _: unit = ... in + ... + end in + let _: unit = + let (x: pointer) = ... in + ... in + ... in + jump [while_512] while_512(x) + else + ... + end in + jump [break_511] break_511(x)) + where break_511 (x: pointer) : unit := + let _: unit = ... in + ... + end in + let _: unit = ... in + ... in +let (a_572: loaded integer) = ... in +... +let _: unit = + let x: pointer = ... in + let _: unit = + let a_514: loaded integer = ... in + ... in + let _: unit = + (let [break_511] _: unit = + jump [while_512] while_512(x) + where [break_511] while_512 (x: pointer) : unit := + let [break_511, while_512] a_515: loaded integer = ... in + let [break_511, while_512] a_513: boolean = + case a_515 of + | Specified(a_516: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [break_511, while_512] a_513 then + let [break_511, while_512] _: unit = + let [break_511] _: unit = + (let [__cerb_continue0, break_511] _: unit = + let [__cerb_continue0, break_511] _: unit = + let [__cerb_continue0, break_511] a_523: loaded integer = ... in + let [__cerb_continue0, break_511] a_522: boolean = + case a_523 of + | Specified(a_524: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [__cerb_continue0, break_511] a_522 then + let [break_511] _: unit = jump [break_511] break_511(x) in + ... + else + let [__cerb_continue0] a_537: loaded integer = ... in + let [__cerb_continue0] a_536: boolean = + case a_537 of + | Specified(a_538: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [__cerb_continue0] a_536 then + let [__cerb_continue0] _: unit = + let _: loaded integer = ... in + ... in + let [__cerb_continue0] _: unit = jump [__cerb_continue0] __cerb_continue0(x) in + ... + else + ... in + let _: unit = + let _: loaded integer = ... in + ... in + ... in + jump [__cerb_continue0] __cerb_continue0(x)) + where [break_511] __cerb_continue0 (x: pointer) : unit := + let _: unit = ... in + ... + end in + let _: unit = + let (x: pointer) = ... in + ... in + ... in + jump [while_512] while_512(x) + else + ... + end in + jump [break_511] break_511(x)) + where break_511 (x: pointer) : unit := + let _: unit = ... in + ... + end in + let _: unit = ... in + ... in +let (a_572: loaded integer) = ... in +... diff --git a/tests/where/debug.json b/tests/where/debug.json new file mode 100644 index 0000000000..c6c0c2c650 --- /dev/null +++ b/tests/where/debug.json @@ -0,0 +1,6 @@ +{ + "name": "debug", + "args": ["--switches", "save_to_where", "-d", "1", "--typecheck-core"], + "filter": "^(.*\\.c)$", + "timeout": 5 +} diff --git a/tests/where/filter_debug.sh b/tests/where/filter_debug.sh new file mode 100755 index 0000000000..ed7426f7a1 --- /dev/null +++ b/tests/where/filter_debug.sh @@ -0,0 +1,2 @@ +#!/usr/bin/env bash +cerberus "$@" 2> >(tail -n +9 | sed '/\((debug 1):\)\|\(Core typechecking\)/d') diff --git a/tests/where/goto_under_if.c b/tests/where/goto_under_if.c new file mode 100644 index 0000000000..8f3620dce8 --- /dev/null +++ b/tests/where/goto_under_if.c @@ -0,0 +1,15 @@ +int main() +{ + int x = 10; + + if (x > 0) { +inner: + x--; + } + + if (x > 0) { + goto inner; + } + + return x; +} diff --git a/tests/where/goto_under_if.c.debug b/tests/where/goto_under_if.c.debug new file mode 100644 index 0000000000..8ad08f5c69 --- /dev/null +++ b/tests/where/goto_under_if.c.debug @@ -0,0 +1,193 @@ +return code: 0 +let [inner:1, ret_507:2] _: unit = + let [inner:1, ret_507:1] x: pointer = ... in + let [inner:1, ret_507:1] _: unit = + let a_510: loaded integer = ... in + ... in + let [inner:2, ret_507:1] _: unit = + let [inner:1] a_511: loaded integer = ... in + let [inner:1] a_509: boolean = + case a_511 of + | Specified(a_512: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [inner:1] a_509 then + let [inner:1] _: unit = + save [inner:1] inner: unit (x: pointer:= ..) in + let _: loaded integer = ... in + ... in + ... + else + ... in + let [inner:1, ret_507:1] _: unit = + let [inner:1] a_527: loaded integer = ... in + let [inner:1] a_508: boolean = + case a_527 of + | Specified(a_528: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [inner:1] a_508 then + let [inner:1] _: unit = run [inner:1] inner(x) in + ... + else + ... in + let [ret_507:1] _: unit = + let [ret_507:1] a_541: loaded integer = ... in + let [ret_507:1] _: unit = ... in + run [ret_507:1] ret_507(conv_loaded_int('signed int', a_541)) in + let _: unit = ... in + ... in +save [ret_507:1] ret_507: loaded integer (a_542: loaded integer:= ..) in + ... +let [ret_507] _: unit = + let x: pointer = ... in + let _: unit = + let a_510: loaded integer = ... in + ... in + let [inner] _: unit = + let a_511: loaded integer = ... in + let a_509: boolean = + case a_511 of + | Specified(a_512: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if a_509 then + let _: unit = + save inner: unit (x: pointer:= ..) in + let _: loaded integer = ... in + ... in + ... + else + ... in + let _: unit = + let a_527: loaded integer = ... in + let a_508: boolean = + case a_527 of + | Specified(a_528: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if a_508 then + let _: unit = run inner(x) in + ... + else + ... in + let _: unit = + let a_541: loaded integer = ... in + let _: unit = ... in + run ret_507(conv_loaded_int('signed int', a_541)) in + let _: unit = ... in + ... in +save ret_507: loaded integer (a_542: loaded integer:= ..) in + ... +(let [ret_507] _: unit = + let [ret_507] x: pointer = ... in + let [ret_507] _: unit = + let a_510: loaded integer = ... in + ... in + (let [inner, join] a_511: loaded integer = ... in + let [inner, join] a_509: boolean = + case a_511 of + | Specified(a_512: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [inner, join] a_509 then + jump [inner] inner(x) + else + let [join] a_545: unit = ... in + jump [join] join(a_545)) + where [ret_507] join (a_546: unit) : unit := + let [inner, ret_507] _: unit = ... in + let [inner, ret_507] _: unit = + let [inner] a_527: loaded integer = ... in + let [inner] a_508: boolean = + case a_527 of + | Specified(a_528: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [inner] a_508 then + let [inner] _: unit = jump [inner] inner(x) in + ... + else + ... in + let [ret_507] _: unit = + let [ret_507] a_541: loaded integer = ... in + let [ret_507] _: unit = ... in + jump [ret_507] ret_507(conv_loaded_int('signed int', a_541)) in + let _: unit = ... in + ... + and [ret_507] inner (x: pointer) : unit := + let [join] a_544: unit = + let _: unit = + let _: loaded integer = ... in + ... in + ... in + jump [join] join(a_544) + end in +jump [ret_507] ret_507(Specified(0))) + where ret_507 (a_542: loaded integer) : loaded integer := + ... + end +(let [ret_507] _: unit = + let [ret_507] x: pointer = ... in + let [ret_507] _: unit = + let a_510: loaded integer = ... in + ... in + let [ret_507] _: unit = + (let [inner, join] a_511: loaded integer = ... in + let [inner, join] a_509: boolean = + case a_511 of + | Specified(a_512: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [inner, join] a_509 then + jump [inner] inner(x) + else + let [join] a_545: unit = ... in + jump [join] join(a_545)) + where [ret_507] join (a_546: unit) : unit := + let [inner, ret_507] _: unit = ... in + let [inner] a_527: loaded integer = ... in + let [inner] a_508: boolean = + case a_527 of + | Specified(a_528: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [inner] a_508 then + let [inner] _: unit = jump [inner] inner(x) in + ... + else + ... + and [ret_507] inner (x: pointer) : unit := + let [join] a_544: unit = + let _: unit = + let _: loaded integer = ... in + ... in + ... in + jump [join] join(a_544) + end in + let [ret_507] _: unit = + let [ret_507] a_541: loaded integer = ... in + let [ret_507] _: unit = ... in + jump [ret_507] ret_507(conv_loaded_int('signed int', a_541)) in + let _: unit = ... in + ... in +jump [ret_507] ret_507(Specified(0))) + where ret_507 (a_542: loaded integer) : loaded integer := + ... + end diff --git a/tests/where/init_before_loop.c b/tests/where/init_before_loop.c new file mode 100644 index 0000000000..3114a2c0d2 --- /dev/null +++ b/tests/where/init_before_loop.c @@ -0,0 +1,9 @@ +int main() +{ + int x = 10; + while (x > 0) + { + x--; + } + return x; +} diff --git a/tests/where/init_before_loop.c.debug b/tests/where/init_before_loop.c.debug new file mode 100644 index 0000000000..493a57a83a --- /dev/null +++ b/tests/where/init_before_loop.c.debug @@ -0,0 +1,169 @@ +return code: 0 +let [ret_509:2, continue_510:1, break_511:1, while_512:1] _: unit = + let [ret_509:1, continue_510:1, break_511:1, while_512:1] x: pointer = ... in + let [ret_509:1, continue_510:1, break_511:1, while_512:1] _: unit = + let a_514: loaded integer = ... in + ... in + let [ret_509:1, continue_510:1, break_511:1, while_512:1] _: unit = + let [continue_510:1, break_511:1, while_512:1] _: unit = + save [continue_510:1, while_512:2] while_512: unit (x: pointer:= ..) in + let [continue_510:1, while_512:1] a_515: loaded integer = ... in + let [continue_510:1, while_512:1] a_513: boolean = + case a_515 of + | Specified(a_516: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [continue_510:1, while_512:1] a_513 then + let [continue_510:1, while_512:1] _: unit = + let [continue_510:1] _: unit = + let _: unit = + let _: loaded integer = ... in + ... in + ... in + let [continue_510:1] _: unit = save [continue_510:1] continue_510: unit (x: pointer:= ..) in ... in + ... in + run [while_512:1] while_512(x) + else + ... in + let [break_511:1] _: unit = save [break_511:1] break_511: unit (x: pointer:= ..) in ... in + ... in + let [ret_509:1] _: unit = + let [ret_509:1] a_532: loaded integer = ... in + let [ret_509:1] _: unit = ... in + run [ret_509:1] ret_509(conv_loaded_int('signed int', a_532)) in + let _: unit = ... in + ... in +save [ret_509:1] ret_509: loaded integer (a_533: loaded integer:= ..) in + ... +let [ret_509] _: unit = + let x: pointer = ... in + let _: unit = + let a_514: loaded integer = ... in + ... in + let _: unit = + let _: unit = + save [while_512] while_512: unit (x: pointer:= ..) in + let a_515: loaded integer = ... in + let a_513: boolean = + case a_515 of + | Specified(a_516: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if a_513 then + let _: unit = + let _: unit = + let _: unit = + let _: loaded integer = ... in + ... in + ... in + let _: unit = save [!continue_510] continue_510: unit (x: pointer:= ..) in ... in + ... in + run while_512(x) + else + ... in + let _: unit = save [!break_511] break_511: unit (x: pointer:= ..) in ... in + ... in + let _: unit = + let a_532: loaded integer = ... in + let _: unit = ... in + run ret_509(conv_loaded_int('signed int', a_532)) in + let _: unit = ... in + ... in +save ret_509: loaded integer (a_533: loaded integer:= ..) in + ... +(let [ret_509] _: unit = + let [ret_509] x: pointer = ... in + let [ret_509] _: unit = + let a_514: loaded integer = ... in + ... in + let [ret_509] _: unit = + let _: unit = + jump [while_512] while_512(x) + where while_512 (x: pointer) : unit := + let [while_512] a_515: loaded integer = ... in + let [while_512] a_513: boolean = + case a_515 of + | Specified(a_516: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [while_512] a_513 then + let [while_512] _: unit = + let _: unit = + let _: unit = + let _: loaded integer = ... in + ... in + ... in + let _: unit = + let (x: pointer) = ... in + ... in + ... in + jump [while_512] while_512(x) + else + ... + end in + let _: unit = + let (x: pointer) = ... in + ... in + ... in + let [ret_509] _: unit = + let [ret_509] a_532: loaded integer = ... in + let [ret_509] _: unit = ... in + jump [ret_509] ret_509(conv_loaded_int('signed int', a_532)) in + let _: unit = ... in + ... in +jump [ret_509] ret_509(Specified(0))) + where ret_509 (a_533: loaded integer) : loaded integer := + ... + end +(let [ret_509] _: unit = + let [ret_509] x: pointer = ... in + let [ret_509] _: unit = + let [ret_509] _: unit = + let a_514: loaded integer = ... in + ... in + let [ret_509] _: unit = + let _: unit = + jump [while_512] while_512(x) + where while_512 (x: pointer) : unit := + let [while_512] a_515: loaded integer = ... in + let [while_512] a_513: boolean = + case a_515 of + | Specified(a_516: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [while_512] a_513 then + let [while_512] _: unit = + let _: unit = + let _: unit = + let _: loaded integer = ... in + ... in + ... in + let _: unit = + let (x: pointer) = ... in + ... in + ... in + jump [while_512] while_512(x) + else + ... + end in + let _: unit = + let (x: pointer) = ... in + ... in + ... in + let [ret_509] a_532: loaded integer = ... in + let [ret_509] _: unit = ... in + jump [ret_509] ret_509(conv_loaded_int('signed int', a_532)) in + let _: unit = ... in + ... in +jump [ret_509] ret_509(Specified(0))) + where ret_509 (a_533: loaded integer) : loaded integer := + ... + end diff --git a/tests/where/perplexing-ub.c b/tests/where/perplexing-ub.c new file mode 100644 index 0000000000..96ad0f01bb --- /dev/null +++ b/tests/where/perplexing-ub.c @@ -0,0 +1,13 @@ +int main() { + int *p; + goto l2; +l1: + while (1) { + int x = 5; + // p = &x; + return *p; +l2: + p = &x; + goto l1; + } +} diff --git a/tests/where/perplexing-ub.c.debug b/tests/where/perplexing-ub.c.debug new file mode 100644 index 0000000000..98039ae3d6 --- /dev/null +++ b/tests/where/perplexing-ub.c.debug @@ -0,0 +1,230 @@ +return code: 0 +let [l1:1, l2:1, ret_512:2, continue_513:1, break_514:1, while_515:1] _: unit = + let [l1:1, l2:1, ret_512:1, continue_513:1, break_514:1, while_515:1] p: pointer = ... in + let [l1:1, l2:1, ret_512:1, continue_513:1, break_514:1, while_515:1] _: unit = ... in + let [l1:1, l2:2, ret_512:1, continue_513:1, break_514:1, while_515:1] _: unit = + let [l2:1] x: pointer = ... in + run [l2:1] l2(x, p) in + let [l1:1, l2:1, ret_512:1, continue_513:1, break_514:1, while_515:1] _: unit = + save [l1:2, l2:1, ret_512:1, continue_513:1, break_514:1, while_515:1] l1: unit (p: pointer:= ..) in + let [l1:1, l2:1, ret_512:1, continue_513:1, break_514:1, while_515:1] _: unit = + save [l1:1, l2:1, ret_512:1, continue_513:1, while_515:2] while_515: unit (p: pointer:= ..) in + let [l1:1, l2:1, ret_512:1, continue_513:1, while_515:1] a_517: loaded integer = ... in + let [l1:1, l2:1, ret_512:1, continue_513:1, while_515:1] a_516: boolean = + case a_517 of + | Specified(a_518: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [l1:1, l2:1, ret_512:1, continue_513:1, while_515:1] a_516 then + let [l1:1, l2:1, ret_512:1, continue_513:1, while_515:1] _: unit = + let [l1:1, l2:1, ret_512:1, continue_513:1] _: unit = + let [l1:1, l2:1, ret_512:1] x: pointer = ... in + let [l1:1, l2:1, ret_512:1] _: unit = + let a_524: loaded integer = ... in + ... in + let [l1:1, l2:1, ret_512:1] _: unit = + let [ret_512:1] a_530: loaded integer = ... in + let [ret_512:1] _: unit = ... in + let [ret_512:1] _: unit = ... in + run [ret_512:1] ret_512(conv_loaded_int('signed int', a_530)) in + let [l1:1, l2:1] _: unit = + save [l2:1] l2: unit (x: pointer:= .., p: pointer:= ..) in + let _: loaded pointer = ... in + ... in + let [l1:1] _: unit = + let [l1:1] _: unit = ... in + run [l1:1] l1(p) in + let _: unit = ... in + ... in + let [continue_513:1] _: unit = save [continue_513:1] continue_513: unit (p: pointer:= ..) in ... in + ... in + run [while_515:1] while_515(p) + else + ... in + let [break_514:1] _: unit = save [break_514:1] break_514: unit (p: pointer:= ..) in ... in + ... in + let _: unit = ... in + ... in +save [ret_512:1] ret_512: loaded integer (a_534: loaded integer:= ..) in + ... +let [ret_512] _: unit = + let p: pointer = ... in + let _: unit = ... in + let [l2] _: unit = + let x: pointer = ... in + run l2(x, p) in + let _: unit = + save [l1] l1: unit (p: pointer:= ..) in + let _: unit = + save [while_515] while_515: unit (p: pointer:= ..) in + let a_517: loaded integer = ... in + let a_516: boolean = + case a_517 of + | Specified(a_518: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if a_516 then + let _: unit = + let _: unit = + let x: pointer = ... in + let _: unit = + let a_524: loaded integer = ... in + ... in + let _: unit = + let a_530: loaded integer = ... in + let _: unit = ... in + let _: unit = ... in + run ret_512(conv_loaded_int('signed int', a_530)) in + let _: unit = + save l2: unit (x: pointer:= .., p: pointer:= ..) in + let _: loaded pointer = ... in + ... in + let _: unit = + let _: unit = ... in + run l1(p) in + let _: unit = ... in + ... in + let _: unit = save [!continue_513] continue_513: unit (p: pointer:= ..) in ... in + ... in + run while_515(p) + else + ... in + let _: unit = save [!break_514] break_514: unit (p: pointer:= ..) in ... in + ... in + let _: unit = ... in + ... in +save ret_512: loaded integer (a_534: loaded integer:= ..) in + ... +(let [ret_512] _: unit = + let [ret_512] p: pointer = ... in + let [ret_512] _: unit = ... in + (let [l1, l2] _: unit = + let [l2] x: pointer = ... in + jump [l2] l2(x, p) in + jump [l1] l1(p)) + where [ret_512] join (a_538: unit) : unit := + let _: unit = + let _: unit = ... in + let _: unit = + let (p: pointer) = ... in + ... in + ... in + let _: unit = ... in + ... + and [ret_512] l2 (x: pointer, p: pointer) : unit := + let [l1, while_515, join] a_536: unit = + let [l1, while_515] _: unit = + let [l1] _: unit = + let [l1] _: unit = + let _: loaded pointer = ... in + ... in + let [l1] _: unit = + let [l1] _: unit = ... in + jump [l1] l1(p) in + let _: unit = ... in + ... in + let _: unit = + let (p: pointer) = ... in + ... in + ... in + jump [while_515] while_515(p) in + jump [join] join(a_536) + and [ret_512] while_515 (p: pointer) : unit := + let [l2, ret_512, join] a_517: loaded integer = ... in + let [l2, ret_512, join] a_516: boolean = + case a_517 of + | Specified(a_518: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [l2, ret_512, join] a_516 then + let [l2, ret_512] x: pointer = ... in + let [l2, ret_512] _: unit = + let a_524: loaded integer = ... in + ... in + let [l2, ret_512] _: unit = + let [ret_512] a_530: loaded integer = ... in + let [ret_512] _: unit = ... in + let [ret_512] _: unit = ... in + jump [ret_512] ret_512(conv_loaded_int('signed int', a_530)) in + jump [l2] l2(x, p) + else + let [join] a_537: unit = ... in + jump [join] join(a_537) + and [ret_512] l1 (p: pointer) : unit := + jump [while_515] while_515(p) + end in +jump [ret_512] ret_512(Specified(0))) + where ret_512 (a_534: loaded integer) : loaded integer := + ... + end +(let [ret_512] _: unit = + let [ret_512] p: pointer = ... in + let [ret_512] _: unit = ... in + let [ret_512] _: unit = + let [ret_512] _: unit = + (let [l1, l2] _: unit = + let [l2] x: pointer = ... in + jump [l2] l2(x, p) in + jump [l1] l1(p)) + where [ret_512] join (a_538: unit) : unit := + ... + and [ret_512] l2 (x: pointer, p: pointer) : unit := + let [l1, while_515, join] a_536: unit = + let [l1, while_515] _: unit = + let [l1] _: unit = + let [l1] _: unit = + let [l1] _: unit = + let _: loaded pointer = ... in + ... in + let [l1] _: unit = ... in + jump [l1] l1(p) in + let _: unit = ... in + ... in + let _: unit = + let (p: pointer) = ... in + ... in + ... in + jump [while_515] while_515(p) in + jump [join] join(a_536) + and [ret_512] while_515 (p: pointer) : unit := + let [l2, ret_512, join] a_517: loaded integer = ... in + let [l2, ret_512, join] a_516: boolean = + case a_517 of + | Specified(a_518: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [l2, ret_512, join] a_516 then + let [l2, ret_512] x: pointer = ... in + let [l2, ret_512] _: unit = + let a_524: loaded integer = ... in + ... in + let [l2, ret_512] _: unit = + let [ret_512] a_530: loaded integer = ... in + let [ret_512] _: unit = ... in + let [ret_512] _: unit = ... in + jump [ret_512] ret_512(conv_loaded_int('signed int', a_530)) in + jump [l2] l2(x, p) + else + let [join] a_537: unit = ... in + jump [join] join(a_537) + and [ret_512] l1 (p: pointer) : unit := + jump [while_515] while_515(p) + end in + let _: unit = + let (p: pointer) = ... in + ... in + ... in + let _: unit = ... in + ... in +jump [ret_512] ret_512(Specified(0))) + where ret_512 (a_534: loaded integer) : loaded integer := + ... + end diff --git a/tests/where/uninit_do_while.c b/tests/where/uninit_do_while.c new file mode 100644 index 0000000000..01586f9531 --- /dev/null +++ b/tests/where/uninit_do_while.c @@ -0,0 +1,9 @@ +int main() +{ + int x; + do + { + x; + } while (x > 0); + return x; +} diff --git a/tests/where/uninit_do_while.c.debug b/tests/where/uninit_do_while.c.debug new file mode 100644 index 0000000000..0e8277c3cd --- /dev/null +++ b/tests/where/uninit_do_while.c.debug @@ -0,0 +1,153 @@ +return code: 0 +let [ret_509:2, continue_510:1, break_511:1, do_512:1] _: unit = + let [ret_509:1, continue_510:1, break_511:1, do_512:1] x: pointer = ... in + let [ret_509:1, continue_510:1, break_511:1, do_512:1] _: unit = ... in + let [ret_509:1, continue_510:1, break_511:1, do_512:1] _: unit = + let [continue_510:1, break_511:1, do_512:1] _: unit = + save [continue_510:1, do_512:2] do_512: unit (x: pointer:= ..) in + let [continue_510:1, do_512:1] _: unit = + let [continue_510:1] _: unit = + let _: unit = + let _: loaded integer = ... in + ... in + ... in + let [continue_510:1] _: unit = save [continue_510:1] continue_510: unit (x: pointer:= ..) in ... in + ... in + let [do_512:1] a_514: loaded integer = ... in + case [do_512:1] a_514 of + | Specified(a_513: integer) => + if [do_512:1] not(a_513 = 0) then + run [do_512:1] do_512(x) + else + ... + | Unspecified(_: ctype) => + ... + end in + let [break_511:1] _: unit = save [break_511:1] break_511: unit (x: pointer:= ..) in ... in + ... in + let [ret_509:1] _: unit = + let [ret_509:1] a_523: loaded integer = ... in + let [ret_509:1] _: unit = ... in + run [ret_509:1] ret_509(conv_loaded_int('signed int', a_523)) in + let _: unit = ... in + ... in +save [ret_509:1] ret_509: loaded integer (a_524: loaded integer:= ..) in + ... +let [ret_509] _: unit = + let x: pointer = ... in + let _: unit = ... in + let _: unit = + let _: unit = + save [do_512] do_512: unit (x: pointer:= ..) in + let _: unit = + let _: unit = + let _: unit = + let _: loaded integer = ... in + ... in + ... in + let _: unit = save [!continue_510] continue_510: unit (x: pointer:= ..) in ... in + ... in + let a_514: loaded integer = ... in + case a_514 of + | Specified(a_513: integer) => + if not(a_513 = 0) then + run do_512(x) + else + ... + | Unspecified(_: ctype) => + ... + end in + let _: unit = save [!break_511] break_511: unit (x: pointer:= ..) in ... in + ... in + let _: unit = + let a_523: loaded integer = ... in + let _: unit = ... in + run ret_509(conv_loaded_int('signed int', a_523)) in + let _: unit = ... in + ... in +save ret_509: loaded integer (a_524: loaded integer:= ..) in + ... +(let [ret_509] _: unit = + let [ret_509] x: pointer = ... in + let [ret_509] _: unit = ... in + let [ret_509] _: unit = + let _: unit = + jump [do_512] do_512(x) + where do_512 (x: pointer) : unit := + let [do_512] _: unit = + let _: unit = + let _: unit = + let _: loaded integer = ... in + ... in + ... in + let _: unit = + let (x: pointer) = ... in + ... in + ... in + let [do_512] a_514: loaded integer = ... in + case [do_512] a_514 of + | Specified(a_513: integer) => + if [do_512] not(a_513 = 0) then + jump [do_512] do_512(x) + else + ... + | Unspecified(_: ctype) => + ... + end + end in + let _: unit = + let (x: pointer) = ... in + ... in + ... in + let [ret_509] _: unit = + let [ret_509] a_523: loaded integer = ... in + let [ret_509] _: unit = ... in + jump [ret_509] ret_509(conv_loaded_int('signed int', a_523)) in + let _: unit = ... in + ... in +jump [ret_509] ret_509(Specified(0))) + where ret_509 (a_524: loaded integer) : loaded integer := + ... + end +(let [ret_509] _: unit = + let [ret_509] x: pointer = ... in + let [ret_509] _: unit = + let [ret_509] _: unit = ... in + let [ret_509] _: unit = + let _: unit = + jump [do_512] do_512(x) + where do_512 (x: pointer) : unit := + let [do_512] _: unit = + let _: unit = + let _: unit = + let _: loaded integer = ... in + ... in + ... in + let _: unit = + let (x: pointer) = ... in + ... in + ... in + let [do_512] a_514: loaded integer = ... in + case [do_512] a_514 of + | Specified(a_513: integer) => + if [do_512] not(a_513 = 0) then + jump [do_512] do_512(x) + else + ... + | Unspecified(_: ctype) => + ... + end + end in + let _: unit = + let (x: pointer) = ... in + ... in + ... in + let [ret_509] a_523: loaded integer = ... in + let [ret_509] _: unit = ... in + jump [ret_509] ret_509(conv_loaded_int('signed int', a_523)) in + let _: unit = ... in + ... in +jump [ret_509] ret_509(Specified(0))) + where ret_509 (a_524: loaded integer) : loaded integer := + ... + end diff --git a/tests/where/while_10.c b/tests/where/while_10.c new file mode 100644 index 0000000000..3f2a4efc7e --- /dev/null +++ b/tests/where/while_10.c @@ -0,0 +1,7 @@ +int main(void) { + int n = 0; + while (n < 10) { + n = n + 1; + } + return n; // 10 +} diff --git a/tests/where/while_10.c.debug b/tests/where/while_10.c.debug new file mode 100644 index 0000000000..067f6ac2b2 --- /dev/null +++ b/tests/where/while_10.c.debug @@ -0,0 +1,169 @@ +return code: 0 +let [ret_509:2, continue_510:1, break_511:1, while_512:1] _: unit = + let [ret_509:1, continue_510:1, break_511:1, while_512:1] n: pointer = ... in + let [ret_509:1, continue_510:1, break_511:1, while_512:1] _: unit = + let a_514: loaded integer = ... in + ... in + let [ret_509:1, continue_510:1, break_511:1, while_512:1] _: unit = + let [continue_510:1, break_511:1, while_512:1] _: unit = + save [continue_510:1, while_512:2] while_512: unit (n: pointer:= ..) in + let [continue_510:1, while_512:1] a_515: loaded integer = ... in + let [continue_510:1, while_512:1] a_513: boolean = + case a_515 of + | Specified(a_516: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [continue_510:1, while_512:1] a_513 then + let [continue_510:1, while_512:1] _: unit = + let [continue_510:1] _: unit = + let _: unit = + let _: loaded integer = ... in + ... in + ... in + let [continue_510:1] _: unit = save [continue_510:1] continue_510: unit (n: pointer:= ..) in ... in + ... in + run [while_512:1] while_512(n) + else + ... in + let [break_511:1] _: unit = save [break_511:1] break_511: unit (n: pointer:= ..) in ... in + ... in + let [ret_509:1] _: unit = + let [ret_509:1] a_537: loaded integer = ... in + let [ret_509:1] _: unit = ... in + run [ret_509:1] ret_509(conv_loaded_int('signed int', a_537)) in + let _: unit = ... in + ... in +save [ret_509:1] ret_509: loaded integer (a_538: loaded integer:= ..) in + ... +let [ret_509] _: unit = + let n: pointer = ... in + let _: unit = + let a_514: loaded integer = ... in + ... in + let _: unit = + let _: unit = + save [while_512] while_512: unit (n: pointer:= ..) in + let a_515: loaded integer = ... in + let a_513: boolean = + case a_515 of + | Specified(a_516: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if a_513 then + let _: unit = + let _: unit = + let _: unit = + let _: loaded integer = ... in + ... in + ... in + let _: unit = save [!continue_510] continue_510: unit (n: pointer:= ..) in ... in + ... in + run while_512(n) + else + ... in + let _: unit = save [!break_511] break_511: unit (n: pointer:= ..) in ... in + ... in + let _: unit = + let a_537: loaded integer = ... in + let _: unit = ... in + run ret_509(conv_loaded_int('signed int', a_537)) in + let _: unit = ... in + ... in +save ret_509: loaded integer (a_538: loaded integer:= ..) in + ... +(let [ret_509] _: unit = + let [ret_509] n: pointer = ... in + let [ret_509] _: unit = + let a_514: loaded integer = ... in + ... in + let [ret_509] _: unit = + let _: unit = + jump [while_512] while_512(n) + where while_512 (n: pointer) : unit := + let [while_512] a_515: loaded integer = ... in + let [while_512] a_513: boolean = + case a_515 of + | Specified(a_516: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [while_512] a_513 then + let [while_512] _: unit = + let _: unit = + let _: unit = + let _: loaded integer = ... in + ... in + ... in + let _: unit = + let (n: pointer) = ... in + ... in + ... in + jump [while_512] while_512(n) + else + ... + end in + let _: unit = + let (n: pointer) = ... in + ... in + ... in + let [ret_509] _: unit = + let [ret_509] a_537: loaded integer = ... in + let [ret_509] _: unit = ... in + jump [ret_509] ret_509(conv_loaded_int('signed int', a_537)) in + let _: unit = ... in + ... in +jump [ret_509] ret_509(Specified(0))) + where ret_509 (a_538: loaded integer) : loaded integer := + ... + end +(let [ret_509] _: unit = + let [ret_509] n: pointer = ... in + let [ret_509] _: unit = + let [ret_509] _: unit = + let a_514: loaded integer = ... in + ... in + let [ret_509] _: unit = + let _: unit = + jump [while_512] while_512(n) + where while_512 (n: pointer) : unit := + let [while_512] a_515: loaded integer = ... in + let [while_512] a_513: boolean = + case a_515 of + | Specified(a_516: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [while_512] a_513 then + let [while_512] _: unit = + let _: unit = + let _: unit = + let _: loaded integer = ... in + ... in + ... in + let _: unit = + let (n: pointer) = ... in + ... in + ... in + jump [while_512] while_512(n) + else + ... + end in + let _: unit = + let (n: pointer) = ... in + ... in + ... in + let [ret_509] a_537: loaded integer = ... in + let [ret_509] _: unit = ... in + jump [ret_509] ret_509(conv_loaded_int('signed int', a_537)) in + let _: unit = ... in + ... in +jump [ret_509] ret_509(Specified(0))) + where ret_509 (a_538: loaded integer) : loaded integer := + ... + end diff --git a/tests/where/while_sum.c b/tests/where/while_sum.c new file mode 100644 index 0000000000..c595c8a6b3 --- /dev/null +++ b/tests/where/while_sum.c @@ -0,0 +1,8 @@ +int f(int i, int limit) { + int sum = 0; + while (i < limit) { + sum = sum + i; + i = i + 1; + } + return sum; +} diff --git a/tests/where/while_sum.c.debug b/tests/where/while_sum.c.debug new file mode 100644 index 0000000000..3bcc187a1a --- /dev/null +++ b/tests/where/while_sum.c.debug @@ -0,0 +1,181 @@ +return code: 0 +let [ret_513:2, continue_514:1, break_515:1, while_516:1] _: unit = + let [ret_513:1, continue_514:1, break_515:1, while_516:1] sum: pointer = ... in + let [ret_513:1, continue_514:1, break_515:1, while_516:1] _: unit = + let a_518: loaded integer = ... in + ... in + let [ret_513:1, continue_514:1, break_515:1, while_516:1] _: unit = + let [continue_514:1, break_515:1, while_516:1] _: unit = + save [continue_514:1, while_516:2] while_516: unit (sum: pointer:= ..) in + let [continue_514:1, while_516:1] a_519: loaded integer = ... in + let [continue_514:1, while_516:1] a_517: boolean = + case a_519 of + | Specified(a_520: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [continue_514:1, while_516:1] a_517 then + let [continue_514:1, while_516:1] _: unit = + let [continue_514:1] _: unit = + let _: unit = + let _: loaded integer = ... in + ... in + let _: unit = + let _: loaded integer = ... in + ... in + ... in + let [continue_514:1] _: unit = save [continue_514:1] continue_514: unit (sum: pointer:= ..) in ... in + ... in + run [while_516:1] while_516(sum) + else + ... in + let [break_515:1] _: unit = save [break_515:1] break_515: unit (sum: pointer:= ..) in ... in + ... in + let [ret_513:1] _: unit = + let [ret_513:1] a_551: loaded integer = ... in + let [ret_513:1] _: unit = ... in + run [ret_513:1] ret_513(conv_loaded_int('signed int', a_551)) in + let _: unit = ... in + ... in +save [ret_513:1] ret_513: loaded integer (a_552: loaded integer:= ..) in + ... +let [ret_513] _: unit = + let sum: pointer = ... in + let _: unit = + let a_518: loaded integer = ... in + ... in + let _: unit = + let _: unit = + save [while_516] while_516: unit (sum: pointer:= ..) in + let a_519: loaded integer = ... in + let a_517: boolean = + case a_519 of + | Specified(a_520: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if a_517 then + let _: unit = + let _: unit = + let _: unit = + let _: loaded integer = ... in + ... in + let _: unit = + let _: loaded integer = ... in + ... in + ... in + let _: unit = save [!continue_514] continue_514: unit (sum: pointer:= ..) in ... in + ... in + run while_516(sum) + else + ... in + let _: unit = save [!break_515] break_515: unit (sum: pointer:= ..) in ... in + ... in + let _: unit = + let a_551: loaded integer = ... in + let _: unit = ... in + run ret_513(conv_loaded_int('signed int', a_551)) in + let _: unit = ... in + ... in +save ret_513: loaded integer (a_552: loaded integer:= ..) in + ... +(let [ret_513] _: unit = + let [ret_513] sum: pointer = ... in + let [ret_513] _: unit = + let a_518: loaded integer = ... in + ... in + let [ret_513] _: unit = + let _: unit = + jump [while_516] while_516(sum) + where while_516 (sum: pointer) : unit := + let [while_516] a_519: loaded integer = ... in + let [while_516] a_517: boolean = + case a_519 of + | Specified(a_520: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [while_516] a_517 then + let [while_516] _: unit = + let _: unit = + let _: unit = + let _: loaded integer = ... in + ... in + let _: unit = + let _: loaded integer = ... in + ... in + ... in + let _: unit = + let (sum: pointer) = ... in + ... in + ... in + jump [while_516] while_516(sum) + else + ... + end in + let _: unit = + let (sum: pointer) = ... in + ... in + ... in + let [ret_513] _: unit = + let [ret_513] a_551: loaded integer = ... in + let [ret_513] _: unit = ... in + jump [ret_513] ret_513(conv_loaded_int('signed int', a_551)) in + let _: unit = ... in + ... in +jump [ret_513] ret_513(undef(<>))) + where ret_513 (a_552: loaded integer) : loaded integer := + ... + end +(let [ret_513] _: unit = + let [ret_513] sum: pointer = ... in + let [ret_513] _: unit = + let [ret_513] _: unit = + let a_518: loaded integer = ... in + ... in + let [ret_513] _: unit = + let _: unit = + jump [while_516] while_516(sum) + where while_516 (sum: pointer) : unit := + let [while_516] a_519: loaded integer = ... in + let [while_516] a_517: boolean = + case a_519 of + | Specified(a_520: integer) => + ... + | Unspecified(_: ctype) => + ... + end in + if [while_516] a_517 then + let [while_516] _: unit = + let _: unit = + let _: unit = + let _: loaded integer = ... in + ... in + let _: unit = + let _: loaded integer = ... in + ... in + ... in + let _: unit = + let (sum: pointer) = ... in + ... in + ... in + jump [while_516] while_516(sum) + else + ... + end in + let _: unit = + let (sum: pointer) = ... in + ... in + ... in + let [ret_513] a_551: loaded integer = ... in + let [ret_513] _: unit = ... in + jump [ret_513] ret_513(conv_loaded_int('signed int', a_551)) in + let _: unit = ... in + ... in +jump [ret_513] ret_513(undef(<>))) + where ret_513 (a_552: loaded integer) : loaded integer := + ... + end