From 680e02b729d78b31c35eee4e2532964e2955fa74 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 25 Mar 2026 15:13:43 +0100 Subject: [PATCH 1/2] Fix FUNCTION_CALL callee type: use code type instead of Empty FUNCTION_CALL callees (e.g., print) had Empty type in the symbol table because coreStmtsToGoto created the callee expression with .Empty type. CBMC instrument_preconditions crashed trying to_code_type on Empty. Fix: add Ty.Identifier.code and Ty.mkCode, use it for the callee expression in coreStmtsToGoto. The code type flows through collectSymbolRefs into the symbol table naturally. Fixes 16 Python CBMC tests that use class-related function calls. Co-authored-by: Kiro --- Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean | 3 ++- Strata/Backends/CBMC/GOTO/InstToJson.lean | 6 ++++++ Strata/Backends/CBMC/GOTO/Type.lean | 8 ++++++++ 3 files changed, 16 insertions(+), 1 deletion(-) diff --git a/Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean b/Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean index 796b5d737..e5bf2cff2 100644 --- a/Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean +++ b/Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean @@ -162,7 +162,8 @@ private partial def coreStmtsToGoto .Integer CProverGOTO.Expr.symbol name ty | [] => CProverGOTO.Expr.symbol "" .Empty - let calleeExpr := CProverGOTO.Expr.symbol procName .Empty + let calleeExpr := CProverGOTO.Expr.symbol procName + (CProverGOTO.Ty.mkCode (argExprs.map (ยท.type)) lhsExpr.type) let callCode := CProverGOTO.Code.functionCall lhsExpr calleeExpr argExprs let inst : CProverGOTO.Instruction := { type := .FUNCTION_CALL, code := callCode, locationNum := trans.nextLoc } diff --git a/Strata/Backends/CBMC/GOTO/InstToJson.lean b/Strata/Backends/CBMC/GOTO/InstToJson.lean index 357efd36c..966f32515 100644 --- a/Strata/Backends/CBMC/GOTO/InstToJson.lean +++ b/Strata/Backends/CBMC/GOTO/InstToJson.lean @@ -64,6 +64,12 @@ def tyToJson (ty : Ty) : Json := ("id", "array"), ("sub", Json.arr #[tyToJson elemTy]) ] + | { id := .code, .. } => Json.mkObj [ + ("id", "code"), + ("namedSub", Json.mkObj [ + ("parameters", Json.mkObj [("sub", Json.arr #[])]), + ("return_type", Json.mkObj [("id", "empty")])]) + ] | _ => Json.mkObj [("id", "unknown")] /-- Convert `Expr` to JSON format -/ diff --git a/Strata/Backends/CBMC/GOTO/Type.lean b/Strata/Backends/CBMC/GOTO/Type.lean index 2be696ce7..9fc868550 100644 --- a/Strata/Backends/CBMC/GOTO/Type.lean +++ b/Strata/Backends/CBMC/GOTO/Type.lean @@ -74,6 +74,8 @@ inductive Identifier where | structTag (name : String) /-- Array type with element type -/ | array + /-- Code (function) type -/ + | code deriving Repr, Inhabited, DecidableEq instance : ToFormat Identifier where @@ -82,6 +84,7 @@ instance : ToFormat Identifier where | .bitVector bv => f!"{bv}" | .structTag name => f!"struct_tag({name})" | .array => f!"array" + | .code => f!"code" end Ty @@ -181,6 +184,11 @@ def StructTag (name : _root_.String) : Ty := def Array (elemTy : Ty) : Ty := { id := .array, subtypes := [elemTy] } +/-- Code (function) type with parameter types and return type. + Used for FUNCTION_CALL callee symbols. -/ +def mkCode (_paramTypes : List Ty) (_returnType : Ty) : Ty := + { id := .code, subtypes := [] } + end Ty ------------------------------------------------------------------------------- From bf69a46ce1bc2e081fb176d12a4d531b67caa8af Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 25 Mar 2026 18:07:41 +0100 Subject: [PATCH 2/2] Encode parameter and return types in Ty.mkCode mkCode previously discarded parameter and return types (subtypes was empty). Now stores them as subtypes = [returnType] ++ paramTypes, and tyToJson serializes them into proper CBMC code type JSON with parameter sub-nodes and return_type. This gives CBMC accurate function signatures for callee symbols rather than hardcoded empty parameters and void return type. Co-authored-by: Kiro --- Strata/Backends/CBMC/GOTO/InstToJson.lean | 11 +++++++++-- Strata/Backends/CBMC/GOTO/Type.lean | 7 ++++--- 2 files changed, 13 insertions(+), 5 deletions(-) diff --git a/Strata/Backends/CBMC/GOTO/InstToJson.lean b/Strata/Backends/CBMC/GOTO/InstToJson.lean index 966f32515..eb51ab351 100644 --- a/Strata/Backends/CBMC/GOTO/InstToJson.lean +++ b/Strata/Backends/CBMC/GOTO/InstToJson.lean @@ -64,12 +64,19 @@ def tyToJson (ty : Ty) : Json := ("id", "array"), ("sub", Json.arr #[tyToJson elemTy]) ] + | { id := .code, subtypes := retTy :: paramTypes, .. } => + let paramSubs := paramTypes.map fun pTy => + Json.mkObj [("namedSub", Json.mkObj [("type", tyToJson pTy)])] + Json.mkObj [ + ("id", "code"), + ("namedSub", Json.mkObj [ + ("parameters", Json.mkObj [("sub", Json.arr paramSubs.toArray)]), + ("return_type", tyToJson retTy)])] | { id := .code, .. } => Json.mkObj [ ("id", "code"), ("namedSub", Json.mkObj [ ("parameters", Json.mkObj [("sub", Json.arr #[])]), - ("return_type", Json.mkObj [("id", "empty")])]) - ] + ("return_type", Json.mkObj [("id", "empty")])])] | _ => Json.mkObj [("id", "unknown")] /-- Convert `Expr` to JSON format -/ diff --git a/Strata/Backends/CBMC/GOTO/Type.lean b/Strata/Backends/CBMC/GOTO/Type.lean index 9fc868550..ba774a452 100644 --- a/Strata/Backends/CBMC/GOTO/Type.lean +++ b/Strata/Backends/CBMC/GOTO/Type.lean @@ -185,9 +185,10 @@ def Array (elemTy : Ty) : Ty := { id := .array, subtypes := [elemTy] } /-- Code (function) type with parameter types and return type. - Used for FUNCTION_CALL callee symbols. -/ -def mkCode (_paramTypes : List Ty) (_returnType : Ty) : Ty := - { id := .code, subtypes := [] } + Used for FUNCTION_CALL callee symbols. + Encodes as subtypes = [returnType] ++ paramTypes. -/ +def mkCode (paramTypes : List Ty) (returnType : Ty) : Ty := + { id := .code, subtypes := returnType :: paramTypes } end Ty