From c6dc95e08163e9324839c21e11e957402b5a70cf Mon Sep 17 00:00:00 2001 From: Marcin Benke Date: Fri, 19 Jun 2026 15:38:19 +0200 Subject: [PATCH] Comptime strings: materialize string literals into memory(string) `string` is a comptime-only type with no runtime representation. String literals and comptime concatenations are now polymorphic via a primitive `Str` class and are materialized into `memory(string)` at runtime sites, mirroring the comptime `integer`/`Int.fromInteger` design. - StrLiteralDesugar: untyped pre-typecheck pass wrapping every string literal and every `concatLit(...)` in `Str.fromString(...)`, resolved by the type checker per use site (identity at `string`, materialization at `memory(string)`). Wrapping `concatLit` makes it effectively result-polymorphic, so `concatLit(...)` (incl. nested) works at a `memory(string)` site without a manual `Str.fromString`. - Primitives/TcEnv/NameResolution: `Str` class with bodyless `string` and `memory(string)` instances; `memStringFromLit` backend marker. - Specialise: `Str.fromString` resolves by result type to identity or `memStringFromLit`. - MastEval: `Str.fromString` identity fold; `memStringFromLit` kept impure. - EmitHull: intercept `memStringFromLit [StrLit]` -> per-literal, content- deduped `__strlit_` allocator (alloc + length + char words); clean guards when a comptime-only type reaches emission. - TcStmt: generalize markIntegerComptime -> markComptimeOnly (integer+string). - ComptimeCheck: classify comptime-only-typed params/returns as comptime, so `concatLit` and string functions are implicitly comptime without cascading the annotation to callers. Tests: comptime materialization (basic, concat, nested, dedup, negative) and an end-to-end dispatch case returning "Hello, world!" verified via evmone. Documented in doc/comptime-string.md. Assisted-By: Claude Opus 4.8 --- doc/comptime-string.md | 616 ++++++++++++++++++ run_contests.sh | 1 + sol-core.cabal | 1 + src/Solcore/Backend/EmitHull.hs | 111 +++- src/Solcore/Backend/MastEval.hs | 6 +- src/Solcore/Backend/Specialise.hs | 10 + src/Solcore/Desugarer/StrLiteralDesugar.hs | 32 + src/Solcore/Frontend/ComptimeCheck.hs | 26 +- src/Solcore/Frontend/Syntax/NameResolution.hs | 5 +- src/Solcore/Frontend/TypeInference/TcEnv.hs | 17 +- .../Frontend/TypeInference/TcSimplify.hs | 6 +- src/Solcore/Frontend/TypeInference/TcStmt.hs | 18 +- src/Solcore/Pipeline/SolcorePipeline.hs | 9 +- src/Solcore/Primitives/Primitives.hs | 43 ++ test/Cases.hs | 7 +- test/examples/comptime/string-concat-mem.solc | 29 + test/examples/comptime/string-lit-dedup.solc | 15 + test/examples/comptime/string-lit-mem.solc | 14 + .../comptime/string-mem-runtime-fail.solc | 13 + test/examples/dispatch/stringlit.json | 39 ++ test/examples/dispatch/stringlit.solc | 26 + 21 files changed, 1012 insertions(+), 32 deletions(-) create mode 100644 doc/comptime-string.md create mode 100644 src/Solcore/Desugarer/StrLiteralDesugar.hs create mode 100644 test/examples/comptime/string-concat-mem.solc create mode 100644 test/examples/comptime/string-lit-dedup.solc create mode 100644 test/examples/comptime/string-lit-mem.solc create mode 100644 test/examples/comptime/string-mem-runtime-fail.solc create mode 100644 test/examples/dispatch/stringlit.json create mode 100644 test/examples/dispatch/stringlit.solc diff --git a/doc/comptime-string.md b/doc/comptime-string.md new file mode 100644 index 000000000..11a62dc73 --- /dev/null +++ b/doc/comptime-string.md @@ -0,0 +1,616 @@ +# Comptime String Type: Design and Plan + +> **Status: implemented.** Steps 1–6 below are done; all 712 tests pass, +> including the four new `string-*` tests. Line citations point at the +> post-merge source. + +## Overview + +`string` is a compile-time-only type for string literals and exact +compile-time string manipulation. It mirrors the design of the comptime +[`integer`](comptime-integer.md) type: bare string literals are universally +polymorphic — they desugar to `Str.fromString(s)` calls and are resolved to the +appropriate concrete representation at each use site. + +The crucial difference from `integer` is the runtime story. An `integer` +literal converts to its runtime form (`word`) by a **pure comptime fold** +(`wordFromInteger` masks an `Integer`, both sides live in `IntLit`). A `string` +has **no on-stack runtime form at all** — at runtime a string is an empty type. +To be usable at runtime it must be *materialized* into memory as a +`memory(string)`: a length word followed by the character bytes, padded to +32-byte slots. Materialization is therefore runtime **code generation**, not a +fold, and is the one genuinely new mechanism this design adds over the integer +work. + +### Mental model (read this first) + +- A `string` value exists **only at compile time**. String literals and the + results of comptime ops (`concatLit`, …) are `string`. +- To use a string at runtime you must **explicitly convert** it to a runtime + representation with `Str.fromString`. The only such representation in this + first cut is `memory(string)`. +- There is **no implicit coercion**. `let s : string = …; return s;` where the + function returns `memory(string)` is a **type error** — exactly as `integer` + requires an explicit `wordFromInteger` rather than auto-coercing a variable. + Write `return Str.fromString(s);`. +- The conversion's argument must fold to a literal **in the scope where + `Str.fromString` is applied** (see [Materialization](#materialization-in-emithull) + for why a `string`-taking helper function does not work without inlining). + +### What already exists + +- `string = TyCon "string" []` (`Primitives.hs`). +- `tcLit (StrLit _) = string` (`TcStmt.hs:308`), + `typeOfTcExp (Lit (StrLit _)) = string` (`Specialise.hs:642`). +- `EmitHull.emitLit (StrLit _) = error "String literals not supported yet"` + (`EmitHull.hs:220`) — so `string` is *already* de-facto comptime-only: a bare + literal cannot reach runtime. It only survives by being folded away or + consumed by a special case. +- Comptime folding already works: `concatLit`/`strlenLit`/`keccakLit` are + `std.solc` stubs that MastEval folds when their arguments are concrete + `StrLit` (`MastEval.hs:435-446`). So string ops compose at compile time and + collapse to a single `StrLit`. +- The runtime representation `memory(string)` exists: `data memory(t) = + memory(word)` (`std.solc:752`), a `Typedef` over a pointer. `strlen` reads + `mload(ptr)` (`std.solc:818`); ABIEncode/ABIDecode/CanStore all operate on + `memory(string)`. +- The `revertLit` special case (`EmitHull.hs:285`) already turns + `MastCall revertLit [StrLit s]` into a Hull `SRevert s` — the precedent the + materializer follows. + +### What is missing + +There is no way to take a comptime `string` (a literal, or the folded result of +`concatLit`) and materialize it into a runtime `memory(string)`. That is the +whole job of this work. + +--- + +## The `Str` class + +Direct analog of the primitive `Int` class. Registered in `Primitives.hs` and +`TcEnv.hs`, the name reserved in `NameResolution.emptyEnv`. + +``` +class a : Str { fromString : string -> a } +instance string : Str -- fromString = identity (comptime) +instance memory(string) : Str -- fromString = memStringFromLit (runtime materialization) +``` + +Because `fromString : string -> a` resolves by **result type**, each runtime +representation gets its own materialization strategy through its own instance, +with no change to the others. This is the extension point for the data-section +form (below). + +Each non-identity instance maps to a distinct primitive name that the backend +intercepts: + +| Instance | `fromString` resolves to | Backend handling | +|---|---|---| +| `string : Str` | identity | literal survives as comptime `StrLit` | +| `memory(string) : Str` | `memStringFromLit : string -> memory(string)` | EmitHull: inline `mstore` materializer | +| `code(string) : Str` *(future)* | `codeStringFromLit : string -> code(string)` | EmitHull: Yul `data` section + `codecopy` | + +`Str` is a reserved primitive class name; user programs cannot redefine it. + +Note that `memory(string)` is a **compound** instance head +(`TyCon "memory" [TyCon "string" []]`), unlike the nullary `word`/`integer` +heads of the `Int` instances; instance selection unifies `a := memory(string)`. +This is a slightly richer instance than the integer precedent, not a literal +copy. + +### Instance registration (correctness-critical) + +Both instances are registered as **bodyless heads** in `primInstEnv` +(`TcEnv.hs:205`), exactly like the `Int` instances +(`[] :=> InCls intClassName word []`): + +```haskell +( strClassName, + [ [] :=> InCls strClassName string [], + [] :=> InCls strClassName (TyCon (Name "memory") [string]) [] + ] ) +``` + +They exist **only to satisfy constraint solving** during type checking. The +actual rewrite happens in the dedicated `specCall` case (below), which keeps the +*original argument expression in place*. + +It is tempting to instead write `instance memory(string):Str { function +fromString(s) { return memStringFromLit(s); } }` in `std.solc`. **Do not** — it +reintroduces the function-boundary problem: inside the instance method `s` is a +runtime parameter, so the body specializes to `memStringFromLit(s_param)` with +`s_param` a `MastVar`, never a `StrLit`, and EmitHull's intercept (which matches +`[MastLit (StrLit _)]`) never fires. The dedicated `specCall` rewrite avoids +this precisely because it operates on the call site's own arguments, where the +literal is still present. This is the same reason the `Int` instances are +bodyless and handled in `specCall`. + +`Str` is registered in `primClassEnv` as a one-method class info (mirror +`intInfo` at `TcEnv.hs:230`), and `fromStringEntry` is added to `primCtx` +alongside `fromIntegerEntry` (`TcEnv.hs:176`). + +--- + +## Literals and the desugaring pass + +`Solcore.Desugarer.StrLiteralDesugar.desugarStrLiterals` (a clone of +`IntLiteralDesugar`) runs before type inference on the untyped AST and wraps, in +**expression position**, with `Str.fromString(…)` using SYB `everywhere`: + +- every `Lit (StrLit s)`, and +- every `concatLit(…)` call (matched by leaf name, so `std.concatLit` too). + +`tcLit (StrLit _)` continues to return `string` (the argument type inside the +call). The checker resolves each `Str.fromString(…)` against the expected type +at its site. + +| Source site | Expected type | Resolves to | +|---|---|---| +| `revertLit("msg")` | `string` (revertLit's param) | identity → `StrLit` survives; EmitHull `SRevert` fires | +| `f("x")` where `f : memory(string) -> …` | `memory(string)` | `memStringFromLit` → runtime alloc + store | +| `let s : string = "abcd"` | `string` | identity → comptime `StrLit` | +| `"a" + "b"` evaluated at `string` | `string` | identity on both operands → `concatLit` folds | +| `return concatLit("a","b")` from a `memory(string)` fn | `memory(string)` | wrapped `concatLit` → `memStringFromLit(concatLit …)` → materialize | + +Wrapping `concatLit` makes it effectively result-polymorphic +(`string -> string -> a [a:Str]`) **without** changing its declaration or adding +any type-checker coercion — it is the same untyped literal-wrapping mechanism. +So `let x : memory(string) = concatLit("a","b")` works directly (no manual +`Str.fromString`). Because `concatLit`'s parameters are `string`, a wrapped +`concatLit` used as an **argument** to another `concatLit` resolves to identity, +so nested concatenations (`concatLit(concatLit(a,b),c)`) collapse to one literal +and materialize once. `+` is *not* helped (it desugars to `Add.add` at the +surface; `concatLit` only appears inside `string:Add` after typing), so the +dedicated `concatLit` is the terse comptime-concat form; `+` still needs the +explicit `Str.fromString("a" + "b")`. + +Trade-off: an **unannotated** `let s = concatLit("a","b")` becomes ambiguous +(`a : Str`), exactly like `let s = "literal"` already is — resolvable later by a +defaulting rule. + +**Patterns are out of scope.** `PLit (StrLit _)` patterns are not handled by +this work. Matching a string literal against a `memory(string)` scrutinee is +runtime string comparison — a separate feature. (A future comptime-only form, +matching a `string` scrutinee against literal labels, could be added but is not +planned here.) `tcPat` keeps its existing behaviour; no new `StrLit` pattern +case is added. + +The `noDesugarCalls` validity check (`TcSimplify.hs`) skips `Str` constraints in +`checkEntails`/`hnfEntails`/`ambiguityCheck`, exactly as it skips `Int`. + +### `datasize`/`dataoffset` + +These Yul primops take a `string` that names a Yul *object* (not character +data): `datasize`/`dataoffset` typed `string -> word` (`Primitives.hs:336-337`). +After desugaring, `datasize("runtime")` becomes +`datasize(Str.fromString("runtime"))`, which resolves to the `string` identity +instance and folds back to `datasize(StrLit "runtime")` — the form the Yul +translator already expects. No special handling needed; mentioned only because +their argument is a name, not materializable data. + +--- + +## The comptime → runtime boundary + +Concatenation and other string ops live in the `string` (identity) domain; +MastEval folds them to a single `StrLit`; only the value passed to +`Str.fromString` at a runtime representation is materialized. + +### Worked example: `+` then materialize + +`+` on strings uses `instance string:Add` (`std.solc:934`), whose body is +`concatLit` — so this form requires `import std`. + +Source (function returns `memory(string)`): +```solidity +return Str.fromString("a" + "b"); +``` + +After `StrLiteralDesugar` (every literal wrapped): +``` +return Str.fromString( Add.add( Str.fromString("a"), Str.fromString("b") ) ); +``` + +Type resolution, outside-in: +1. The return expects `memory(string)`, so the **outer** `Str.fromString` + resolves at `memory(string)` → `memStringFromLit`. Its argument is forced to + `string`. +2. `Add.add` must therefore produce `string` → `instance string:Add`, forcing + both operands to `string`. +3. The **inner** `Str.fromString("a")` / `Str.fromString("b")` resolve at + `string` → identity. + +MastEval then folds: `concatLit("a","b") → StrLit "ab"`, leaving +`memStringFromLit(StrLit "ab")`, which EmitHull materializes. + +By the time `memStringFromLit` is reached its argument is always a concrete +`StrLit` — whether it came from source or from a comptime op. A `string` value +that is *not* statically known cannot reach runtime; that is the comptime-only +invariant (the same one `integer` relies on), enforced by the EmitHull guard +plus the `emitLit (StrLit _) = error` backstop. + +--- + +## Materialization in EmitHull + +Chosen home: **EmitHull**. It owns the object body, already has +`SFunction` + `SAssembly [YulStmt]` (`Hull.hs:58,64`), and follows the +`revertLit` intercept precedent. Materialization is runtime codegen from a +comptime value, which is EmitHull-shaped. + +### Why the argument must be a local literal + +EmitHull intercepts +`MastCall (MastId "memStringFromLit" _) [MastLit (StrLit s)]`. The argument has +to be a literal *at that point*. This holds when `Str.fromString` is applied to: + +- a literal directly (`Str.fromString("x")`), or +- a local `string` variable whose comptime `let` folds to a literal and is + substituted by dead-let elimination in the same function scope. + +It does **not** hold across a function boundary: a helper +`toMemory(s : string) { return Str.fromString(s); }` specializes to +`memStringFromLit(s_param)` with `s_param` a `MastVar`, never a `StrLit`. +`memStringFromLit` is impure, so MastEval will not inline the helper (unlike +pure helpers such as `Num.fromInteger`), and specialization is by type, not by +literal value. A readable `toMemory` helper would require an "always inline" +mechanism, which is out of scope. For now, apply `Str.fromString` directly +where the literal is in scope. + +### Mechanism (inline `mstore`, first cut) + +On intercept: + +1. Compute at compile time: `len = byteLength(s)` (UTF-8, matching the existing + `strlenLit` encoding in `MastEval.hs:437`), the char words `w0, w1, …` (each + 32 bytes, last right-padded with zero bytes), and + `total = 32 * (1 + ceil(len / 32))`. +2. Register one generated function **per distinct literal**, deduplicated by content + (a Map keyed on the literal; the suffix is an assigned index), named `__strlit_`. It is **self-contained** — it bumps + the free-memory pointer itself and calls nothing external (the materializer + is injected *after* specialization/tree-shaking, so it must not depend on + `allocate_memory` or other std functions, which may have been pruned): + + ``` + // emitted as a Hull SFunction; memory(string) is a Typedef over word, + // so at this level it is just a word (the pointer). + function __strlit_() -> word { + let p; + assembly { + p := mload(0x40) // free pointer + mstore(p, ) // length slot + mstore(add(p, 32), ) + mstore(add(p, 64), ) + // ... + mstore(0x40, add(p, )) // bump free pointer + } + return p; // the memory(string) representation + } + ``` + ``, ``, and `` are compile-time constants baked into the Yul. +3. Rewrite the call site to `ECall "__strlit_" []`. The surrounding + context already expects the `memory(string)` representation, which is exactly + this word pointer (`Typedef` is representationally identity). +4. Append the accumulated `SFunction`s to the emitted object. + +### Concrete Hull shape (verified mechanically sound) + +The generated function is built directly as Hull (`p` is a Hull local; the asm +references it by name): + +```haskell +Hull.SFunction "__strlit_" [] Hull.TWord + [ Hull.SAlloc "p" Hull.TWord + , Hull.SAssembly + [ YAssign ["p"] (YCall "mload" [YLit (YulNumber 0x40)]) + , YExp (YCall "mstore" [YIdent "p", YLit (YulNumber )]) + , YExp (YCall "mstore" [YCall "add" [YIdent "p", YLit (YulNumber 32)], YLit (YulNumber )]) + , YExp (YCall "mstore" [YCall "add" [YIdent "p", YLit (YulNumber 64)], YLit (YulNumber )]) + -- ... + , YExp (YCall "mstore" [YLit (YulNumber 0x40), YCall "add" [YIdent "p", YLit (YulNumber )]]) + ] + , Hull.SReturn (Hull.EVar "p") + ] +``` + +This is sound because `genStmt (SAssembly …)` substitutes Hull variable names +into the asm via `getVarEnv` (`yule/Translate.hs:109-156`): the `p` written by +`SAlloc` is rewritten to its real Yul name everywhere it appears in the block. +So there is **no** Hull-vs-Yul naming hazard, and no need to fall back to inline +emission. + +### EmitHull plumbing + +`EM = StateT EcState IO`. `EcState` gained `ecStrLits :: Map String String` +(`EmitHull.hs:39`), mapping literal content → generated function name, for +dedup. `registerStrLit` (the intercept in `emitExp`) looks the literal up, +reusing the name if present or assigning `"__strlit_" ++ show (Map.size m)`, and +returns `(Hull.ECall fn [], [])`. `emitContract` resets `ecStrLits` at entry, +builds `runtimeBody`, then reads `ecStrLits`, generates one `SFunction` per +entry, and **prepends** them to the object body (`Hull.Object cname (strLitFuns +++ runtimeBody) []`). + +Limitation (first cut): the generated allocators are emitted into the **runtime** +object only. A string literal used in constructor/deploy code would call an +allocator that lives in the runtime object — a separate Yul object — and not +resolve. String literals in constructor code are therefore not yet supported +(see gaps). + +Dedup-by-content means N identical literals share one function (a separate +function per *distinct* literal). + +### Length boundaries to cover + +- `len == 0` → one slot (length only), `total = 32`. +- `0 < len < 32` → two slots (length + one partial char word). +- `len == 32` → two slots (length + one full char word). +- `len > 32` → length + `ceil(len/32)` char words. + +### Future: data section via `code(string)` + +For large strings the inline `mstore` sequence bloats code. Solidity instead +places literal bytes in the contract's data section and `codecopy`s them into +memory on demand. The primops `datasize`/`dataoffset` and +`YulData`/`InnerData` (`Yul.hs:13-17`) already exist. + +This slots in additively as a new instance `code(string) : Str` → +`codeStringFromLit : string -> code(string)`, where `code(string)` is a handle +to bytes living in the data section. Its `fromString` registers a +`data "__strdata_" hex"…"` object and returns the handle; a conversion +(`code(string) -> memory(string)` via `codecopy`) materializes on demand. Full +semantics of `code(a)` are out of scope for the first cut; the design keeps the +strategy keyed on target type so this requires no change to `memory(string)`. + +--- + +## Specialization + +`Specialise.specCall` gains a dedicated `Str.fromString` case, parallel to the +existing `Int.fromInteger` case: + +- result type `string` → identity (keep the `StrLit`, drop the call). +- result type `memory(string)` → rewrite to `memStringFromLit` (intercepted by + EmitHull). + +Concretely, mirror the `Int.fromInteger` case at `Specialise.hs:395`: + +```haskell +specCall (Id (QualName (Name "Str") "fromString") ty) args _ = do + args' <- mapM (\a -> specExp a (typeOfTcExp a)) args + s <- getSpSubst + let resultTy = snd (splitTy (applytv s ty)) + if resultTy == memString -- TyCon "memory" [string] + then pure (Id (Name "memStringFromLit") (Prim.string :-> memString), args') + else pure (Id (QualName (Name "Str") "fromString") (Prim.string :-> resultTy), args') +``` + +This case must appear **before** the generic `comptimeBuiltins` guard +(`Specialise.hs:403`), exactly as the `Int` case does. + +### Purity bookkeeping (correctness-critical) + +The two `Str.fromString` outcomes have **opposite** purity: + +- The identity path keeps `QualName (Name "Str") "fromString"`. This name must + be a `builtinPureFun` **and** have a MastEval identity clause, so it folds and + is substituted away: + ```haskell + evalPrimitive (QualName (Name "Str") "fromString") [x] = Just x + ``` + (Mirror the existing `Int.fromInteger` identity clause, `MastEval.hs:462`.) + Add `QualName strClassName "fromString"` to the pure/comptime name lists (a + new `stringPrimNames`, or extend the existing list feeding `builtinPureFuns` + and `comptimeBuiltins`). +- `memStringFromLit` must be **excluded** from `builtinPureFuns` / + `comptimeBuiltins` and have **no** `evalPrimitive` clause — folding it would be + wrong (it has no comptime value; it emits code). It is consumed only by the + EmitHull intercept. + +Register `memStringFromLit : string -> memory(string)` as a primitive scheme in +`Primitives.hs` (so it is well-formed where referenced), but keep it out of the +pure lists. The existing `concatLit`/`strlenLit`/`keccakLit` folders are +unaffected. + +--- + +## Comptime-only enforcement + +`markIntegerComptime` was generalized to `markComptimeOnly` (`TcStmt.hs`), which +forces `comptime` on any `let` whose type is comptime-only (`integer` **or** +`string`). Such bindings are then folded and eliminated by MastEval before hull +emission, so a `string`-typed `let` never reaches `translateMastType`. + +The SAIL-level checker (`ComptimeCheck.hs`) likewise treats a **parameter or +return of comptime-only type as comptime** (`isComptimeOnlyTy` / `effRetComptime`): +a `string` value exists only at compile time, so `concatLit`/`strlenLit`/ +`keccakLit` — and any user function over `string` — are implicitly comptime +without annotation. This is the consistent fix: *explicitly* annotating +`concatLit` `comptime` would cascade (its caller `string:Add.add` passes its own +unannotated `string` params to it, which the checker would then reject); treating +all `string`/`integer` values as comptime by type avoids that, because those +caller params are implicitly comptime too. + +Backstops if a `string` value somehow survives: `emitLit (StrLit _) = error` +(`EmitHull.hs:220`) and `translateMastType` of `string` (an empty `data string;`) +fails with "empty sum string". These are crash-level guards, not the clean +per-construct messages the `integer` path has (`emitFunDef`/`translateParam`/ +`emitStmt` at `mastIntegerTy`); dedicated `string` guard messages are minor +future polish (see gaps). The `string-mem-runtime-fail` test shows the common +case (a `string` returned where `memory(string)` is expected) is caught earlier, +at type checking. + +## Interaction with `comptime` + +`comptime` is an **enforcement** annotation (handled by ComptimeCheck), not a +hint: it requires the binding be compile-time-evaluable and is a type error +otherwise. A plain binding merely *allows* folding and falls back to runtime. +Verified behaviour: + +| Binding | Result | +|---|---| +| `let a : word = x + 2` (runtime `x`) | ✅ compiles; runtime `addWord` | +| `let a : comptime word = x + 2` (runtime `x`) | ❌ *"comptime let 'a' is bound to a runtime expression"* | +| `let a : comptime word = 2 + 2` | ✅ folds to `4` | +| `let s : comptime string = "a" + "b"` | ✅ folds to `StrLit "ab"` | +| `let a : comptime memory(string) = "x"` | ❌ same "runtime expression" error | + +Two consequences specific to strings: + +- **`string` is implicitly comptime.** `markComptimeOnly` already forces + `comptime` on `string`-typed lets, so the annotation on + `let s : comptime string = …` is redundant (but legal). +- **`memory(string)` is a runtime type.** `comptime memory(string)` is rejected, + because materialization (`mload(0x40)` + `mstore`s) is runtime code. The + string's *content* is comptime (concatenation folds; the bytes are baked into + `__strlit_` as constants), but *placing* it in memory is runtime. + +### When does a `comptime string` materialize? + +**It does not — on its own.** `let s : comptime string = "Hello " + "world"` +binds a comptime value: `+` folds to `StrLit "Hello world"` and the comptime +`let` is eliminated by dead-let substitution. It emits **zero** runtime code (no +`__strlit_*`, no `mstore`). Materialization happens **only** where the string is +converted to a runtime representation — `Str.fromString(s)` at a `memory(string)` +site (which lowers to `memStringFromLit` → a `__strlit_` call). If `s` +instead flows to a comptime sink (`revertLit`, `strlenLit`, `keccakLit`, another +`concatLit`, …) it never touches memory. Each conversion site emits a runtime +call to the content-shared allocator, so the allocation runs **per use site, at +runtime**, not at the binding. + +The two axes are **orthogonal**: `comptime` controls *when* (enforced +compile-time vs opportunistic); the value's type controls *where the work +happens* (comptime `string`/`integer` domain vs runtime `memory(string)`/`word`). +`Str.fromString @ memory(string)` is precisely the point where comptime content +crosses into a runtime value — the dual of `Int.fromInteger @ word` for integers. + +## Usability: implicit conversion at runtime sites (proposed) + +Today a **bare** literal at a `memory(string)` site works +(`return "abcd";` → materialized), but a string built with a comptime **operation** +does not: + +```solidity +let a : memory(string) = "Hello, " + "world!"; // ERROR: no instance memory(string) : Add +``` + +After desugaring this is `Add.add(Str.fromString("Hello, "), Str.fromString("world!"))`, +and the `memory(string)` annotation forces `Add`'s result to `memory(string)`, +which has no `Add` instance. The user must wrap the whole expression: +`Str.fromString("Hello, " + "world!")`. (The numeric analog `let a : word = 2 + 2` +works only because `word : Add` exists; for `+`/`-`/`*` word arithmetic is +observationally equal to integer-then-truncate, so the missing "operate at the +comptime type, convert the result" is invisible there. Strings have no such +escape hatch — concatenation is not available at `memory(string)` at all.) + +**Proposed fix — expected-type-directed coercion (subsumption).** At an +ascription site (`let x : T = e`, `return e`, typed argument), if `e` naturally +has a comptime-only type `Tc` and the expected type `T` has a `T : Str` / `T : Int` +instance, wrap `e` in `Str.fromString` / `Int.fromInteger`. For +`"Hello, " + "world!"`, the result variable carries exactly `{:Str, :Add}`, and +`string` is the **unique** type satisfying both — so it resolves at `string` +(concat folds) and the ascription materializes the result once. The same +machinery gives exact-integer semantics for the numeric case. + +**Why it is not a quick patch (grounded).** The `memory(string) : Add` failure +does not surface at the `let`; the `let` returns its predicates and they are +discharged later, at the function-level `reduce` (`TcStmt.hs:639`). So a local +"try, then coerce on failure" at the ascription is infeasible. A real fix means +either (a) changing ascription checking from "push `T` into `e`" to +"infer `e`, then coerce", which risks regressions wherever a `let`/`return` +currently relies on the expected type to resolve a polymorphic RHS; or (b) a +defaulting rule that resolves a `{:Str, :Add}` (more generally +comptime-class + operation-class) variable to its unique satisfying type. Both +reintroduce a form of the implicit coercion the literal-wrapping design +deliberately replaced, so this is an architectural decision to take deliberately, +not improvise. Scope is bounded (only annotations whose type has a `Str`/`Int` +instance — today just `memory(string)` / `word` / `integer`), so a guarded, +test-gated implementation is plausible as a follow-up. + +--- + +## Ordered implementation steps + +Each step leaves all existing tests passing. + +1. **`Primitives.hs` / `TcEnv.hs` / `NameResolution.hs`** — add `strClassName = + "Str"`, `fromStringScheme : forall a. (a:Str) => string -> a`, the + `fromString` entry, the two primitive instances (`string`, `memory(string)`), + and the `memStringFromLit` primitive name. Reserve the class name. Follow + the `Int` additions (noting the compound `memory(string)` instance head). + +2. **`StrLiteralDesugar.hs`** + `sol-core.cabal` module entry + pipeline wiring + in `SolcorePipeline.hs` (clone `IntLiteralDesugar`). `tcLit`/`typeOfTcExp` + for `StrLit` already return `string`. + +3. **`TcSimplify.hs`** — skip `Str` constraints in the `noDesugarCalls` validity + checks, as for `Int`. + +4. **`Specialise.hs`** — `specCall` case resolving `Str.fromString` to identity + (`string`) or `memStringFromLit` (`memory(string)`). + +5. **`EmitHull.hs`** — intercept `memStringFromLit [StrLit s]`: compute layout, + register the self-contained per-literal `__strlit_` function, rewrite + the call, prepend the generated functions to the object. Comptime-only + enforcement is handled by generalizing `markIntegerComptime` to + `markComptimeOnly` in `TcStmt.hs` (covers `integer` and `string`). + +6. **Tests** — see below. + +7. **This doc** — update with results, gaps, and the `code(string)` follow-up if + pursued. + +--- + +## Tests + +Source-level (`test/examples/comptime/`, registered in `test/Cases.hs`). These +compile through `emitHull` (the test path stops at Hull objects; runtime/ABI +value checks would need a `dispatch` testrunner case — see gaps). The canonical +style is **A1** (apply `Str.fromString` to the comptime expression directly); +`string-concat-mem.solc` additionally exercises **A2** (`let s : string = …` +then `Str.fromString(s)`), the `string`-typed-`let` + dead-let-substitution +path. + +- **`string-lit-mem.solc`** (A1) — `main()` returns `"abcd"` as `memory(string)`. + The simplest materialization; the generated `__strlit_0` writes length 4 and + the packed word. Verified through `yule` (Hull→Yul typechecks). +- **`string-concat-mem.solc`** — `main()` computes `strlen` of `"Hello, " + + "world!"` materialized two ways: A1 (`Str.fromString("Hello, " + "world!")`) + and A2 (a `greetingLet` helper using a `string` `let`). `+` folds via + `concatLit` in the `string` domain, so both forms produce the same `StrLit` + and share **one** `__strlit_*` allocator (len 13) — proving the + comptime→runtime boundary and dedup across forms. +- **`string-lit-dedup.solc`** — `main()` materializes `"alpha"`, `"beta"`, + `"alpha"`; exactly **two** `__strlit_*` allocators are emitted (the repeated + `"alpha"` shares one). +- **`string-mem-runtime-fail.solc`** (`runTestExpectingFailure`) — returns a + `string`-typed `let` where `memory(string)` is expected, with no conversion. + Rejected at type checking ("memory(string) and string do not unify"), + validating the comptime-only invariant. + +Note: every test needs a `main` entry point. With `--no-gen-dispatch` and no +`main`, the specializer has no roots and prunes all functions, so no +materialization happens — an early version of the concat/dedup tests compiled +vacuously for this reason. + +Already-passing string tests unaffected by the desugaring: `string-lit-ops`, +`string-lit-len`, `string-lit-keccak` (comptime `concatLit`/`strlenLit`/ +`keccakLit` folding) and `string-const`. + +--- + +## Known gaps and future work + +| Gap | Impact | Resolution | +|---|---|---| +| Inline `mstore` materializer code size | Large literals bloat bytecode | `code(string) : Str` data-section path | +| `code(a)` type constructor | No data-section strategy yet | Future additive instance + `codecopy` conversion | +| No `string`-taking helper (`toMemory`) | Must apply `Str.fromString` where the literal is in scope | "Always inline" annotation for helpers (own work) | +| String literals in constructor/deploy code | Allocators emitted into runtime object only; a deploy-side call would not resolve | Emit allocators into the object that references them, or duplicate | +| ~~No runtime/ABI value test~~ | ~~correctness of returned bytes unchecked~~ | ✓ `dispatch/stringlit.json` returns `memory(string)`, asserted via evmone | +| ~~No clean `string` EmitHull guard message~~ | ~~"empty sum string" crash~~ | ✓ `comptimeOnlyMastName` guards on return/param/let (`EmitHull.hs`) | +| `string` binding without `comptime` | Forced comptime by `markComptimeOnly`; if it still survived, clean guard message now | Enforce `comptime` in SAIL/MAST checkers (same gap as `integer`) | +| `let s = "x"` (unannotated) | Result representation ambiguous (`string` vs `memory(string)`) | Default rule (e.g. to `memory(string)`) — mirror the integer `word` default question | +| String literal patterns | Runtime string-match unsupported; comptime-label match not planned | Separate feature if needed | +| UTF-8 vs byte semantics | `len` is UTF-8 byte length (matches `strlenLit`) | Documented; consistent with Solidity `bytes`/`string` | diff --git a/run_contests.sh b/run_contests.sh index 0337035ed..3d3b747c7 100755 --- a/run_contests.sh +++ b/run_contests.sh @@ -15,6 +15,7 @@ bash ./contest.sh test/examples/dispatch/payable.json bash ./contest.sh test/examples/dispatch/payable_ctor.json bash ./contest.sh test/examples/dispatch/nonpayable_ctor.json bash ./contest.sh test/examples/dispatch/concat.json +bash ./contest.sh test/examples/dispatch/stringlit.json bash ./contest.sh test/examples/dispatch/slices.json bash ./contest.sh test/examples/dispatch/fallback.json bash ./contest.sh test/examples/dispatch/ecrecover.json diff --git a/sol-core.cabal b/sol-core.cabal index cbc3df7d9..7e090e16b 100644 --- a/sol-core.cabal +++ b/sol-core.cabal @@ -69,6 +69,7 @@ library Solcore.Desugarer.IfDesugarer Solcore.Desugarer.IndirectCall Solcore.Desugarer.IntLiteralDesugar + Solcore.Desugarer.StrLiteralDesugar Solcore.Desugarer.ReplaceWildcard Solcore.Desugarer.ContractDispatch Solcore.Desugarer.ReplaceFunTypeArgs diff --git a/src/Solcore/Backend/EmitHull.hs b/src/Solcore/Backend/EmitHull.hs index cbf128add..530215f62 100644 --- a/src/Solcore/Backend/EmitHull.hs +++ b/src/Solcore/Backend/EmitHull.hs @@ -3,11 +3,14 @@ module Solcore.Backend.EmitHull (emitHull) where import Common.Monad import Control.Monad (when) import Control.Monad.State +import Data.ByteString qualified as BS import Data.List (partition) import Data.Map qualified as Map import Data.Maybe (fromMaybe) import Data.Set qualified as Set import Data.String (fromString) +import Data.Text qualified as T +import Data.Text.Encoding qualified as TE import GHC.Stack (HasCallStack) import Language.Hull qualified as Hull import Language.Yul @@ -18,6 +21,7 @@ import Solcore.Frontend.Syntax.Name import Solcore.Frontend.Syntax.Stmt (Literal (..)) import Solcore.Frontend.Syntax.Ty (Ty (..), Tyvar (..)) import Solcore.Frontend.TypeInference.TcMonad (insts) +import Solcore.Primitives.Primitives (memStringFromLitName) import Prelude hiding (product) emitHull :: Bool -> MastCompUnit -> IO [Hull.Object] @@ -43,7 +47,10 @@ data EcState = EcState ecDebug :: Bool, ecContext :: [String], ecDeployer :: Maybe Hull.Body, - ecFresh :: Int + ecFresh :: Int, + -- String literals materialized into memory(string), keyed by content for + -- dedup; value is the generated allocator's name (__strlit_). + ecStrLits :: Map.Map String String } initEcState :: Bool -> EcState @@ -55,7 +62,8 @@ initEcState debugp = ecDebug = debugp, ecContext = [], ecDeployer = Nothing, - ecFresh = 0 + ecFresh = 0, + ecStrLits = Map.empty } -- isolate local changes to nesting level and variable substitution @@ -94,6 +102,20 @@ builtinDataInfo = [("sum", sumDataTy)] mastIntegerTy :: MastTy mastIntegerTy = MastTyCon (Name "integer") [] +-- | The comptime-only string type. A `string` has no runtime representation +-- (it is an empty `data string;`); it must be folded away or materialized into +-- memory(string) via Str.fromString before hull emission. Reaching here is a +-- bug, and without this guard it would surface as a cryptic "empty sum string". +mastStringTy :: MastTy +mastStringTy = MastTyCon (Name "string") [] + +-- | Name of a comptime-only type if the given type is one, for guard messages. +comptimeOnlyMastName :: MastTy -> Maybe String +comptimeOnlyMastName t + | t == mastIntegerTy = Just "integer" + | t == mastStringTy = Just "string" + | otherwise = Nothing + type VSubst = Map.Map Name Hull.Expr emptyVSubst :: VSubst @@ -130,7 +152,12 @@ emitContract :: MastContract -> EM Hull.Object emitContract c = do let cname = show (mastContrName c) writes ["Emitting hull for contract ", cname] - runtimeBody <- concatMapM emitCDecl (mastContrDecls c) + modify (\s -> s {ecStrLits = Map.empty}) + runtimeBody0 <- concatMapM emitCDecl (mastContrDecls c) + -- Prepend the per-literal string allocators referenced by the runtime code. + strLits <- gets ecStrLits + let strLitFuns = [genStrLitFun fn s | (s, fn) <- Map.toList strLits] + let runtimeBody = strLitFuns ++ runtimeBody0 deployer <- gets ecDeployer case deployer of Nothing -> pure (Hull.Object cname runtimeBody []) @@ -138,6 +165,65 @@ emitContract c = do let runtimeObject = Hull.Object cname runtimeBody [] in pure (Hull.Object (cname ++ "Deploy") code [runtimeObject]) +-- | Register a string literal for materialization, deduplicated by content. +-- Returns the name of the generated allocator function. +registerStrLit :: String -> EM String +registerStrLit s = do + lits <- gets ecStrLits + case Map.lookup s lits of + Just fn -> pure fn + Nothing -> do + let fn = "__strlit_" ++ show (Map.size lits) + modify (\st -> st {ecStrLits = Map.insert s fn (ecStrLits st)}) + pure fn + +-- | Generate the allocator for one string literal. It allocates length + +-- character slots from the free-memory pointer (0x40), writes the byte length +-- and the (right-padded) character words, bumps the free pointer, and returns +-- the pointer (the memory(string) representation). The block is self-contained +-- and depends on no other emitted function. +genStrLitFun :: String -> String -> Hull.Stmt +genStrLitFun fn s = + Hull.SFunction fn [] Hull.TWord $ + [ Hull.SAlloc "p" Hull.TWord, + Hull.SAssembly asm, + Hull.SReturn (Hull.EVar "p") + ] + where + (len, charWords, total) = strLitLayout s + asm = + [YAssign ["p"] (YCall "mload" [YLit (YulNumber 0x40)])] + ++ [YExp (YCall "mstore" [YIdent "p", YLit (YulNumber len)])] + ++ [ YExp + ( YCall + "mstore" + [YCall "add" [YIdent "p", YLit (YulNumber (32 * i))], YLit (YulNumber w)] + ) + | (i, w) <- zip [1 ..] charWords + ] + ++ [ YExp + ( YCall + "mstore" + [YLit (YulNumber 0x40), YCall "add" [YIdent "p", YLit (YulNumber total)]] + ) + ] + +-- | Compute the in-memory layout of a string literal: +-- (byte length, character words right-padded to 32 bytes, total bytes allocated). +strLitLayout :: String -> (Integer, [Integer], Integer) +strLitLayout s = + (toInteger len, map chunkToWord chunks, toInteger total) + where + bytes = BS.unpack (TE.encodeUtf8 (T.pack s)) + len = length bytes + chunks = chunk32 bytes + total = 32 * (1 + length chunks) + chunk32 [] = [] + chunk32 xs = let (h, t) = splitAt 32 xs in h : chunk32 t + -- big-endian word of the 32-byte slot (bytes left-aligned, zero-padded right) + chunkToWord chunk = + foldl (\acc b -> acc * 256 + toInteger b) 0 (take 32 (chunk ++ replicate 32 0)) + emitCDecl :: MastContractDecl -> EM [Hull.Stmt] emitCDecl (MastCFunDecl f) = emitFunDef f emitCDecl (MastCMutualDecl ds) = case findConstructor ds of @@ -164,8 +250,10 @@ findConstructor = go ----------------------------------------------------------------------- emitFunDef :: (HasCallStack) => MastFunDef -> EM [Hull.Stmt] emitFunDef fd = withContext (show (mastFunName fd)) do - when (mastFunReturn fd == mastIntegerTy) $ - errorsEM ["integer-typed return in '", show (mastFunName fd), "': comptime value not eliminated before hull emission"] + case comptimeOnlyMastName (mastFunReturn fd) of + Just tn -> + errorsEM [tn, "-typed return in '", show (mastFunName fd), "': comptime value not eliminated before hull emission"] + Nothing -> pure () let name = show (mastFunName fd) hullArgs <- mapM translateParam (mastFunParams fd) hullTyp <- translateMastType (mastFunReturn fd) @@ -177,8 +265,8 @@ emitFunDef fd = withContext (show (mastFunName fd)) do translateParam :: MastParam -> EM Hull.Arg translateParam (MastParam n _ct t) - | t == mastIntegerTy = - errorsEM ["integer-typed parameter '", show n, "': comptime value not eliminated before hull emission"] + | Just tn <- comptimeOnlyMastName t = + errorsEM [tn, "-typed parameter '", show n, "': comptime value not eliminated before hull emission"] | otherwise = Hull.TArg (show n) <$> translateMastType t ----------------------------------------------------------------------- @@ -283,6 +371,11 @@ emitExp (MastVar x) = do Nothing -> pure (Hull.EVar (show (mastIdName x)), []) -- special handling of revertLit emitExp (MastCall (MastId "revertLit" _) [MastLit (StrLit s)]) = pure (Hull.EUnit, [Hull.SRevert s]) +-- materialize a string literal into memory(string): call its per-literal allocator +emitExp (MastCall (MastId name _) [MastLit (StrLit s)]) + | name == memStringFromLitName = do + fn <- registerStrLit s + pure (Hull.ECall fn [], []) emitExp (MastCall f as) = do (hullArgs, codes) <- unzip <$> mapM emitExp as let call = Hull.ECall (show (mastIdName f)) hullArgs @@ -309,8 +402,8 @@ emitStmt (MastAssign i e) = do let assign = [Hull.SAssign (Hull.EVar (show (mastIdName i))) e'] return (stmts ++ assign) emitStmt (MastLet _ct (MastId name ty) _ mexp) - | ty == mastIntegerTy = - errorsEM ["integer-typed let '", show name, "': comptime value not eliminated before hull emission"] + | Just tn <- comptimeOnlyMastName ty = + errorsEM [tn, "-typed let '", show name, "': comptime value not eliminated before hull emission"] | otherwise = do let hullName = show name hullTy <- translateMastType ty diff --git a/src/Solcore/Backend/MastEval.hs b/src/Solcore/Backend/MastEval.hs index 191d899aa..2443ef47e 100644 --- a/src/Solcore/Backend/MastEval.hs +++ b/src/Solcore/Backend/MastEval.hs @@ -51,7 +51,7 @@ import Language.Yul (YLiteral (..), YulExp (..), YulStmt (..)) import Solcore.Backend.Mast import Solcore.Frontend.Syntax.Name import Solcore.Frontend.Syntax.Stmt (Literal (..)) -import Solcore.Primitives.Primitives (integerPrimNames) +import Solcore.Primitives.Primitives (integerPrimNames, memStringFromLitName, stringPrimNames) ----------------------------------------------------------------------- -- Data structures @@ -460,6 +460,7 @@ evalPrimitive (Name "integerLt") [MastLit (IntLit a), MastLit (IntLit b)] = evalPrimitive (Name "integerEq") [MastLit (IntLit a), MastLit (IntLit b)] = Just (mkBool (a == b)) evalPrimitive (QualName (Name "Int") "fromInteger") [x] = Just x -- identity for integer -> integer +evalPrimitive (QualName (Name "Str") "fromString") [x] = Just x -- identity for string -> string evalPrimitive _ _ = Nothing bsToIntegerBE :: BS.ByteString -> Integer @@ -829,10 +830,11 @@ builtinPureFuns = Name "keccakLit" ] ++ integerPrimNames + ++ stringPrimNames -- Functions with dummy pure bodies that are intercepted by EmitHull builtinImpureFuns :: Set.Set Name -builtinImpureFuns = Set.fromList [Name "revertLit"] +builtinImpureFuns = Set.fromList [Name "revertLit", memStringFromLitName] -- | Compute the set of pure functions via fixed-point iteration. -- Start from builtinPureFuns; each iteration adds functions whose bodies diff --git a/src/Solcore/Backend/Specialise.hs b/src/Solcore/Backend/Specialise.hs index 995850bc8..e57f11513 100644 --- a/src/Solcore/Backend/Specialise.hs +++ b/src/Solcore/Backend/Specialise.hs @@ -399,6 +399,16 @@ specCall (Id (QualName (Name "Int") "fromInteger") ty) args _ = do if resultTy == word then pure (Id (Name "wordFromInteger") (Prim.integer :-> word), args') else pure (Id (QualName (Name "Int") "fromInteger") (Prim.integer :-> resultTy), args') +-- Str.fromString coercion: resolve based on result type. +-- string -> memory(string) becomes memStringFromLit (lowered per-literal by EmitHull) +-- string -> string is identity (folded by MastEval) +specCall (Id (QualName (Name "Str") "fromString") ty) args _ = do + args' <- mapM (\a -> specExp a (typeOfTcExp a)) args + s <- getSpSubst + let resultTy = snd (splitTy (applytv s ty)) + if resultTy == Prim.memString + then pure (Id Prim.memStringFromLitName (Prim.string :-> Prim.memString), args') + else pure (Id (QualName (Name "Str") "fromString") (Prim.string :-> resultTy), args') specCall i args _ty | idName i `elem` comptimeBuiltins = do args' <- mapM (\a -> specExp a (typeOfTcExp a)) args diff --git a/src/Solcore/Desugarer/StrLiteralDesugar.hs b/src/Solcore/Desugarer/StrLiteralDesugar.hs new file mode 100644 index 000000000..bd3da4802 --- /dev/null +++ b/src/Solcore/Desugarer/StrLiteralDesugar.hs @@ -0,0 +1,32 @@ +module Solcore.Desugarer.StrLiteralDesugar (desugarStrLiterals) where + +import Data.Generics +import Solcore.Frontend.Syntax +import Solcore.Primitives.Primitives (strClassName) + +-- Wrap comptime string values in expression position with a call to +-- Str.fromString, making them polymorphic over their target representation: +-- * every string literal, and +-- * every comptime concatenation (`concatLit(...)`). +-- At a `string` site the wrapper resolves to the identity instance (and folds); +-- at a `memory(string)` site it materializes. Because `concatLit`'s parameters +-- are `string`, a wrapped `concatLit` used as an argument to another `concatLit` +-- resolves to identity, so nested concatenations collapse to a single literal +-- and materialize once. Pattern literals (PLit) are not expressions and are +-- left untouched. +desugarStrLiterals :: [TopDecl Name] -> [TopDecl Name] +desugarStrLiterals = everywhere (mkT desugarExp) + +fromStringName :: Name +fromStringName = QualName strClassName "fromString" + +-- | Recognise concatLit regardless of qualification (e.g. @std.concatLit@). +isConcatLit :: Name -> Bool +isConcatLit (Name "concatLit") = True +isConcatLit (QualName _ "concatLit") = True +isConcatLit _ = False + +desugarExp :: Exp Name -> Exp Name +desugarExp (Lit l@(StrLit _)) = Call Nothing fromStringName [Lit l] +desugarExp e@(Call _ n _) | isConcatLit n = Call Nothing fromStringName [e] +desugarExp e = e diff --git a/src/Solcore/Frontend/ComptimeCheck.hs b/src/Solcore/Frontend/ComptimeCheck.hs index 6f641c462..d93951ba4 100644 --- a/src/Solcore/Frontend/ComptimeCheck.hs +++ b/src/Solcore/Frontend/ComptimeCheck.hs @@ -26,6 +26,7 @@ import Solcore.Frontend.Syntax.Name (Name) import Solcore.Frontend.Syntax.Stmt import Solcore.Frontend.Syntax.Ty (Ty (..)) import Solcore.Frontend.TypeInference.Id (Id (..)) +import Solcore.Primitives.Primitives qualified as Prim ----------------------------------------------------------------------- -- Comptime-ness classification @@ -87,15 +88,16 @@ checkContrDecl _ _ = Right () ----------------------------------------------------------------------- checkFunDef :: SigTable -> String -> FunDef Id -> Either String () -checkFunDef st ctx fd = checkBody st (sigRetComptime sig) ctx initEnv (funDefBody fd) +checkFunDef st ctx fd = checkBody st (effRetComptime sig) ctx initEnv (funDefBody fd) where sig = funSignature fd -- For '-> comptime' functions, treat ALL params as CTComptime when checking -- the body: this verifies "given comptime args, does the body produce comptime?" - -- For other functions, non-comptime params are CTRuntime. + -- A param of comptime-only type (string/integer) is also implicitly comptime, + -- since such values exist only at compile time. Other params are CTRuntime. initEnv = Map.fromList - [ (idName (paramName p), if paramComptime p || sigRetComptime sig then CTComptime else CTRuntime) + [ (idName (paramName p), if paramComptime p || effRetComptime sig || isComptimeOnlyTy (paramTy p) then CTComptime else CTRuntime) | p <- sigParams sig ] @@ -211,8 +213,20 @@ checkCallSite st env f args = ++ "' of '" ++ show (idName f) ++ "'" - paramTy (Typed _ _ ty) = ty - paramTy (Untyped _ _) = TyCon (error "paramTy: Untyped") [] + +-- | A value of comptime-only type (string / integer) exists only at compile +-- time, so it is always comptime regardless of annotation. +isComptimeOnlyTy :: Ty -> Bool +isComptimeOnlyTy t = t == Prim.string || t == Prim.integer + +-- | A function is effectively '-> comptime' if it is annotated so, or if its +-- return type is comptime-only. +effRetComptime :: Signature Id -> Bool +effRetComptime sig = sigRetComptime sig || maybe False isComptimeOnlyTy (sigReturn sig) + +paramTy :: Param Id -> Ty +paramTy (Typed _ _ ty) = ty +paramTy (Untyped _ _) = TyCon (error "paramTy: Untyped") [] -- | True if the type contains any type variable or meta variable. hasTypeVar :: Ty -> Bool @@ -252,7 +266,7 @@ classifyCall st env f args = case Map.lookup (idName f) st of Nothing -> CTDeferred Just sig - | sigRetComptime sig && allArgsComptime -> + | effRetComptime sig && allArgsComptime -> CTComptime | otherwise -> CTDeferred diff --git a/src/Solcore/Frontend/Syntax/NameResolution.hs b/src/Solcore/Frontend/Syntax/NameResolution.hs index 4d2b6d9d0..5bc7cb2c4 100644 --- a/src/Solcore/Frontend/Syntax/NameResolution.hs +++ b/src/Solcore/Frontend/Syntax/NameResolution.hs @@ -921,7 +921,7 @@ emptyEnv = (Name "sum", TTyCon) ] ) - (Map.fromList [(Name "invokable", TClass), (Name "Int", TClass)]) + (Map.fromList [(Name "invokable", TClass), (Name "Int", TClass), (Name "Str", TClass)]) Map.empty ( Map.fromList [ (Name "true", TDataCon), @@ -940,7 +940,8 @@ emptyEnv = (Name "integerMul", TFunction), (Name "integerLt", TFunction), (Name "integerEq", TFunction), - (QualName (Name "Int") "fromInteger", TFunction) + (QualName (Name "Int") "fromInteger", TFunction), + (QualName (Name "Str") "fromString", TFunction) ] ) diff --git a/src/Solcore/Frontend/TypeInference/TcEnv.hs b/src/Solcore/Frontend/TypeInference/TcEnv.hs index 6b6d3531b..07fe689a6 100644 --- a/src/Solcore/Frontend/TypeInference/TcEnv.hs +++ b/src/Solcore/Frontend/TypeInference/TcEnv.hs @@ -173,7 +173,8 @@ primCtx = integerMul, integerLt, integerEq, - fromIntegerEntry + fromIntegerEntry, + fromStringEntry ] -- Primitive constructor schemes only — never overwritten by user function definitions. @@ -209,6 +210,11 @@ primInstEnv = [ [] :=> InCls intClassName word [], [] :=> InCls intClassName integer [] ] + ), + ( strClassName, + [ [] :=> InCls strClassName string [], + [] :=> InCls strClassName memString [] + ] ) ] @@ -216,7 +222,8 @@ primClassEnv :: ClassTable primClassEnv = Map.fromList [ (Name "invokable", invokableInfo), - (intClassName, intInfo) + (intClassName, intInfo), + (strClassName, strInfo) ] where invokableInfo = @@ -233,6 +240,12 @@ primClassEnv = [QualName intClassName "fromInteger"] (InCls intClassName (TyVar (TVar (Name "a"))) []) [] + strInfo = + ClassInfo + 0 + [QualName strClassName "fromString"] + (InCls strClassName (TyVar (TVar (Name "a"))) []) + [] primDataType :: Map Name DataTy primDataType = diff --git a/src/Solcore/Frontend/TypeInference/TcSimplify.hs b/src/Solcore/Frontend/TypeInference/TcSimplify.hs index 5a51c83b5..154176775 100644 --- a/src/Solcore/Frontend/TypeInference/TcSimplify.hs +++ b/src/Solcore/Frontend/TypeInference/TcSimplify.hs @@ -84,7 +84,7 @@ checkEntails qs rs = noDesugarCalls <- getNoDesugarCalls info [">>! Trying to check the entailment of:", pretty rs, " from:", pretty qs] let qs' = nub $ concatMap (bySuperM ctable) qs - skip q = isInvoke q || (noDesugarCalls && isInt q) + skip q = isInvoke q || (noDesugarCalls && (isInt q || isStr q)) unsolved q = not (isHnf q) && not (skip q) && not (entail ctable itable qs' q) -- compiler generated instances can introduce invokable constraints -- not present in the called function. Since type inference can produce @@ -103,6 +103,10 @@ isInt :: Pred -> Bool isInt (InCls n _ _) = n == Name "Int" isInt _ = False +isStr :: Pred -> Bool +isStr (InCls n _ _) = n == Name "Str" +isStr _ = False + simplify :: [Pred] -> [Pred] -> TcM [Pred] simplify qs ps = do diff --git a/src/Solcore/Frontend/TypeInference/TcStmt.hs b/src/Solcore/Frontend/TypeInference/TcStmt.hs index b968741d4..d3e8bc014 100644 --- a/src/Solcore/Frontend/TypeInference/TcStmt.hs +++ b/src/Solcore/Frontend/TypeInference/TcStmt.hs @@ -649,7 +649,7 @@ tiFunDef d@(FunDef isPub sig@(Signature _ _ n args _ _ _) bd) = -- elaborating the type signature sig' <- elabSignature [] sig sch (fd', sch') <- withCurrentSubst (FunDef isPub sig' bd1, sch) - pure (markIntegerComptime fd', sch') + pure (markComptimeOnly fd', sch') ambiguityCheck :: Scheme -> TcM Bool ambiguityCheck (Forall _ (ps :=> ty)) = @@ -740,7 +740,7 @@ tcFunDef incl vs' qs d@(FunDef isPub sig@(Signature vs ps n _ _ _ _) _) let ann' = if changeTy then inf else ann fdt <- elabFunDef isPub vs' sig1 bd1' inf ann' `wrapError` d (fd', ann'') <- withCurrentSubst (fdt, ann') - pure (markIntegerComptime fd', ann'') + pure (markComptimeOnly fd', ann'') | otherwise = tiFunDef d -- elaborating function definition @@ -1416,14 +1416,16 @@ hnfEntails qs ps = remaining <- toHnfs depth needSolving pure (filter (not . skip) remaining) --- Any let binding whose type is `integer` is implicitly comptime: integer is a --- comptime-only type and cannot survive to hull emission regardless of whether --- the user wrote `comptime`. Applied after the full substitution is known. -markIntegerComptime :: FunDef Id -> FunDef Id -markIntegerComptime = everywhere (mkT fix) +-- Any let binding whose type is comptime-only (`integer` or `string`) is +-- implicitly comptime: such types have no runtime representation and cannot +-- survive to hull emission regardless of whether the user wrote `comptime`. +-- Applied after the full substitution is known. +markComptimeOnly :: FunDef Id -> FunDef Id +markComptimeOnly = everywhere (mkT fix) where - fix (Let _ i mt me) | idType i == Prim.integer = Let True i mt me + fix (Let _ i mt me) | isComptimeOnly (idType i) = Let True i mt me fix s = s + isComptimeOnly t = t == Prim.integer || t == Prim.string -- type generalization diff --git a/src/Solcore/Pipeline/SolcorePipeline.hs b/src/Solcore/Pipeline/SolcorePipeline.hs index e07175460..3b0e4bc8f 100644 --- a/src/Solcore/Pipeline/SolcorePipeline.hs +++ b/src/Solcore/Pipeline/SolcorePipeline.hs @@ -25,6 +25,7 @@ import Solcore.Desugarer.IndirectCall (indirectCallTopDecls) import Solcore.Desugarer.IntLiteralDesugar (desugarIntLiterals) import Solcore.Desugarer.ReplaceFunTypeArgs import Solcore.Desugarer.ReplaceWildcard (replaceWildcardTopDecls) +import Solcore.Desugarer.StrLiteralDesugar (desugarStrLiterals) import Solcore.Frontend.ComptimeCheck (checkComptimeEarly) import Solcore.Frontend.Module.Identity qualified as Mod import Solcore.Frontend.Module.Loader (ModuleGraph (..), loadModuleGraph, moduleSourcePath, moduleValidationTopDeclSegments) @@ -355,7 +356,13 @@ prepareInferenceDeclsForTypeInference opts emitOutput imps inferenceDecls = do putStrLn "> Integer literal desugaring:" putStrLn $ prettyInferenceDecls withFromInt - pure withFromInt + -- String literal desugaring: wrap bare string literals in fromString() + let withFromStr = mapModuleInferenceTopDecls desugarStrLiterals withFromInt + liftIO $ when verbose $ do + putStrLn "> String literal desugaring:" + putStrLn $ prettyInferenceDecls withFromStr + + pure withFromStr parseExternalLibSpecs :: [String] -> Either String [(Name, FilePath)] parseExternalLibSpecs = diff --git a/src/Solcore/Primitives/Primitives.hs b/src/Solcore/Primitives/Primitives.hs index adab303a8..e112352b8 100644 --- a/src/Solcore/Primitives/Primitives.hs +++ b/src/Solcore/Primitives/Primitives.hs @@ -174,6 +174,49 @@ integerPrimNames = QualName intClassName "fromInteger" ] +-- Str class: overloaded coercion from string literals +-- instance string : Str { fromString = identity } +-- instance memory(string) : Str { fromString = materialize into memory } +-- +-- The memory(string) instance is resolved by a dedicated case in +-- Specialise.specCall to `memStringFromLit`, which EmitHull lowers per literal. +-- Both instances are registered bodyless in TcEnv.primInstEnv; the rewrite keeps +-- the original literal argument in place (a real instance body would move the +-- literal behind a runtime parameter and defeat the EmitHull intercept). + +strClassName :: Name +strClassName = Name "Str" + +strVar :: Tyvar +strVar = aVar + +strPred :: Pred +strPred = InCls strClassName (TyVar strVar) [] + +-- | Scheme for fromString: forall a. (a:Str) => string -> a +fromStringScheme :: Scheme +fromStringScheme = Forall [strVar] ([strPred] :=> (string :-> TyVar strVar)) + +fromStringEntry :: (Name, Scheme) +fromStringEntry = (QualName strClassName "fromString", fromStringScheme) + +-- | The runtime representation of a string: memory(string). +memString :: Ty +memString = TyCon "memory" [string] + +-- | Backend marker emitted by Specialise for `Str.fromString @ memory(string)`. +-- Intercepted by EmitHull; never folded (it emits code, has no comptime value), +-- so it is deliberately absent from builtinPureFuns / comptimeBuiltins. +memStringFromLitName :: Name +memStringFromLitName = Name "memStringFromLit" + +-- | String primitive function names that are pure (foldable by MastEval). +-- Only the identity `Str.fromString` belongs here; `memStringFromLit` does not. +stringPrimNames :: [Name] +stringPrimNames = + [ QualName strClassName "fromString" + ] + stack :: Ty -> Ty stack t = TyCon "stack" [t] diff --git a/test/Cases.hs b/test/Cases.hs index 0a394e60e..820f22139 100644 --- a/test/Cases.hs +++ b/test/Cases.hs @@ -56,13 +56,18 @@ comptime = runTestForFile "integer-lit-cond.solc" comptimeFolder, runTestForFile "integer-lit-pat.solc" comptimeFolder, runTestForFile "match_labels.solc" comptimeFolder, + -- comptime string materialization into memory(string) + runTestForFile "string-lit-mem.solc" comptimeFolder, + runTestForFile "string-concat-mem.solc" comptimeFolder, + runTestForFile "string-lit-dedup.solc" comptimeFolder, -- comptime verification: negative cases (must be rejected) runTestExpectingFailure "ct_param_runtime.solc" comptimeFolder, runTestExpectingFailure "ct_param_poly_runtime.solc" comptimeFolder, runTestExpectingFailure "ct_runtime_arg.solc" comptimeFolder, runTestExpectingFailure "ct_let_runtime.solc" comptimeFolder, runTestExpectingFailure "ct_asm_ret.solc" comptimeFolder, - runTestExpectingFailure "ct_overloaded_bad.solc" comptimeFolder + runTestExpectingFailure "ct_overloaded_bad.solc" comptimeFolder, + runTestExpectingFailure "string-mem-runtime-fail.solc" comptimeFolder ] where comptimeFolder = "./test/examples/comptime" diff --git a/test/examples/comptime/string-concat-mem.solc b/test/examples/comptime/string-concat-mem.solc new file mode 100644 index 000000000..aaab6c377 --- /dev/null +++ b/test/examples/comptime/string-concat-mem.solc @@ -0,0 +1,29 @@ +// Comptime string concatenation, materialized into runtime memory(string). +// Concatenation runs at comptime (in the `string` domain); the result is +// materialized at the memory(string) site. All four forms below build the same +// "Hello, world!" (length 13), so they fold to one StrLit and share ONE +// generated allocator (dedup). main returns 4 * 13 = 52. +// +// Forms exercised: +// a — `+` wrapped in Str.fromString (overloaded Add at the `string` site) +// b — terse concatLit (Str.fromString inserted by the desugarer) +// c — nested concatLit (intermediate wraps fold to identity) +// d — A2: a `string`-typed let, then convert (dead-let substitution) + +import std; +import std.{*}; + +contract StringConcat { + function viaLet() -> memory(string) { + let s : string = "Hello, " + "world!"; + return Str.fromString(s); + } + + public function main() -> word { + let a : memory(string) = Str.fromString("Hello, " + "world!"); + let b : memory(string) = concatLit("Hello, ", "world!"); + let c : memory(string) = concatLit(concatLit("Hello", ", "), "world!"); + let d : memory(string) = viaLet(); + return strlen(a) + strlen(b) + strlen(c) + strlen(d); + } +} diff --git a/test/examples/comptime/string-lit-dedup.solc b/test/examples/comptime/string-lit-dedup.solc new file mode 100644 index 000000000..777838c2d --- /dev/null +++ b/test/examples/comptime/string-lit-dedup.solc @@ -0,0 +1,15 @@ +// Distinct string literals get distinct allocators; identical literals share +// one (dedup by content). "alpha" is used twice and "beta" once, so the +// generated hull must contain exactly two __strlit_* allocators. + +import std; +import std.{*}; + +contract StringDedup { + public function main() -> word { + let x : memory(string) = "alpha"; + let y : memory(string) = "beta"; + let z : memory(string) = "alpha"; + return strlen(x) + strlen(y) + strlen(z); + } +} diff --git a/test/examples/comptime/string-lit-mem.solc b/test/examples/comptime/string-lit-mem.solc new file mode 100644 index 000000000..73a2c89c2 --- /dev/null +++ b/test/examples/comptime/string-lit-mem.solc @@ -0,0 +1,14 @@ +// Materialize a string literal into a runtime memory(string). +// The literal is comptime; Str.fromString at memory(string) lowers to a +// per-literal allocator that writes the length and characters into memory. +// +// Expected: compiles; main() returns a memory(string) for "abcd". + +import std; +import std.{*}; + +contract StringLitMem { + public function main() -> memory(string) { + return "abcd"; + } +} diff --git a/test/examples/comptime/string-mem-runtime-fail.solc b/test/examples/comptime/string-mem-runtime-fail.solc new file mode 100644 index 000000000..0f0ab9ca3 --- /dev/null +++ b/test/examples/comptime/string-mem-runtime-fail.solc @@ -0,0 +1,13 @@ +// A `string` is comptime-only: it has no runtime representation. Returning a +// string-typed value where memory(string) is expected, without an explicit +// Str.fromString conversion, must be rejected by the type checker. + +import std; +import std.{*}; + +contract StringMemRuntimeFail { + public function f() -> memory(string) { + let s : string = "x"; + return s; + } +} diff --git a/test/examples/dispatch/stringlit.json b/test/examples/dispatch/stringlit.json new file mode 100644 index 000000000..dfaa65a87 --- /dev/null +++ b/test/examples/dispatch/stringlit.json @@ -0,0 +1,39 @@ +{ + "stringlit": { + "bytecode": "", + "contract": "C", + "tests": [ + { + "input": { + "calldata": "", + "value": "0" + }, + "kind": "constructor" + }, + { + "input": { + "comment": "greeting()(string)", + "calldata": "ef690cc0", + "value": "0" + }, + "kind": "call", + "output": { + "returndata": "0000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000000d48656c6c6f2c20776f726c642100000000000000000000000000000000000000", + "status": "success" + } + }, + { + "input": { + "comment": "greetLet()(string)", + "calldata": "84b0d9a0", + "value": "0" + }, + "kind": "call", + "output": { + "returndata": "0000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000000d48656c6c6f2c20776f726c642100000000000000000000000000000000000000", + "status": "success" + } + } + ] + } +} diff --git a/test/examples/dispatch/stringlit.solc b/test/examples/dispatch/stringlit.solc new file mode 100644 index 000000000..6136d3661 --- /dev/null +++ b/test/examples/dispatch/stringlit.solc @@ -0,0 +1,26 @@ +import std.{*}; +import std.{memory, string, uint256}; +import std.dispatch.{*}; +pragma no-patterson-condition ; +pragma no-coverage-condition ; +pragma no-bounded-variable-condition ; + +// End-to-end test of comptime string materialization into memory(string): +// each form must ABI-encode to the same "Hello, world!" return value. +contract C { + constructor() {} + + // terse: concatLit wrapped in Str.fromString by the desugarer + public function greeting() -> memory(string) { + return concatLit("Hello, ", "world!"); + // fromString inserted automatically when using concatLit + // later we may have an operator for that e.g. <> + } + + // A2: via an intermediate string-typed let (dead-let substitution path) + public function greetLet() -> memory(string) { + let s : string = "Hello, " + "world!"; + return Str.fromString(s); + // here fromString needs to be inserted manually + } +}