Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
36 changes: 36 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -77,6 +77,18 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
- Methods returning compound types (structs, arrays) use sret calling convention
- `ResolvedCallee` enum consolidates three callee patterns (Function, AssociatedFunction, InstanceMethod) across all call paths
- `assert!` on mangled name collision: detects `TypeName.method_name` conflicts with top-level functions in release builds
- Add nested compound type codegen: struct-in-struct, array-in-struct, struct-in-array ([#161])
- Recursive `type_byte_size()` computes byte sizes for nested compound types via `TypedContext` struct lookup
- `CompoundFieldLayout` enum (`Scalar`, `NestedStruct`, `NestedArray`) caches sub-layout on `StructFieldSlot` for efficient chained access
- Pointer semantics for compound member/index access: compound fields push i32 pointer, load only at terminal scalar field
- Struct-in-struct: nested struct literals, chained field access (`outer.inner.x`), field writes, parameter passing, sret return, copy
- Array-in-struct: array field literals, index access through struct (`s.arr[i]`), field writes, parameter passing
- Struct-in-array: struct element literals, field access through index (`arr[i].field`), element writes, sret return
- Method support for nested types: `self.inner.x` and `self.arr[i]` via pointer chaining
- Multidimensional array uzumaki: `[[i32; 3]; 2] = @` emits per-element uzumaki stores in non-det blocks
- Struct uzumaki with array fields: `let s: HasArray = @;` emits per-element uzumaki for array-typed fields
- `element_layout: Option<Vec<StructFieldSlot>>` on `ArraySlot` for cached struct-element array layouts
- One level of compound nesting permitted (enforced by analysis rule A026)
- Add assignment statement lowering to WebAssembly codegen ([#146])
- `mut` keyword support in AST: `is_mut: bool` field on `VariableDefinitionStatement`
- Mutability enforcement in type-checker: `AssignToImmutable` error for assignment to non-`mut` variables
Expand Down Expand Up @@ -130,6 +142,13 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
- Migrated codegen restriction rules: A012 array-literal-as-argument, A013 struct-literal-as-argument, A014 array-uzumaki-as-argument, A015 compound-literal-in-unsupported-position, A016 compound-return-call-in-expression-position, A017 compound-return-call-in-assignment, A018 method-call-chain-on-compound-return, A019 array-index-64bit, A022 literal-out-of-range
- New rules: A023 uzumaki-in-reassignment, A024 extern-function-call
- `AssignToImmutable` and `VariableShadowed` remain in the type checker (require scope state)
- Add 5 analysis rules for nested compound type constraints ([#161])
- A026 `NestedCompoundDepth`: reject struct field nesting deeper than one level (definition-site check)
- A027 `UzumakiOnNestedStruct`: reject uzumaki on structs with compound fields
- A028 `UzumakiOnStructInArray`: reject uzumaki on arrays of structs at any dimension depth
- A029 `CompoundLiteralMemberAssign`: reject compound literal assignment directly to compound elements
- A031 `UnsupportedCompoundReturnExpr`: reject complex return expressions in compound-returning functions
- Walker helpers: `has_compound_fields()`, `array_nesting_depth()`, `is_compound_return_call()`

### AST

Expand Down Expand Up @@ -227,6 +246,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
- Fix `from_builtin_str` uses exact case-sensitive matching
- Fix external function parameter parsing corrected in AST builder (previously dropped parameters in some cases)
- Bump `tree-sitter-inference` grammar from 0.0.39 to 0.0.40 — fixes chained member access parsing
- Add `compound_literal_allowed` propagation into nested struct literal fields and array literal elements ([#161])
- `Outer { inner: Inner { x: 1 } }` correctly accepted in variable declarations
- Array literals inside struct fields accepted: `HasArray { arr: [1, 2, 3] }`
- Add `find_enclosing_variable_name()` to `TypedContext` for analysis rule uzumaki struct name lookup ([#161])

### Testing

Expand All @@ -240,6 +263,18 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
- Add 43 analysis walker tests covering all 5 rules across free functions, struct methods, and spec functions ([#156])
- Negative tests for valid code, edge cases for nested loops, deeply nested nondet, overlapping rule triggers
- All four nondet block types (forall, exists, assume, unique) tested for A002
- Add 5 nested compound codegen test fixtures with four-tier verification (byte, WAT, validation, wasmtime execution) ([#161])
- `nested_struct`: struct-in-struct literal, chained access, write, param, return, copy, method
- `struct_with_array`: array-in-struct literal, index access through struct, write, param, method
- `array_of_structs`: struct-in-array literal, field access through index, element write, method
- `nested_struct_with_array`: combined struct nesting with array fields
- `multidim_array_uzumaki`: multidimensional array uzumaki in non-det block
- Add `struct_array_field_nondet` test fixture for struct uzumaki with array fields ([#161])
- Add 3 analysis test modules for nested compound rules ([#161])
- `rules_a026_a028.rs`: nested depth, uzumaki on nested struct, uzumaki on struct-in-array (703 lines)
- `rules_a029_a030.rs`: compound literal in compound assign, uzumaki on deep array (364 lines)
- `rules_a031.rs`: unsupported compound return expression (234 lines)
- Add type checker tests for nested compound literal propagation (`compound_literal_allowed`) ([#161])
- Add 9 method codegen test fixtures with four-tier verification (byte, WAT, validation, wasmtime execution) ([#162])
- `method_instance`, `method_assoc`, `method_self_mutate`, `method_return_struct`, `method_cross_call`, `method_multi_struct`, `method_i64_fields`, `method_three_fields`, `method_array_return`
- Add negative codegen tests for unsupported features: `assert`, `**` operator, standalone `TypeMemberAccess`, recursive compound returns ([#162])
Expand Down Expand Up @@ -574,4 +609,5 @@ Initial tagged release.
[#152]: https://github.com/Inferara/inference/pull/152
[#149]: https://github.com/Inferara/inference/pull/159
[#156]: https://github.com/Inferara/inference/pull/156
[#161]: https://github.com/Inferara/inference/pull/185
[#162]: https://github.com/Inferara/inference/pull/178
33 changes: 33 additions & 0 deletions core/analysis/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -67,6 +67,12 @@ A003 and A005 require a single exit point per function to simplify formal verifi
| A010 | `MethodNeverAccessesSelf` | warning | method declares `self` but never reads or writes a field through it |
| A011 | `EmptyStructDefinition` | warning | struct with no fields and no methods |

### Variable Initialization (errors)

| ID | Struct | Severity | What it checks |
|----|--------|----------|----------------|
| A025 | `UninitializedVariable` | error | variable declared without an initializer |

### Codegen Restrictions (errors)

These rules cover constructs that are valid in the type system but cannot yet be lowered by the code generator. They live here rather than in the type checker because they are implementation limits, not type errors.
Expand All @@ -84,6 +90,12 @@ These rules cover constructs that are valid in the type system but cannot yet be
| A022 | `LiteralOutOfRange` | error | numeric literal is outside the valid range for its declared type |
| A023 | `UzumakiInReassignment` | error | uzumaki (`@`) used in a variable reassignment (only `let` initializers are supported) |
| A024 | `ExternFunctionCall` | error | call to an external (`extern`) function (not yet implemented in codegen) |
| A026 | `NestedCompoundDepth` | error | struct field is itself a nested compound type beyond one level of nesting |
| A027 | `UzumakiOnNestedStruct` | error | uzumaki (`@`) assigned to a struct whose fields include another struct or an array of structs |
| A028 | `UzumakiOnStructInArray` | error | uzumaki (`@`) assigned to an array whose element type is a struct |
| A029 | `CompoundLiteralMemberAssign` | error | compound literal (struct or array) used directly as the RHS of a member-access or array-index assignment |
| A030 | *(removed)* | — | *(uzumaki on scalar arrays now supported at any depth)* |
| A031 | `UnsupportedCompoundReturnExpr` | error | return expression in a compound-returning function is not a supported form (identifier, literal, call, or field/element access) |

## Diagnostic Output Format

Expand Down Expand Up @@ -149,6 +161,12 @@ Rules that need scoping logic beyond `loop_depth` and `nondet_depth` can impleme

Using `dyn FnMut` instead of a generic parameter avoids monomorphization cost when the number of rules grows.

The walker module also exposes several type-inspection helpers used by multiple rules:

- `array_nesting_depth(kind)` — returns how many array layers deep a type is (`[[i32; 3]; 2]` → 2, `i32` → 0)
- `has_compound_fields(ctx, kind)` — returns true if a struct or array type contains fields that are themselves structs, arrays of structs, or multidimensional arrays; used by A026, A027, and A028
- `is_compound_return_call(arena, expr_id, ctx)` — returns true when an expression is a function call that returns a compound type (struct or array); used by A016, A017, and A018

## Testing

Unit tests live alongside each source file in `src/`. The integration test `rule_ids_match_diagnostic_rule_ids` in `lib.rs` asserts that:
Expand All @@ -161,6 +179,20 @@ End-to-end tests that compile `.inf` source and assert on diagnostic output live
cargo test -p inference-tests analysis
```

Test files are organized by rule group:

| File | Rules covered |
|------|---------------|
| `rules_a006_a011.rs` | A006–A011 (uzumaki, missing return, lint warnings) |
| `rules_a012_a022.rs` | A012–A022 (codegen restrictions, literal range) |
| `rules_a023.rs` | A023 (uzumaki in reassignment) |
| `rules_a024.rs` | A024 (extern function calls) |
| `rules_a025.rs` | A025 (uninitialized variable) |
| `rules_a026_a028.rs` | A026–A028 (nested compound depth, uzumaki on nested structs, uzumaki on struct arrays) |
| `rules_a029_a030.rs` | A029 (compound literal in compound assign), A030 removal acceptance tests |
| `rules_a031.rs` | A031 (unsupported compound return expression) |
| `walker_tests.rs` | `walk_function_bodies`, `WalkContext` depth tracking |

## Dependencies

| Crate | Role |
Expand All @@ -174,3 +206,4 @@ cargo test -p inference-tests analysis
1. The walker visits all statements but does not expose expression-level traversal. Rules that need to inspect expressions must do their own descent.
2. Rules are executed sequentially on a single thread. The infrastructure is designed for parallel execution (rules are `Send + Sync`) but parallelism is not yet enabled.
3. `AssignToImmutable` and `VariableShadowed` remain in the type checker because they depend on scope state that the type checker tracks but the analysis pass does not replicate.
4. Nested compound type support (A026) limits nesting depth to one level. Structs whose fields are structs or arrays of structs are permitted; structs whose fields contain further nested structs or arrays-of-structs are rejected. This bound matches what the code generator can lower.
33 changes: 32 additions & 1 deletion core/analysis/src/errors.rs
Original file line number Diff line number Diff line change
Expand Up @@ -144,6 +144,26 @@

#[error("variable `{name}` must be initialized at declaration; use `let {name}: <type> = <value>;`")]
UninitializedVariable { name: String, location: Location },

#[error("struct `{outer}` field `{field}` has type `{ty}` which contains nested compound types; only one level of nesting is supported")]
NestedCompoundDepthExceeded {
outer: String,
field: String,
ty: String,
location: Location,
},

#[error("uzumaki (@) cannot be assigned to struct `{name}` because it contains compound fields; uzumaki is only supported for structs whose fields are all scalars or scalar arrays")]
UzumakiOnNestedStruct { name: String, location: Location },

#[error("uzumaki (@) cannot be assigned to array of structs; arrays of structs do not support uzumaki")]
UzumakiOnStructInArray { location: Location },

#[error("compound literal cannot be assigned directly to a compound element; assign to a temporary variable first")]
CompoundLiteralInCompoundAssign { location: Location },

#[error("return expression in compound-returning function must be a variable, literal, function call, or field/element access; assign the expression to a temporary variable first")]
UnsupportedCompoundReturnExpression { location: Location },
}

impl AnalysisDiagnostic {
Expand Down Expand Up @@ -173,7 +193,12 @@
| AnalysisDiagnostic::LiteralOutOfRange { location, .. }
| AnalysisDiagnostic::UzumakiInReassignment { location }
| AnalysisDiagnostic::ExternFunctionCall { location, .. }
| AnalysisDiagnostic::UninitializedVariable { location, .. } => location,
| AnalysisDiagnostic::UninitializedVariable { location, .. }
| AnalysisDiagnostic::NestedCompoundDepthExceeded { location, .. }
| AnalysisDiagnostic::UzumakiOnNestedStruct { location, .. }
| AnalysisDiagnostic::UzumakiOnStructInArray { location, .. }
| AnalysisDiagnostic::CompoundLiteralInCompoundAssign { location }

Check warning on line 200 in core/analysis/src/errors.rs

View check run for this annotation

Codecov / codecov/patch

core/analysis/src/errors.rs#L196-L200

Added lines #L196 - L200 were not covered by tests
| AnalysisDiagnostic::UnsupportedCompoundReturnExpression { location } => location,
}
}

Expand Down Expand Up @@ -206,6 +231,12 @@
AnalysisDiagnostic::UzumakiInReassignment { .. } => "A023",
AnalysisDiagnostic::ExternFunctionCall { .. } => "A024",
AnalysisDiagnostic::UninitializedVariable { .. } => "A025",
AnalysisDiagnostic::NestedCompoundDepthExceeded { .. } => "A026",
AnalysisDiagnostic::UzumakiOnNestedStruct { .. } => "A027",
AnalysisDiagnostic::UzumakiOnStructInArray { .. } => "A028",
AnalysisDiagnostic::CompoundLiteralInCompoundAssign { .. } => "A029",
// A030: removed (multidimensional scalar array uzumaki is now supported at any depth)
AnalysisDiagnostic::UnsupportedCompoundReturnExpression { .. } => "A031",
}
}
}
Expand Down
13 changes: 12 additions & 1 deletion core/analysis/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@
//!
//! - A025: Variable declarations must have an initializer
//!
//! ### Codegen Restrictions (A012–A019, A022–A024)
//! ### Codegen Restrictions (A012–A019, A022–A031)
//!
//! These rules describe constructs that are valid in the type system but cannot
//! be lowered by the current code generator.
Expand All @@ -51,6 +51,12 @@
//! - A022: Numeric literal out of range for its declared type
//! - A023: Uzumaki used in a variable reassignment (only `let` initializers allowed)
//! - A024: Call to an external (`extern`) function
//! - A026: Nested compound type depth exceeds one level
//! - A027: Uzumaki on struct with compound fields (nested struct)
//! - A028: Uzumaki on array of structs
//! - A029: Compound literal in compound element assignment
//! - A030: (removed — uzumaki on scalar arrays now supported at any depth)
//! - A031: Unsupported expression form in compound-returning function return
//!
//! ## Pipeline Position
//!
Expand Down Expand Up @@ -148,6 +154,11 @@ mod tests {
AnalysisDiagnostic::UzumakiInReassignment { location: dummy_location() },
AnalysisDiagnostic::ExternFunctionCall { name: "print".to_string(), location: dummy_location() },
AnalysisDiagnostic::UninitializedVariable { name: "x".to_string(), location: dummy_location() },
AnalysisDiagnostic::NestedCompoundDepthExceeded { outer: "Outer".to_string(), field: "inner".to_string(), ty: "Inner".to_string(), location: dummy_location() },
AnalysisDiagnostic::UzumakiOnNestedStruct { name: "Outer".to_string(), location: dummy_location() },
AnalysisDiagnostic::UzumakiOnStructInArray { location: dummy_location() },
AnalysisDiagnostic::CompoundLiteralInCompoundAssign { location: dummy_location() },
AnalysisDiagnostic::UnsupportedCompoundReturnExpression { location: dummy_location() },
];

let rules = rules::all_rules();
Expand Down
40 changes: 40 additions & 0 deletions core/analysis/src/rules/compound_literal_member_assign.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
//! A029: Compound literal in compound assignment.
//!
//! Compound literals (struct or array) cannot be used as the RHS of an
//! assignment where the LHS is a member access or array index expression.
//! The codegen does not yet support writing struct/array literals directly
//! to a compound element. Use a temporary variable instead:
//! ```text
//! let temp = Inner { x: 1, y: 2 };
//! outer.inner = temp;
//! ```

use inference_ast::nodes::{Expr, Stmt};

use crate::{errors::AnalysisDiagnostic, walker};

crate::rule! {
/// Compound literals cannot be used as RHS in compound element assignments.
#[id = "A029"]
#[name = "Compound literal in compound assignment"]
#[severity = error]
pub struct CompoundLiteralMemberAssign;
fn check(ctx: &TypedContext) -> Vec<AnalysisDiagnostic> {
let mut errors = Vec::new();
let arena = ctx.arena();
walker::walk_function_bodies(ctx, &mut |stmt_id, _walk_ctx| {
if let Stmt::Assign { left, right } = &arena[stmt_id].kind
&& matches!(arena[*left].kind, Expr::MemberAccess { .. } | Expr::ArrayIndexAccess { .. })
&& matches!(
arena[*right].kind,
Expr::StructLiteral { .. } | Expr::ArrayLiteral { .. }
)
{
errors.push(AnalysisDiagnostic::CompoundLiteralInCompoundAssign {
location: arena[*right].location,
});
}
});
errors
}
}
15 changes: 15 additions & 0 deletions core/analysis/src/rules/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ pub mod array_uzumaki_as_argument;
pub mod compound_literal_as_argument;
pub mod break_inside_nondet_block;
pub mod break_outside_loop;
pub mod compound_literal_member_assign;
pub mod compound_literal_position;
pub mod compound_return_call_assignment;
pub mod compound_return_call_position;
Expand All @@ -15,18 +16,23 @@ pub mod literal_out_of_range;
pub mod method_call_chain_compound;
pub mod method_never_accesses_self;
pub mod missing_return;
pub mod nested_compound_depth;
pub mod return_inside_loop;
pub mod return_inside_nondet_block;
pub mod standalone_uzumaki;
pub mod uninitialized_variable;
pub mod uzumaki_in_reassignment;
pub mod uzumaki_on_nested_struct;
pub mod uzumaki_on_struct_in_array;
pub mod unsupported_compound_return_expr;
pub mod uzumaki_outside_nondet_block;

use array_index_64bit::ArrayIndex64Bit;
use array_uzumaki_as_argument::ArrayUzumakiAsArgument;
use compound_literal_as_argument::CompoundLiteralAsArgument;
use break_inside_nondet_block::BreakInsideNonDetBlock;
use break_outside_loop::BreakOutsideLoop;
use compound_literal_member_assign::CompoundLiteralMemberAssign;
use compound_literal_position::CompoundLiteralPosition;
use compound_return_call_assignment::CompoundReturnCallAssignment;
use compound_return_call_position::CompoundReturnCallPosition;
Expand All @@ -39,11 +45,15 @@ use literal_out_of_range::LiteralOutOfRange;
use method_call_chain_compound::MethodCallChainCompound;
use method_never_accesses_self::MethodNeverAccessesSelf;
use missing_return::MissingReturn;
use nested_compound_depth::NestedCompoundDepth;
use return_inside_loop::ReturnInsideLoop;
use return_inside_nondet_block::ReturnInsideNonDetBlock;
use standalone_uzumaki::StandaloneUzumaki;
use uninitialized_variable::UninitializedVariable;
use uzumaki_in_reassignment::UzumakiInReassignment;
use uzumaki_on_nested_struct::UzumakiOnNestedStruct;
use uzumaki_on_struct_in_array::UzumakiOnStructInArray;
use unsupported_compound_return_expr::UnsupportedCompoundReturnExpr;
use uzumaki_outside_nondet_block::UzumakiOutsideNonDetBlock;

/// Returns all registered analysis rules.
Expand Down Expand Up @@ -78,5 +88,10 @@ pub fn all_rules() -> &'static [&'static dyn crate::rule::Rule] {
&UzumakiInReassignment,
&ExternFunctionCall,
&UninitializedVariable,
&NestedCompoundDepth,
&UzumakiOnNestedStruct,
&UzumakiOnStructInArray,
&CompoundLiteralMemberAssign,
&UnsupportedCompoundReturnExpr,
]
}
Loading
Loading