Skip to content

Fix FUNCTION_CALL callee type: use code type instead of Empty #659

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
tautschnig merged 4 commits into from
Mar 26, 2026
+24 −1
Merged

Fix FUNCTION_CALL callee type: use code type instead of Empty #659

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
680e02b
Fix FUNCTION_CALL callee type: use code type instead of Empty
tautschnig Mar 25, 2026
bf69a46
Encode parameter and return types in Ty.mkCode
tautschnig Mar 25, 2026
5997d01
Merge branch 'main' into tautschnig/goto-fix-callee-type
joscoh Mar 25, 2026
85af9bc
Merge branch 'main' into tautschnig/goto-fix-callee-type
joscoh Mar 25, 2026
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
3 changes: 2 additions & 1 deletion Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 }
Expand Down
13 changes: 13 additions & 0 deletions Strata/Backends/CBMC/GOTO/InstToJson.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +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")])])]
| _ => Json.mkObj [("id", "unknown")]

/-- Convert `Expr` to JSON format -/
Expand Down
9 changes: 9 additions & 0 deletions Strata/Backends/CBMC/GOTO/Type.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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

Expand Down Expand Up @@ -181,6 +184,12 @@ 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.
Encodes as subtypes = [returnType] ++ paramTypes. -/
def mkCode (paramTypes : List Ty) (returnType : Ty) : Ty :=
{ id := .code, subtypes := returnType :: paramTypes }

end Ty

-------------------------------------------------------------------------------
Expand Down
Loading