[acl2/acl2] 375d52: [C$] Remove local theorem no longer needed.

[Alessandro Coglio]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 375d525b7577356e87e38d15937da345987f62d5
https://github.com/acl2/acl2/commit/375d525b7577356e87e38d15937da345987f62d5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-05 (Thu, 05 Feb 2026)

Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp

Log Message:
-----------
[C$] Remove local theorem no longer needed.


Commit: 7666f70fabf7392672445242fc2f70190b3960ff
https://github.com/acl2/acl2/commit/7666f70fabf7392672445242fc2f70190b3960ff
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-05 (Thu, 05 Feb 2026)

Changed paths:
M books/kestrel/c/syntax/macro-tables.lisp
M books/kestrel/c/syntax/preprocessor.lisp

Log Message:
-----------
[C$] Have macro lookup return 'reach'.

This will support a more nuanced way to check for self-contained files.


Commit: 7b3247e04871dc472d4aa23174a325d368709f62
https://github.com/acl2/acl2/commit/7b3247e04871dc472d4aa23174a325d368709f62
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-05 (Thu, 05 Feb 2026)

Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp

Log Message:
-----------
[C$] Track maximum macro reach during preprocessing.


Commit: ad2b433146a23999ad649b504efdcf35ae97ce5b
https://github.com/acl2/acl2/commit/ad2b433146a23999ad649b504efdcf35ae97ce5b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-05 (Thu, 05 Feb 2026)

Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp

Log Message:
-----------
[C$] Return max macro reach from `pproc-file`.


Commit: 3c3902a351fe33e7bebad3ef30501a5d5e02a701
https://github.com/acl2/acl2/commit/3c3902a351fe33e7bebad3ef30501a5d5e02a701
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-05 (Thu, 05 Feb 2026)

Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp

Log Message:
-----------
[C$] Improve and simplify preprocessor.

Eliminate the `not-self-contained-p` flag, using the max reach instead. Also, do
not treat max reach > 0 as an exception, but instead continue preprocessing the
file.


Commit: 3924a355b89b6b66167c564ac54c3b6d3b15088a
https://github.com/acl2/acl2/commit/3924a355b89b6b66167c564ac54c3b6d3b15088a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-05 (Thu, 05 Feb 2026)

Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp

Log Message:
-----------
[C$] Improve handling of non-self-contained files.

Instead of adding the bytes of the included file to the stobj, use directly
the lexemes coming from the attempt to preprocess the file as self-contained,
which would be the same lexemes anyhow.

Although the C standard is not super-clear about the level at which included
files are expanded in place (byte level, character level, or lexical level), the
syntax of the `#include` directive suggests that the lexical level is the right
one. In some contrived cases, Clang and GCC exhibit some strange (and not
mutually consistent) behaviors that do not quite match that interpretation, but
that still seems the right interpretation.


Commit: b407e741815b821326c6cacd1097c5632d29ae05
https://github.com/acl2/acl2/commit/b407e741815b821326c6cacd1097c5632d29ae05
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-05 (Thu, 05 Feb 2026)

Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp

Log Message:
-----------
[C$] Streamline some preprocessor code.

Have `pproc-file` return a (reversed) list of lexemes and a macro scope, not
packaged into an `scfile`, and do not extend the `preprocessed` alist there.
Let the callers do all of that, if the file is self-contained; if it is not,
the lexemes and macros are used in a different way.


Commit: 712aeecaa6c75c47be2f4992d1e6e56353f0a797
https://github.com/acl2/acl2/commit/712aeecaa6c75c47be2f4992d1e6e56353f0a797
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-05 (Thu, 05 Feb 2026)

Changed paths:
M books/kestrel/c/syntax/implementation-environments.lisp
M books/kestrel/c/syntax/macro-tables.lisp
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/preprocessor-evaluator.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor.lisp

Log Message:
-----------
[C$] Use logical integer fixer in executable code.


Commit: e597f9881ae630e61ef891c75f4ba8f210ca0738
https://github.com/acl2/acl2/commit/e597f9881ae630e61ef891c75f4ba8f210ca0738
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-05 (Thu, 05 Feb 2026)

Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor.lisp

Log Message:
-----------
[C$] Simplify a data structure.

We do not need to have a `macros` component in `scfile`, after some code changes
we have made.


Commit: d2512b28f7657b7f9a4e8e655ab3119cad637b29
https://github.com/acl2/acl2/commit/d2512b28f7657b7f9a4e8e655ab3119cad637b29
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-05 (Thu, 05 Feb 2026)

