Skip to content

Fix Failure("nth") crash in remove_unused_parameters #678

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
elefthei wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Fix Failure("nth") crash in remove_unused_parameters #678

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
1d8e0b7
Fix Failure("nth") crash in remove_unused_parameters
Feb 11, 2026
a4caa58
Add regression test for Failure("nth") crash in remove_unused_parameters
Feb 18, 2026
826444e
Merge branch 'master' into fix/nth-crash-unused-params
elefthei Feb 18, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion lib/Simplify.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -233,7 +233,7 @@ let unused private_count_table lid ts (i: int) =
snd (List.nth l i) = Mark.AtMost 0
) ||
(* Second case: it's a unit, so here type-based elimination *)
List.nth ts i = TUnit
i < List.length ts && List.nth ts i = TUnit
in
unused_i i &&
implies (i = 0) (List.exists not (List.init (List.length ts) unused_i))
Expand Down
7 changes: 6 additions & 1 deletion test/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,7 +85,7 @@ FSTAR = $(FSTAR_EXE) \
--trivial_pre_for_unannotated_effectful_fns false \
--cmi --warn_error -274

all: $(FILES) rust $(WASM_FILES) $(CUSTOM) ctypes-test sepcomp-test rust-val-test bundle-test rust-propererasure-bundle-test
all: $(FILES) rust $(WASM_FILES) $(CUSTOM) ctypes-test sepcomp-test rust-val-test bundle-test json-test rust-propererasure-bundle-test

# Needs node
wasm: $(WASM_FILES)
Expand Down Expand Up @@ -269,6 +269,7 @@ check-ignore: $(OUTPUT_DIR)/KrmlTrue.exe

clean:
rm -rf $(WEB_DIR) .output
+$(MAKE) -C json clean

distclean: clean
rm -rf .cache
Expand Down Expand Up @@ -299,6 +300,10 @@ rust-val-test:
+$(MAKE) -C rust-val
.PHONY: rust-val-test

json-test:
+$(MAKE) -C json
.PHONY: json-test

rust-propererasure-bundle-test:
+$(MAKE) -C rust-propererasure-bundle
.PHONY: rust-propererasure-bundle-test
Expand Down
29 changes: 29 additions & 0 deletions test/json/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
include ../../Makefile.common

KRML_BIN = ../../_build/default/src/Karamel.exe
KRML = $(KRML_BIN)

OUTPUT_DIR = .output

JSON_FILES = $(wildcard *.json)
TESTS = $(patsubst %.json,%.test,$(JSON_FILES))

all: $(TESTS)

.PRECIOUS: $(OUTPUT_DIR)/%.exe
$(OUTPUT_DIR)/%.exe: %.json $(KRML_BIN) | $(OUTPUT_DIR)
$(call run-with-log, \
$(KRML) -tmpdir $(subst .exe,.out,$@) -no-prefix $* \
-o $@ $< \
,[JSON_KRML] $*,$(OUTPUT_DIR)/$*)

$(OUTPUT_DIR):
mkdir -p $@

%.test: $(OUTPUT_DIR)/%.exe
@$^ && echo -e "\033[01;32m✔\033[00m [JSON_TEST,$*]" || (echo -e "\033[01;31m✘\033[00m [JSON_TEST,$*]" && false)

clean:
rm -rf $(OUTPUT_DIR)

.PHONY: all clean
75 changes: 75 additions & 0 deletions test/json/NthCrash.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,75 @@
[
31,
[
[
"NthCrash",
[
[
"DExternal2",
[
null,
[],
[
[
"NthCrash"
],
"callee"
],
[
"TArrow",
[
[
"TInt",
[
"UInt32"
]
],
[
"TInt",
[
"UInt32"
]
]
]
],
[
"x",
"ghost_perm",
"ghost_seq"
]
]
],
[
"DFunction",
[
null,
[],
0,
[
"TInt",
[
"Int32"
]
],
[
[
"NthCrash"
],
"main"
],
[],
[
"EConstant",
[
[
"Int32"
],
"0"
]
]
]
]
]
]
]
]
Loading