{"id":"1d338e7b-13c1-4e18-ada6-e7500b711a08","arxiv_id":"2608.06705","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A hybrid of formal macro-translation rules and LLMs translates more C macros correctly than either approach alone.","lead":"This paper introduces MerC, a rule-based tool that translates C preprocessor macros into equivalent C variables, enums, or functions without inlining them, plus a new benchmark called MacroBench for measuring macro translation. It finds that running MerC first and letting large language models handle the remaining macros cuts failure rates by about a third compared to LLMs alone while translating far more than MerC alone.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Rule I's 'static const type name' output changes pointer types for pointer-typed constants, so MerC's formalism does not preserve callsite types and the universal correctness guarantee is not established.","rationale":"The reader's weakest_assumption was that MerC's correctness inherits from Maki's unverified Boolean properties. That is a valid concern, but the more load-bearing vulnerability is Rule I itself: the formal rule as printed in Figure 2 changes the type of any pointer-typed constant macro because `const` is placed before the type. This does not require doubting Maki; it is a direct, localized flaw in the paper's central formal contribution. The paper's empirical evidence is substantial: 198 MerC translations checked, 0 failures, whole-program compile/test on 23 projects, a public artifact, and a statistically sampled benchmark. However, those checks could miss pointer-typed constants because GCC's default diagnostic for const-discard is a warning, and the rule's premise set does not exclude pointer types. The correct fix is narrow (emit `static type const name` and/or restrict Rule I to non-pointer scalar types), so the paper's tag-team empirical conclusions may survive a revision, but the universal correctness guarantee cannot stand as written. Since the reader already assigned CONDITIONAL and noted the same const-placement issue in their rationale, my stress-test does not change the verdict.","tokens_in":22003,"tokens_out":9324,"duration_ms":77537,"concrete_test":"Build a one-file test case `#define NULLPTR ((void*)0)` plus `void *p = NULLPTR;` (or `#define STR \"hello\"` with `char *s = STR;`), run MerC on it, and compile the emitted C with `gcc -std=c11 -Werror=incompatible-pointer-types`. If MerC applies Rule I, the output declares `static const void *NULLPTR = ((void*)0);` (or `static const char *STR = \"hello\";`), and the initialization assigns a `const void *`/`const char *` to a `void *`/`char *`, producing a constraint violation; the test thus refutes the 'only correct translations' claim. Also confirm the rule's type change by writing out the declaration from Figure 2 with type `char *` and checking with the C standard that the declared type is `char const *`, not `char * const`.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Figure 2 Rule I concludes with `static const type name = body;` for any object-like macro whose invocation type γ is a single non-void type. If that type is a pointer type, the `const` qualifier binds to the pointed-to type, not to the variable. For example, a macro `#define STR \"hello\"` used as a `char *` expression yields `static const char *STR = \"hello\";`, whose type is `const char *`, not `char *`. The original macro's callsite `char *s = STR;` or `foo(STR)` with a `char *` parameter then violates C's type compatibility rules (C11 6.5.16.1), so the translation is not semantics- and callsite-preserving. No premise of Rule I excludes pointer types (only `type notin {void}` is required), and Rule II only handles integer constant expressions, so pointer-typed constants fall through to Rule I. This is a defect in MerC's own formal specification, independent of Maki's soundness: even with perfect Boolean properties, the rule's output changes the type of the translated name. Therefore the paper's strongest claim that 'MerC only produces correct translations' is not supported and, for pointer-typed constant macros, appears false. The whole-program evaluation (Section 6.2) reports all 23 programs compile and pass tests, which is real evidence, but it does not exercise the full space of pointer-typed constant macro usages that Rule I admits.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents MerC, a rule-based macro-to-C translator whose seven inference rules (Figure 2) convert object-like macros to global variables or enums and function-like macros to functions, using semantic Boolean properties computed by the Maki analyzer. It also introduces MacroBench, a statistically sampled benchmark of 398 macro test cases drawn from 23 real-world C programs, and compares MerC against three LLMs (GPT-4o, Claude 3.5 Sonnet, o1 Preview). The reported results are that MerC translates 50% of MacroBench with zero failures, LLMs translate 61-88% with 8-28% failure rates, and a MerC-first tag team lowers the average failure rate by 32% while increasing translations by 51% over MerC alone.","tokens_in":22266,"tokens_out":11426,"duration_ms":106363,"significance":"MacroBench and the empirical comparison are useful contributions: the benchmark was sampled independently of MerC, correctness labels were checked with GCC and by manual review, and whole-program compile/test results are reported for all 23 programs. The tag-team insight is actionable, since a fast rule-based front end reduces the number of LLM outputs that need hand validation. The formal rule set is not yet sound as written, however: at least two rules in Figure 2 admit macros whose translations change callsite types or are not strictly conforming C. The paper's strongest claim that MerC 'only produces correct translations' therefore needs repair before the headline results can be accepted as stated.","major_comments":[{"comment":"Rule I's conclusion `static const type name = body;` is incorrect when `type` is a pointer type. In C, `static const char *name` declares a pointer to const char, not a const pointer to char. For example, if `#define STR \"hello\"` is used at a callsite `char *s = STR;`, the original macro expansion is valid, but the translated declaration `static const char *STR = \"hello\";` makes `STR` have type `const char *`, so `char *s = STR;` violates C11 6.5.16.1 by discarding the `const` qualifier from the pointed-to type. Premise 12 only excludes `void`; no premise excludes pointer types, and pointer-valued constant expressions otherwise satisfy Rule I's premises. Thus the rule does not preserve callsite types for pointer-typed constant macros, and the Section 2.5 claim that MerC's rules guarantee correct translations is not supported. The rule needs a correct declarator form such as `static type const name = body;` (e.g., `static char *const STR = ...;`) or an added premise excluding pointer types.","section":"Section 2.3, Figure 2 (Rule I)"},{"comment":"Rule II's translation to `enum { name = body; }` is not strictly conforming C for all macros admitted by its premises. Premise 23 checks only `SizeOf(type) <= SizeOf(int)`, but C11 6.7.2.2 requires the expression defining an enumeration constant to have a value representable as an `int`. A macro such as `#define FLAG 0x80000000u` satisfies Premises 19, 22, and 23 (type `unsigned int`, integer constant expression, size 4 on a typical platform), yet `enum { FLAG = 0x80000000u };` is not strictly conforming C, and in C11 an enumeration constant has type `int`, changing `FLAG`'s type from `unsigned int`. Rule II needs a value-range premise or an explicit statement of the C dialect and compiler extensions it relies on.","section":"Section 2.4, Figure 2 (Rule II)"},{"comment":"The correctness argument treats Maki's Boolean properties in Table 1 as premises whose soundness is assumed. Section 2.5 cites only Maki's own 95-test suite as evidence for these properties, and no theorem relates each property to the C and preprocessor semantics it is supposed to capture. Because a false positive in any property, such as `CapturesEnvironment` or `IsConstExpr`, would make a rule fire on a macro whose translation changes behavior, the universal claim that MerC 'only produces correct translations' is stronger than the evidence provided. I would like a formal statement of what each predicate over-approximates or under-approximates, or an independent validation of the predicates against a manually labeled corpus of macro invocations.","section":"Section 2.5"}],"minor_comments":[{"comment":"The helper names contain typos: `AddressReqired`, `SizeReqired`, and `ConstExprReqired` should be spelled `AddressRequired`, `SizeRequired`, and `ConstExprRequired`.","section":"Table 1 and Figure 2"},{"comment":"The stacked-bar figures are hard to decode; the caption of Figure 5 should define explicitly, for each tool, how the three categories ('Correct formal translations', 'Hand-validated LLM translations', 'Incorrect LLM translations') relate to the totals for the 'Alone' and 'With MerC' conditions, and Figure 6 should state that MerC's 37 seconds is rounded to 1 minute.","section":"Figures 5 and 6"},{"comment":"The temperature settings are described only as the Copilot defaults; for reproducibility, the actual temperature values (or the exact Copilot versions whose defaults were used) should be reported.","section":"Section 5.2"},{"comment":"The statement that the tag team has an 'average failure rate 32% lower' should specify whether the reduction is relative or absolute, and should give the baseline average over which the 32% is computed, since the individual LLM failure rates vary from 8% to 28%.","section":"Section 5.6"},{"comment":"The description of recursive context inclusion is informal; a precise algorithm or a reference to the artifact's slicing code would make the benchmark construction fully reproducible.","section":"Section 4.2"}],"recommendation":"major_revision","confidential_remarks":"The paper is within scope for ASE and the benchmark is a valuable community resource. The empirical comparison is generally well conducted, but the formal correctness claim is load-bearing and is undermined by the Rule I pointer-type issue and the Rule II enumerator-value issue; both are fixable within the scope of a revision. I would also press the authors to either prove or independently validate the Maki predicates before claiming a guarantee. If these points are addressed, the paper could be acceptable."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: this is a genuinely useful paper for anyone working on C-to-Rust translation or macro refactoring. MacroBench is a real contribution, and the tag team idea is sensible. But the paper's headline guarantee—MerC only produces correct translations—doesn't hold as stated, because Rule I's output changes pointer types.\n\nWhat's new: MacroBench is the first benchmark aimed squarely at macro translation, sampled independently of MerC, and the LLM comparison plus tag team measure real things. The artifact is promised and the evaluation is careful: GCC checks, manual labeling by two people, and the whole-program compile/test results on 23 programs are solid evidence. The observation that LLMs over-translate and need validation, while a rule-based tool can handle the easy half, is worth publishing.\n\nWhere it gets soft: The stress-test note is right. Rule I concludes `static const type name = body;`. If `type` is a pointer type, the `const` binds to the pointed-to type, not the variable. A macro like `#define STR \"hello\"` used as a `char *` expression becomes `static const char *STR`, which is `const char *`. Any callsite assigning it to `char *` is a constraint violation. Nothing in Rule I's premises excludes pointer types. So the formal claim that substituting the definition preserves callsite syntax and behavior is false for those cases. The whole-program evaluation may not have exercised that pattern, but the rule admits it.\n\nAlso worth flagging: correctness rides on Maki's Boolean properties, which are validated only by a 95-test suite from the same group. That's not fatal—the benchmark is independent and the compile/test results are real evidence—but the paper should present the rule correctness as 'we have strong evidence' rather than 'guarantee'.\n\nBottom line: the paper deserves a serious referee. The benchmark and the tag team result are valuable, and the flaw in Rule I is fixable (add a premise excluding pointer types, or adjust the const placement and re-run the eval). As it stands, the universal correctness claim should be softened.\n\nRecommendation: engage it, but require the rule fix before acceptance.","headline":"Useful benchmark and tag-team evaluation, but Rule I's const placement breaks pointer types and the universal correctness claim is not established.","tokens_in":22817,"tokens_out":2367,"would_cite":true,"duration_ms":21469,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Formal translation rules and LLMs translate more C macros as a tag team than either does alone.","keywords":["C preprocessor macros","macro translation","formal inference rules","large language models","program translation","C to Rust","benchmark","semantic analysis"],"falsifier":"Compile and run, with identical inputs, the original and MerC-translated versions of every MacroBench case and compare behavior, memory layout, and preprocessor conditionals; a single translated macro that behaves differently, or a single macro satisfying all premises of one rule in Figure 2 that MerC refuses to translate or translates incorrectly, would refute the claim that MerC only produces correct translations.","tokens_in":21774,"feed_emoji":"🧩","tokens_out":8394,"duration_ms":70686,"temperature":0.7,"pith_summary":"This paper tries to show that C preprocessor macros can be translated into ordinary C variables, enums, and functions without changing their call sites, and that this step is what makes macro-heavy C code translatable without losing its abstractions. It claims MerC, a rule-based translator built from seven formal inference rules, never emits an incorrect translation, but only covers half of a new 398-case benchmark, MacroBench, sampled from real programs. It claims the large language models it tested translate more macros but make mistakes on 8% to 28% of attempts, forcing manual validation of every output. The central result is a two-stage tag team: run MerC first, then let an LLM handle the remainder, which lowers the average failure rate by 32% compared with LLMs alone while translating 51% more cases than MerC alone. If correct, this gives a practical recipe for preserving macro abstractions during C-to-Rust translation instead of losing them to preprocessing.","feed_headline":"Rules first, LLMs second: 32% fewer failed macro translations","feed_subtitle":"A zero-error rule translator covers half of macro cases; adding an LLM for the rest lifts coverage by 51%.","key_machinery":"The central mechanism is a six-way Venn diagram of the semantics shared by macros and C constructs, formalized as seven inference rules in Figure 2. Each rule names premises phrased as Boolean properties, such as defined globally, no environment capture, no metaprogramming, no address-of or sizeof use, no compile-time-constant requirement, and monomorphic non-void type, and a conclusion that rewrites the macro definition to a static const variable, enum, static inline function, or void function while leaving every call site unchanged. The premises are evaluated by a macro analyzer from prior work that computes these Boolean properties for every abstract-syntax-tree-aligned macro invocation. Because every invocation must satisfy every premise, at most one rule applies to a macro and unsupported macros are left untranslated, which is what underpins the claim that MerC only produces correct translations.","core_discovery":"On its own terms, the paper's central discovery is that macros can be classified by which C-language semantics they already obey, and that this classification yields a sound translator. MerC's seven rules convert object-like macros to global variables or enums and function-like macros to inline or void functions, but only when the macro is globally defined, does not capture surrounding identifiers, does no token manipulation, is not used with address-of or sizeof, is not required to be a compile-time constant, and has one consistent type. On MacroBench's 398 randomly sampled, statistically significant test cases, MerC translated 50% with zero failures, while three widely used LLMs translated more but failed on 8% to 28% of their attempts. Running MerC first and then asking an LLM to translate only the remaining macros cut the average failure rate by 32% relative to using an LLM alone and increased translations by 51% relative to MerC alone, with about 66% fewer LLM translations requiring hand-validation. The paper also reports that on 23 whole programs, MerC translated 8,211 of 100,711 macro invocations and all programs still compiled and passed their test suites.","pith_inferences":["Editorial extension: A direct test of the rules' completeness would run MerC to a fixpoint on the 23 whole programs, peeling nested macros, and measure how far the 8% translation rate rises; the paper notes this is possible but does not quantify it.","Editorial extension: The 30 macros no tool translated are mostly token-pasting or metaprogramming macros, so a targeted rule or prompt for those patterns would close most of the remaining gap without weakening MerC's conservative premises.","Editorial extension: The tag-team division, a sound narrow tool first and an unsound broad tool on the residue, is a general recipe for other code-translation tasks; the paper's measured 32% failure-rate reduction quantifies the benefit in this setting.","Editorial extension: Because MacroBench ships per-macro single files, the same evaluation can be rerun as LLMs improve, making the paper's LLM-versus-MerC comparison a moving baseline rather than a fixed result."],"forward_implications":["For the roughly half of macros MerC supports, developers can translate them with zero manual validation, because MerC produced no incorrect translations across MacroBench.","Tag teams using MerC first cut the number of LLM translations needing hand-validation by about 66% on average compared with delegating all macros to an LLM.","Because MerC preserves call-site syntax, downstream C-to-Rust translators can convert MerC's inline functions into Rust inline functions or macros, preserving both abstraction and performance.","On whole programs, MerC translated 8,211 of 100,711 macro invocations across 23 programs and all programs still compiled and passed their test suites, suggesting the zero-failure result is not limited to the benchmark.","Few-shot and chain-of-thought prompting reduced failures for the reasoning-focused LLM but also made it skip more cases, so prompting alone does not close the gap the tag team addresses."],"supporting_citations":[{"why":"Supplies the semantic Boolean properties, defined globally, environment capture, call-by-name, constant-expression status, that every MerC rule premise reads.","marker":"[54]"},{"why":"Provides the empirical distribution of macro usage and the real-world program corpus from which MacroBench's stratified sample is drawn.","marker":"[16]"},{"why":"Earlier rule-based macro-to-C translator limited to variable-like macros; MerC's function-like rules extend this line of work.","marker":"[45]"},{"why":"The macro analyzer's own 95-test suite is the evidence offered for the correctness of the properties MerC inherits.","marker":"[55]"},{"why":"Example of a rule-based IDE refactoring that ignores invocation semantics and produces wrong results, motivating MerC's semantic premises.","marker":"[57]"},{"why":"Measures LLM code-translation bug rates, providing the comparison baseline for the paper's LLM failure-rate results.","marker":"[52]"},{"why":"Infers types of macro invocations, underlying the type-monomorphism checks in MerC's rules.","marker":"[14]"}],"fun_headline_variants":["Rules first, LLMs second: 32% fewer failed translations","Tag-teaming rules and LLMs cuts macro translation failures by 32%","Zero-error rule translator covers half; LLM handles the rest","MerC rules + LLM: 51% more macros, 32% fewer failures","Formal macro rules first, then ask LLMs for leftovers"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the semantic properties supplied by the pre-existing macro analyzer are complete and correct; those properties are validated only by the analyzer's own 95-test suite, so if a property is wrong for some invocation, MerC's promise of zero incorrect translations fails.","fun_headline_variants_meta":{"raw":{"variants":["Rules first, LLMs second: 32% fewer failed translations","Tag-teaming rules and LLMs cuts macro translation failures by 32%","Zero-error rule translator covers half; LLM handles the rest","MerC rules + LLM: 51% more macros, 32% fewer failures","Formal macro rules first, then ask LLMs for leftovers"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000251,"raw_usage":{"total_tokens":1625,"prompt_tokens":1079,"completion_tokens":546,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":695,"completion_tokens_details":{"reasoning_tokens":450}},"tokens_in":695,"tokens_out":546,"duration_ms":5176,"temperature":1.0,"reasoning_tokens":450,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T04:13:53.200781+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Compile and run, with identical inputs, the original and MerC-translated versions of every MacroBench case and compare behavior, memory layout, and preprocessor conditionals; a single translated macro that behaves differently, or a single macro satisfying all premises of one rule in Figure 2 that MerC refuses to translate or translates incorrectly, would refute the claim that MerC only produces correct translations.","supporting_citations":[{"cited_title":"Mennie and Charles L","cited_arxiv_id":null,"evidence_quote":"Earlier rule-based macro-to-C translator limited to variable-like macros; MerC's function-like rules extend this line of work."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The macro analyzer's own 95-test suite is the evidence offered for the correctness of the properties MerC inherits."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Example of a rule-based IDE refactoring that ignores invocation semantics and produces wrong results, motivating MerC's semantic premises."},{"cited_title":"2021.CppSig: Extracting Type Information for C-Preprocessor Macro Expansions","cited_arxiv_id":null,"evidence_quote":"Infers types of macro invocations, underlying the type-monomorphism checks in MerC's rules."}],"review_version":2}