Changed paths:
M books/kestrel/arm/instructions.lisp
M books/kestrel/arm/package.lsp
M books/kestrel/arm/step.lisp
M books/kestrel/axe/def-simplified.lisp
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/jvm/lifter2.lisp
M books/kestrel/axe/jvm/unroller.lisp
M books/kestrel/axe/jvm/unroller2.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/risc-v/assumptions.lisp
M books/kestrel/axe/risc-v/support-non-axe.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/unroll-spec-basic.lisp
M books/kestrel/axe/unroll-spec.lisp
M books/kestrel/axe/x86/examples/factorial/factorial-elf64.lisp
M books/kestrel/axe/x86/examples/factorial/factorial-macho64.lisp
M books/kestrel/axe/x86/examples/popcount/popcount-32-proof.lisp
M books/kestrel/axe/x86/examples/popcount/popcount-64-proof.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/tester.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/add-section-attr-doc.lisp
A books/kestrel/c/transformation/command-line/tests/add-section-attr.json
A books/kestrel/c/transformation/command-line/tests/add-section-attr2.json
A books/kestrel/c/transformation/command-line/tests/input-files/file10.c
A books/kestrel/c/transformation/command-line/tests/input-files/file11.c
A books/kestrel/c/transformation/command-line/tests/input-files/file9.c
M books/kestrel/c/transformation/command-line/tests/run-tests.sh
M books/kestrel/c/transformation/command-line/wrappers.lisp
M books/kestrel/c/transformation/simpadd0-doc.lisp
M books/kestrel/c/transformation/tests/add-section-attr/add-section-attr.lisp
A books/kestrel/executable-parsers/.sys/elf-...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/mach-o...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-e...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-ex...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-ma...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parsed-exec...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parser...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/pe-t...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/t...@useless-runes.lsp
A books/kestrel/executable-parsers/elf-tools.lisp
A books/kestrel/executable-parsers/mach-o-tools.lisp
A books/kestrel/executable-parsers/parse-elf-file.lisp
A books/kestrel/executable-parsers/parse-executable.lisp
A books/kestrel/executable-parsers/parse-mach-o-file.lisp
A books/kestrel/executable-parsers/parse-pe-file.lisp
A books/kestrel/executable-parsers/parsed-executable-tools.lisp
A books/kestrel/executable-parsers/parser-utils.lisp
A books/kestrel/executable-parsers/pe-tools.lisp
A books/kestrel/executable-parsers/top.lisp
M books/kestrel/json-parser/parsed-json.lisp
A books/kestrel/lists-light/set-difference-equal-fast.lisp
M books/kestrel/lists-light/top.lisp
M books/kestrel/top.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/assumptions32.lisp
M books/kestrel/x86/assumptions64.lisp
R books/kestrel/x86/parsers/.sys/elf-...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/mach-o...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-e...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-ex...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-ma...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parsed-exec...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parser...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/pe-t...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/t...@useless-runes.lsp
R books/kestrel/x86/parsers/elf-tools.lisp
R books/kestrel/x86/parsers/mach-o-tools.lisp
R books/kestrel/x86/parsers/parse-elf-file.lisp
R books/kestrel/x86/parsers/parse-executable.lisp
R books/kestrel/x86/parsers/parse-mach-o-file.lisp
R books/kestrel/x86/parsers/parse-pe-file.lisp
R books/kestrel/x86/parsers/parsed-executable-tools.lisp
R books/kestrel/x86/parsers/parser-utils.lisp
R books/kestrel/x86/parsers/pe-tools.lisp
R books/kestrel/x86/parsers/top.lisp
M books/kestrel/x86/tools/unroll-x86-code-old.lisp
M books/kestrel/x86/top.lisp

Log Message:
-----------
Merge.


Commit: ade645ebcea7e92a7819ec13d22179ffacf22a71
https://github.com/acl2/acl2/commit/ade645ebcea7e92a7819ec13d22179ffacf22a71
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-05 (Thu, 05 Feb 2026)

Changed paths:
A books/kestrel/c/syntax/tests/gincluder.c
A books/kestrel/c/syntax/tests/gincluder1.h
A books/kestrel/c/syntax/tests/gincluder2.h
A books/kestrel/c/syntax/tests/guarded.h
M books/kestrel/c/syntax/tests/preprocessor.lisp

Log Message:
-----------
[C$] Add a preprocessor test with header guards.

Not quite doing what we want just yet, but getting there.


Commit: 8c7f09bd438f3aca2e9e2c516993f4ace993e59a
https://github.com/acl2/acl2/commit/8c7f09bd438f3aca2e9e2c516993f4ace993e59a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-05 (Thu, 05 Feb 2026)

Changed paths:
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/preprocessor-reader.lisp

Log Message:
-----------
[C$] Simplify preprocessor stobj.

Now that we are handling included file expansion (when not self-contained) at
the lexical level, we no longer need the array of byte sequences.


Commit: 41dd9ee939c5cfdd2ba7606f4307752088fc7451
https://github.com/acl2/acl2/commit/41dd9ee939c5cfdd2ba7606f4307752088fc7451
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-05 (Thu, 05 Feb 2026)

Changed paths:
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/lifter-common.lisp
M books/kestrel/axe/risc-v/rule-lists.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/rule-limits.lisp
M books/kestrel/axe/step-increments.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/executable-parsers/elf-tools.lisp

Log Message:
-----------
Merge.


Compare: https://github.com/acl2/acl2/compare/f1282125f266...41dd9ee939c5

To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications

[Alessandro Coglio]

Branch: refs/heads/testing

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel