From b1bf43f2421fc9958bd2609f5b4612389f7977c0 Mon Sep 17 00:00:00 2001
From: JTrenerry <105094182+JTrenerry@users.noreply.github.com>
Date: Mon, 25 May 2026 11:05:01 +1000
Subject: [PATCH 01/10] Setup grammar

---
 lib/fe/AbsBasilIR.ml   |  9 +++++++++
 lib/fe/BasilIR.cf      | 10 +++++++++-
 lib/fe/LexBasilIR.mll  |  6 +++---
 lib/fe/ParBasilIR.mly  | 25 ++++++++++++++++++++++---
 lib/fe/PrintBasilIR.ml | 10 ++++++++++
 lib/fe/ShowBasilIR.ml  | 10 ++++++++++
 lib/fe/SkelBasilIR.ml  | 10 ++++++++++
 lib/loadir.ml          | 25 +++++++++++++++++++++++++
 8 files changed, 98 insertions(+), 7 deletions(-)

diff --git a/lib/fe/AbsBasilIR.ml b/lib/fe/AbsBasilIR.ml
index 7826cbd1..03e56438 100644
--- a/lib/fe/AbsBasilIR.ml
+++ b/lib/fe/AbsBasilIR.ml
@@ -116,6 +116,7 @@ and stmt =
  | Stmt_Store of endian * globalIdent * expr * expr * intVal
  | Stmt_DirectCall of lVars * procIdent * openParen * callParams * closeParen
  | Stmt_IndirectCall of expr
+ | Stmt_IntrinCall of lVars * intrinCall * openParen * callParams * closeParen
  | Stmt_Assume of expr
  | Stmt_Guard of expr
  | Stmt_Assert of expr
@@ -156,6 +157,14 @@ and callParams =
    CallParams_Exprs of expr list
  | CallParams_Named of namedCallArg list
 
+and intrinCall =
+   MallocCall
+ | FreeCall
+ | CallocCall
+ | HavocCall
+ | AllocaCall
+ | FreeAllocaCall
+
 and jump =
    Jump_GoTo of openParen * blockIdent list * closeParen
  | Jump_Unreachable
diff --git a/lib/fe/BasilIR.cf b/lib/fe/BasilIR.cf
index 25eeb642..d9bd2328 100644
--- a/lib/fe/BasilIR.cf
+++ b/lib/fe/BasilIR.cf
@@ -164,8 +164,16 @@ separator nonempty NamedCallArg "," ;
 CallParams_Exprs . CallParams ::= [Expr];
 CallParams_Named . CallParams ::= [NamedCallArg];
 
-Stmt_DirectCall . Stmt ::= LVars "call" ProcIdent OpenParen CallParams CloseParen ;
+Stmt_DirectCall   . Stmt ::= LVars "call" ProcIdent OpenParen CallParams CloseParen ;
 Stmt_IndirectCall . Stmt ::= "indirect" "call" Expr ;
+Stmt_IntrinCall   . Stmt ::= LVars IntrinCall OpenParen CallParams CloseParen ;
+
+MallocCall     . IntrinCall ::= "@_malloc";
+FreeCall       . IntrinCall ::= "@_free";
+CallocCall     . IntrinCall ::= "@_calloc";
+HavocCall      . IntrinCall ::= "@_havoc";
+AllocaCall     . IntrinCall ::= "@_alloca";
+FreeAllocaCall . IntrinCall ::= "@_free_alloca";
 
 Stmt_Assume . Stmt ::= "assume" Expr ;
 Stmt_Guard . Stmt ::= "guard" Expr ;
diff --git a/lib/fe/LexBasilIR.mll b/lib/fe/LexBasilIR.mll
index c75cdd1a..6620dfaa 100644
--- a/lib/fe/LexBasilIR.mll
+++ b/lib/fe/LexBasilIR.mll
@@ -7,9 +7,9 @@
 open ParBasilIR
 open Lexing
 
-let symbol_table = Hashtbl.create 10
+let symbol_table = Hashtbl.create 16
 let _ = List.iter (fun (kwd, tok) -> Hashtbl.add symbol_table kwd tok)
-                  [(";", SYMB1);(",", SYMB2);("->", SYMB3);("::", SYMB4);(":", SYMB5);("=", SYMB6);("|", SYMB7);(":=", SYMB8);("mem:=", SYMB9);("_", SYMB10)]
+                  [(";", SYMB1);(",", SYMB2);("->", SYMB3);("::", SYMB4);(":", SYMB5);("=", SYMB6);("|", SYMB7);(":=", SYMB8);("mem:=", SYMB9);("@_malloc", SYMB10);("@_free", SYMB11);("@_calloc", SYMB12);("@_havoc", SYMB13);("@_alloca", SYMB14);("@_free_alloca", SYMB15);("_", SYMB16)]
 
 let resword_table = Hashtbl.create 109
 let _ = List.iter (fun (kwd, tok) -> Hashtbl.add resword_table kwd tok)
@@ -53,7 +53,7 @@ let _idchar = _letter | _digit | ['_' '\'']         (*  identifier character *)
 let _universal = _                                  (* universal: any character *)
 
 (* reserved words consisting of special symbols *)
-let rsyms = ";" | "," | "->" | "::" | ":" | "=" | "|" | ":=" | "mem:=" | "_"
+let rsyms = ";" | "," | "->" | "::" | ":" | "=" | "|" | ":=" | "mem:=" | "@_malloc" | "@_free" | "@_calloc" | "@_havoc" | "@_alloca" | "@_free_alloca" | "_"
 
 (* user-defined token types *)
 let bVTYPE = "bv" _digit +
diff --git a/lib/fe/ParBasilIR.mly b/lib/fe/ParBasilIR.mly
index d47dbb22..36b44e44 100644
--- a/lib/fe/ParBasilIR.mly
+++ b/lib/fe/ParBasilIR.mly
@@ -18,7 +18,13 @@ open Lexing
 %token SYMB7 /* | */
 %token SYMB8 /* := */
 %token SYMB9 /* mem:= */
-%token SYMB10 /* _ */
+%token SYMB10 /* @_malloc */
+%token SYMB11 /* @_free */
+%token SYMB12 /* @_calloc */
+%token SYMB13 /* @_havoc */
+%token SYMB14 /* @_alloca */
+%token SYMB15 /* @_free_alloca */
+%token SYMB16 /* _ */
 
 %token TOK_EOF
 %token <string> TOK_Ident
@@ -45,7 +51,7 @@ open Lexing
 %token <(int * int) * string> TOK_IntegerHex
 %token <(int * int) * string> TOK_IntegerDec
 
-%start pModuleT pDecl_list pBlockIdent_list pLambdaSep pVarModifiers pVarModifiers_list pDecl pTypeT_list pTypeAssign pTypeAssign_list pProcDef pField_list pField pIntType pBoolType pRecordType pPointerType pBVType pMapType pRecordField pRecordField_list pSumCase pSumCase_list pType1 pTypeT pIntVal pBVVal pFieldVal_list pFieldVal pEndian pAssignment pStmt pAssignment_list pLocalVar pLocalVar_list pGlobalVar pGlobalVar_list pVar pLocalVarParen pGlobalVarParen pLocalVarParen_list pNamedCallReturn pNamedCallReturn_list pLVars pNamedCallArg pNamedCallArg_list pCallParams pJump pLVar pLVar_list pBlock_list pStmtWithAttrib pStmtWithAttrib_list pJumpWithAttrib pPhiExpr pPhiExpr_list pPhiAssign pPhiAssign_list pBlock pAttrKeyValue pAttrKeyValue_list pAttribSet pAttr_list pAttr pParams pParams_list pValue pExpr_list pExpr pExpr1 pExpr2 pLambdaDef pBinOp pUnOp pCase pCase_list pFieldAssign pFieldAssign_list pEqOp pBVUnOp pBVBinOp pBVLogicalBinOp pIntBinOp pIntLogicalBinOp pIntrinOp pPointerBinOp pRequireTok pEnsureTok pRelyTok pGuarTok pFunSpec pVarSpec pProgSpec pFunSpec_list pProgSpec_list
+%start pModuleT pDecl_list pBlockIdent_list pLambdaSep pVarModifiers pVarModifiers_list pDecl pTypeT_list pTypeAssign pTypeAssign_list pProcDef pField_list pField pIntType pBoolType pRecordType pPointerType pBVType pMapType pRecordField pRecordField_list pSumCase pSumCase_list pType1 pTypeT pIntVal pBVVal pFieldVal_list pFieldVal pEndian pAssignment pStmt pAssignment_list pLocalVar pLocalVar_list pGlobalVar pGlobalVar_list pVar pLocalVarParen pGlobalVarParen pLocalVarParen_list pNamedCallReturn pNamedCallReturn_list pLVars pNamedCallArg pNamedCallArg_list pCallParams pIntrinCall pJump pLVar pLVar_list pBlock_list pStmtWithAttrib pStmtWithAttrib_list pJumpWithAttrib pPhiExpr pPhiExpr_list pPhiAssign pPhiAssign_list pBlock pAttrKeyValue pAttrKeyValue_list pAttribSet pAttr_list pAttr pParams pParams_list pValue pExpr_list pExpr pExpr1 pExpr2 pLambdaDef pBinOp pUnOp pCase pCase_list pFieldAssign pFieldAssign_list pEqOp pBVUnOp pBVBinOp pBVLogicalBinOp pIntBinOp pIntLogicalBinOp pIntrinOp pPointerBinOp pRequireTok pEnsureTok pRelyTok pGuarTok pFunSpec pVarSpec pProgSpec pFunSpec_list pProgSpec_list
 %type <AbsBasilIR.moduleT> pModuleT
 %type <AbsBasilIR.decl list> pDecl_list
 %type <AbsBasilIR.blockIdent list> pBlockIdent_list
@@ -93,6 +99,7 @@ open Lexing
 %type <AbsBasilIR.namedCallArg> pNamedCallArg
 %type <AbsBasilIR.namedCallArg list> pNamedCallArg_list
 %type <AbsBasilIR.callParams> pCallParams
+%type <AbsBasilIR.intrinCall> pIntrinCall
 %type <AbsBasilIR.jump> pJump
 %type <AbsBasilIR.lVar> pLVar
 %type <AbsBasilIR.lVar list> pLVar_list
@@ -189,6 +196,7 @@ open Lexing
 %type <AbsBasilIR.namedCallArg> namedCallArg
 %type <AbsBasilIR.namedCallArg list> namedCallArg_list
 %type <AbsBasilIR.callParams> callParams
+%type <AbsBasilIR.intrinCall> intrinCall
 %type <AbsBasilIR.jump> jump
 %type <AbsBasilIR.lVar> lVar
 %type <AbsBasilIR.lVar list> lVar_list
@@ -353,6 +361,8 @@ pNamedCallArg_list : namedCallArg_list TOK_EOF { $1 };
 
 pCallParams : callParams TOK_EOF { $1 };
 
+pIntrinCall : intrinCall TOK_EOF { $1 };
+
 pJump : jump TOK_EOF { $1 };
 
 pLVar : lVar TOK_EOF { $1 };
@@ -589,6 +599,7 @@ stmt : KW_nop { Stmt_Nop  }
   | KW_store endian globalIdent expr2 expr intVal { Stmt_Store ($2, $3, $4, $5, $6) }
   | lVars KW_call procIdent openParen callParams closeParen { Stmt_DirectCall ($1, $3, $4, $5, $6) }
   | KW_indirect KW_call expr { Stmt_IndirectCall $3 }
+  | lVars intrinCall openParen callParams closeParen { Stmt_IntrinCall ($1, $2, $3, $4, $5) }
   | KW_assume expr { Stmt_Assume $2 }
   | KW_guard expr { Stmt_Guard $2 }
   | KW_assert expr { Stmt_Assert $2 }
@@ -657,6 +668,14 @@ callParams : expr_list { CallParams_Exprs $1 }
   | namedCallArg_list { CallParams_Named $1 }
   ;
 
+intrinCall : SYMB10 { MallocCall  }
+  | SYMB11 { FreeCall  }
+  | SYMB12 { CallocCall  }
+  | SYMB13 { HavocCall  }
+  | SYMB14 { AllocaCall  }
+  | SYMB15 { FreeAllocaCall  }
+  ;
+
 jump : KW_goto openParen blockIdent_list closeParen { Jump_GoTo ($2, $3, $4) }
   | KW_unreachable { Jump_Unreachable  }
   | KW_return openParen expr_list closeParen { Jump_Return ($2, $3, $4) }
@@ -805,7 +824,7 @@ unOp : bVUnOp { UnOpBVUnOp $1 }
   ;
 
 case : expr SYMB3 expr { CaseCase ($1, $3) }
-  | SYMB10 SYMB3 expr { CaseDefault $3 }
+  | SYMB16 SYMB3 expr { CaseDefault $3 }
   ;
 
 case_list : /* empty */ { []  }
diff --git a/lib/fe/PrintBasilIR.ml b/lib/fe/PrintBasilIR.ml
index 6aaf0f3c..d454046d 100644
--- a/lib/fe/PrintBasilIR.ml
+++ b/lib/fe/PrintBasilIR.ml
@@ -283,6 +283,7 @@ and prtStmt (i:int) (e : AbsBasilIR.stmt) : doc = match e with
   |    AbsBasilIR.Stmt_Store (endian, globalident, expr1, expr2, intval) -> prPrec i 0 (concatD [render "store" ; prtEndian 0 endian ; prtGlobalIdent 0 globalident ; prtExpr 2 expr1 ; prtExpr 0 expr2 ; prtIntVal 0 intval])
   |    AbsBasilIR.Stmt_DirectCall (lvars, procident, openparen, callparams, closeparen) -> prPrec i 0 (concatD [prtLVars 0 lvars ; render "call" ; prtProcIdent 0 procident ; prtOpenParen 0 openparen ; prtCallParams 0 callparams ; prtCloseParen 0 closeparen])
   |    AbsBasilIR.Stmt_IndirectCall expr -> prPrec i 0 (concatD [render "indirect" ; render "call" ; prtExpr 0 expr])
+  |    AbsBasilIR.Stmt_IntrinCall (lvars, intrincall, openparen, callparams, closeparen) -> prPrec i 0 (concatD [prtLVars 0 lvars ; prtIntrinCall 0 intrincall ; prtOpenParen 0 openparen ; prtCallParams 0 callparams ; prtCloseParen 0 closeparen])
   |    AbsBasilIR.Stmt_Assume expr -> prPrec i 0 (concatD [render "assume" ; prtExpr 0 expr])
   |    AbsBasilIR.Stmt_Guard expr -> prPrec i 0 (concatD [render "guard" ; prtExpr 0 expr])
   |    AbsBasilIR.Stmt_Assert expr -> prPrec i 0 (concatD [render "assert" ; prtExpr 0 expr])
@@ -348,6 +349,15 @@ and prtCallParams (i:int) (e : AbsBasilIR.callParams) : doc = match e with
   |    AbsBasilIR.CallParams_Named namedcallargs -> prPrec i 0 (concatD [prtNamedCallArgListBNFC 0 namedcallargs])
 
 
+and prtIntrinCall (i:int) (e : AbsBasilIR.intrinCall) : doc = match e with
+       AbsBasilIR.MallocCall  -> prPrec i 0 (concatD [render "@_malloc"])
+  |    AbsBasilIR.FreeCall  -> prPrec i 0 (concatD [render "@_free"])
+  |    AbsBasilIR.CallocCall  -> prPrec i 0 (concatD [render "@_calloc"])
+  |    AbsBasilIR.HavocCall  -> prPrec i 0 (concatD [render "@_havoc"])
+  |    AbsBasilIR.AllocaCall  -> prPrec i 0 (concatD [render "@_alloca"])
+  |    AbsBasilIR.FreeAllocaCall  -> prPrec i 0 (concatD [render "@_free_alloca"])
+
+
 and prtJump (i:int) (e : AbsBasilIR.jump) : doc = match e with
        AbsBasilIR.Jump_GoTo (openparen, blockidents, closeparen) -> prPrec i 0 (concatD [render "goto" ; prtOpenParen 0 openparen ; prtBlockIdentListBNFC 0 blockidents ; prtCloseParen 0 closeparen])
   |    AbsBasilIR.Jump_Unreachable  -> prPrec i 0 (concatD [render "unreachable"])
diff --git a/lib/fe/ShowBasilIR.ml b/lib/fe/ShowBasilIR.ml
index bb1dc1c6..8e89d023 100644
--- a/lib/fe/ShowBasilIR.ml
+++ b/lib/fe/ShowBasilIR.ml
@@ -176,6 +176,7 @@ and showStmt (e : AbsBasilIR.stmt) : showable = match e with
   |    AbsBasilIR.Stmt_Store (endian, globalident, expr0, expr, intval) -> s2s "Stmt_Store" >> c2s ' ' >> c2s '(' >> showEndian endian  >> s2s ", " >>  showGlobalIdent globalident  >> s2s ", " >>  showExpr expr0  >> s2s ", " >>  showExpr expr  >> s2s ", " >>  showIntVal intval >> c2s ')'
   |    AbsBasilIR.Stmt_DirectCall (lvars, procident, openparen, callparams, closeparen) -> s2s "Stmt_DirectCall" >> c2s ' ' >> c2s '(' >> showLVars lvars  >> s2s ", " >>  showProcIdent procident  >> s2s ", " >>  showOpenParen openparen  >> s2s ", " >>  showCallParams callparams  >> s2s ", " >>  showCloseParen closeparen >> c2s ')'
   |    AbsBasilIR.Stmt_IndirectCall expr -> s2s "Stmt_IndirectCall" >> c2s ' ' >> c2s '(' >> showExpr expr >> c2s ')'
+  |    AbsBasilIR.Stmt_IntrinCall (lvars, intrincall, openparen, callparams, closeparen) -> s2s "Stmt_IntrinCall" >> c2s ' ' >> c2s '(' >> showLVars lvars  >> s2s ", " >>  showIntrinCall intrincall  >> s2s ", " >>  showOpenParen openparen  >> s2s ", " >>  showCallParams callparams  >> s2s ", " >>  showCloseParen closeparen >> c2s ')'
   |    AbsBasilIR.Stmt_Assume expr -> s2s "Stmt_Assume" >> c2s ' ' >> c2s '(' >> showExpr expr >> c2s ')'
   |    AbsBasilIR.Stmt_Guard expr -> s2s "Stmt_Guard" >> c2s ' ' >> c2s '(' >> showExpr expr >> c2s ')'
   |    AbsBasilIR.Stmt_Assert expr -> s2s "Stmt_Assert" >> c2s ' ' >> c2s '(' >> showExpr expr >> c2s ')'
@@ -226,6 +227,15 @@ and showCallParams (e : AbsBasilIR.callParams) : showable = match e with
   |    AbsBasilIR.CallParams_Named namedcallargs -> s2s "CallParams_Named" >> c2s ' ' >> c2s '(' >> showList showNamedCallArg namedcallargs >> c2s ')'
 
 
+and showIntrinCall (e : AbsBasilIR.intrinCall) : showable = match e with
+       AbsBasilIR.MallocCall  -> s2s "MallocCall"
+  |    AbsBasilIR.FreeCall  -> s2s "FreeCall"
+  |    AbsBasilIR.CallocCall  -> s2s "CallocCall"
+  |    AbsBasilIR.HavocCall  -> s2s "HavocCall"
+  |    AbsBasilIR.AllocaCall  -> s2s "AllocaCall"
+  |    AbsBasilIR.FreeAllocaCall  -> s2s "FreeAllocaCall"
+
+
 and showJump (e : AbsBasilIR.jump) : showable = match e with
        AbsBasilIR.Jump_GoTo (openparen, blockidents, closeparen) -> s2s "Jump_GoTo" >> c2s ' ' >> c2s '(' >> showOpenParen openparen  >> s2s ", " >>  showList showBlockIdent blockidents  >> s2s ", " >>  showCloseParen closeparen >> c2s ')'
   |    AbsBasilIR.Jump_Unreachable  -> s2s "Jump_Unreachable"
diff --git a/lib/fe/SkelBasilIR.ml b/lib/fe/SkelBasilIR.ml
index d1012b4d..a2a0adf6 100644
--- a/lib/fe/SkelBasilIR.ml
+++ b/lib/fe/SkelBasilIR.ml
@@ -199,6 +199,7 @@ and transStmt (x : stmt) : result = match x with
   | Stmt_Store (endian, globalident, expr0, expr, intval) -> failure x
   | Stmt_DirectCall (lvars, procident, openparen, callparams, closeparen) -> failure x
   | Stmt_IndirectCall expr -> failure x
+  | Stmt_IntrinCall (lvars, intrincall, openparen, callparams, closeparen) -> failure x
   | Stmt_Assume expr -> failure x
   | Stmt_Guard expr -> failure x
   | Stmt_Assert expr -> failure x
@@ -249,6 +250,15 @@ and transCallParams (x : callParams) : result = match x with
   | CallParams_Named namedcallargs -> failure x
 
 
+and transIntrinCall (x : intrinCall) : result = match x with
+    MallocCall  -> failure x
+  | FreeCall  -> failure x
+  | CallocCall  -> failure x
+  | HavocCall  -> failure x
+  | AllocaCall  -> failure x
+  | FreeAllocaCall  -> failure x
+
+
 and transJump (x : jump) : result = match x with
     Jump_GoTo (openparen, blockidents, closeparen) -> failure x
   | Jump_Unreachable  -> failure x
diff --git a/lib/loadir.ml b/lib/loadir.ml
index 339a0759..8b3cdbc6 100644
--- a/lib/loadir.ml
+++ b/lib/loadir.ml
@@ -730,6 +730,15 @@ module BasilASTLoader = struct
           `Call
             (Instr_IndirectCall
                { target = trans_expr p_st expr; attrib = Attrib.empty }) )
+    | Stmt_IntrinCall (lvars, intrin_call, _, params, _) ->
+        let args = trans_intrin_call_rhs p_st params in
+        let p_st, lhs = trans_intrin_lhs p_st lvars in
+        let name = trans_intrin_call_name intrin_call in
+        (p_st,
+          `Call
+            (Instr_IntrinCall { attrib = Attrib.empty; lhs; name; args}
+            )
+        )
     | Stmt_Assume expr ->
         ( p_st,
           `Stmt
@@ -765,6 +774,22 @@ module BasilASTLoader = struct
         |> List.map (function NamedCallArg1 (li, e) ->
             (unsafe_unsigil (`Local li), trans_expr e))
         |> StringMap.of_list
+    
+  and trans_intrin_call_rhs p_st (x : callParams) =
+    let trans_expr = trans_expr p_st in
+    match x with
+    | CallParams_Exprs exprs ->
+        List.map trans_expr exprs
+    | CallParams_Named nl ->
+      failwith "Named args in Intrin call"
+
+  and trans_intrin_call_name = Stmt.Intrinsic.(function
+    | MallocCall -> Malloc
+    | FreeCall -> Free
+    | CallocCall -> Calloc
+    | HavocCall -> Havoc
+    | AllocaCall -> AllocStack
+    | FreeAllocaCall -> FreeStack)
 
   and trans_intrin_lhs prog (x : lVars) : load_st * Var.t list =
     let vars : Var.t list =

From c4ee88dd3c04686eed3e09e65f95585ddb66f4c7 Mon Sep 17 00:00:00 2001
From: JTrenerry <105094182+JTrenerry@users.noreply.github.com>
Date: Mon, 25 May 2026 11:43:03 +1000
Subject: [PATCH 02/10] changes grammar to include call and type check

---
 .gitignore                   |  3 ++-
 lib/fe/BasilIR.cf            |  2 +-
 lib/fe/ParBasilIR.mly        |  2 +-
 lib/fe/PrintBasilIR.ml       |  2 +-
 lib/lang/stmt.ml             | 19 ++++++++-------
 lib/transforms/type_check.ml | 47 +++++++++++++++++++++++++++++++++++-
 tree-sitter/grammar.bnfc.js  | 17 +++++++++++++
 7 files changed, 78 insertions(+), 14 deletions(-)

diff --git a/.gitignore b/.gitignore
index b26c1fde..0c999af7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -7,4 +7,5 @@ trace.json
 *.dot
 **/*.dot
 
-.vscode/
\ No newline at end of file
+.vscode/
+.helix/
diff --git a/lib/fe/BasilIR.cf b/lib/fe/BasilIR.cf
index d9bd2328..61c350ba 100644
--- a/lib/fe/BasilIR.cf
+++ b/lib/fe/BasilIR.cf
@@ -166,7 +166,7 @@ CallParams_Named . CallParams ::= [NamedCallArg];
 
 Stmt_DirectCall   . Stmt ::= LVars "call" ProcIdent OpenParen CallParams CloseParen ;
 Stmt_IndirectCall . Stmt ::= "indirect" "call" Expr ;
-Stmt_IntrinCall   . Stmt ::= LVars IntrinCall OpenParen CallParams CloseParen ;
+Stmt_IntrinCall   . Stmt ::= LVars "call" IntrinCall OpenParen CallParams CloseParen ;
 
 MallocCall     . IntrinCall ::= "@_malloc";
 FreeCall       . IntrinCall ::= "@_free";
diff --git a/lib/fe/ParBasilIR.mly b/lib/fe/ParBasilIR.mly
index 36b44e44..6a0ca14f 100644
--- a/lib/fe/ParBasilIR.mly
+++ b/lib/fe/ParBasilIR.mly
@@ -599,7 +599,7 @@ stmt : KW_nop { Stmt_Nop  }
   | KW_store endian globalIdent expr2 expr intVal { Stmt_Store ($2, $3, $4, $5, $6) }
   | lVars KW_call procIdent openParen callParams closeParen { Stmt_DirectCall ($1, $3, $4, $5, $6) }
   | KW_indirect KW_call expr { Stmt_IndirectCall $3 }
-  | lVars intrinCall openParen callParams closeParen { Stmt_IntrinCall ($1, $2, $3, $4, $5) }
+  | lVars KW_call intrinCall openParen callParams closeParen { Stmt_IntrinCall ($1, $3, $4, $5, $6) }
   | KW_assume expr { Stmt_Assume $2 }
   | KW_guard expr { Stmt_Guard $2 }
   | KW_assert expr { Stmt_Assert $2 }
diff --git a/lib/fe/PrintBasilIR.ml b/lib/fe/PrintBasilIR.ml
index d454046d..67c6e14e 100644
--- a/lib/fe/PrintBasilIR.ml
+++ b/lib/fe/PrintBasilIR.ml
@@ -283,7 +283,7 @@ and prtStmt (i:int) (e : AbsBasilIR.stmt) : doc = match e with
   |    AbsBasilIR.Stmt_Store (endian, globalident, expr1, expr2, intval) -> prPrec i 0 (concatD [render "store" ; prtEndian 0 endian ; prtGlobalIdent 0 globalident ; prtExpr 2 expr1 ; prtExpr 0 expr2 ; prtIntVal 0 intval])
   |    AbsBasilIR.Stmt_DirectCall (lvars, procident, openparen, callparams, closeparen) -> prPrec i 0 (concatD [prtLVars 0 lvars ; render "call" ; prtProcIdent 0 procident ; prtOpenParen 0 openparen ; prtCallParams 0 callparams ; prtCloseParen 0 closeparen])
   |    AbsBasilIR.Stmt_IndirectCall expr -> prPrec i 0 (concatD [render "indirect" ; render "call" ; prtExpr 0 expr])
-  |    AbsBasilIR.Stmt_IntrinCall (lvars, intrincall, openparen, callparams, closeparen) -> prPrec i 0 (concatD [prtLVars 0 lvars ; prtIntrinCall 0 intrincall ; prtOpenParen 0 openparen ; prtCallParams 0 callparams ; prtCloseParen 0 closeparen])
+  |    AbsBasilIR.Stmt_IntrinCall (lvars, intrincall, openparen, callparams, closeparen) -> prPrec i 0 (concatD [prtLVars 0 lvars ; render "call" ; prtIntrinCall 0 intrincall ; prtOpenParen 0 openparen ; prtCallParams 0 callparams ; prtCloseParen 0 closeparen])
   |    AbsBasilIR.Stmt_Assume expr -> prPrec i 0 (concatD [render "assume" ; prtExpr 0 expr])
   |    AbsBasilIR.Stmt_Guard expr -> prPrec i 0 (concatD [render "guard" ; prtExpr 0 expr])
   |    AbsBasilIR.Stmt_Assert expr -> prPrec i 0 (concatD [render "assert" ; prtExpr 0 expr])
diff --git a/lib/lang/stmt.ml b/lib/lang/stmt.ml
index 0003a776..7d42e191 100644
--- a/lib/lang/stmt.ml
+++ b/lib/lang/stmt.ml
@@ -27,15 +27,16 @@ module Intrinsic = struct
     | "@_free_alloca" -> Some FreeStack
     | _ -> None
 
-  let pretty e =
-    (match e with
-      | Havoc -> "@_havoc"
-      | Malloc -> "@_malloc"
-      | Calloc -> "@_calloc"
-      | Free -> "@_free"
-      | AllocStack -> "@_allcoa"
-      | FreeStack -> "@_free_alloca")
-    |> Containers_pp.text
+  let to_string e =
+    match e with
+    | Havoc -> "@_havoc"
+    | Malloc -> "@_malloc"
+    | Calloc -> "@_calloc"
+    | Free -> "@_free"
+    | AllocStack -> "@_allcoa"
+    | FreeStack -> "@_free_alloca"
+
+  let pretty = Containers_pp.text % to_string
 end
 
 let show_endian = function `Big -> "be" | `Little -> "le"
diff --git a/lib/transforms/type_check.ml b/lib/transforms/type_check.ml
index 61416da5..3b4a4abe 100644
--- a/lib/transforms/type_check.ml
+++ b/lib/transforms/type_check.ml
@@ -263,6 +263,51 @@ let type_check stmt_id block_id expr =
   in
   BasilExpr.cata type_error_alg expr
 
+let check_intrin_call (intrin_call : Stmt.Intrinsic.t) args params =
+  Stmt.Intrinsic.(
+    match intrin_call with
+    | Havoc ->
+        List.fold_left2
+          (fun err lhs rhs ->
+            if Types.equal (Var.typ lhs) (BasilExpr.type_of rhs) then err
+            else TypeError { text = "Type of lhs != rhs in Havoc call" } :: err)
+          [] args params
+    | Malloc | AllocStack | Calloc -> (
+        match (args, params) with
+        | [ size ], [ ptr ] ->
+            let err =
+              if Types.leq (Bitvector 64) (BasilExpr.type_of ptr) then []
+              else
+                [
+                  TypeError
+                    { text = "Wrong type of arg in " ^ to_string intrin_call };
+                ]
+            in
+            if Types.equal (Bitvector 64) (Var.typ size) then err
+            else
+              TypeError
+                { text = "Wrong type of arg in " ^ to_string intrin_call }
+              :: err
+        | _ ->
+            [
+              TypeError
+                { text = "Wrong amount of args in " ^ to_string intrin_call };
+            ])
+    | Free | FreeStack -> (
+        match (args, params) with
+        | [ ptr ], [] ->
+            if Types.leq (Bitvector 64) (Var.typ ptr) then []
+            else
+              [
+                TypeError
+                  { text = "Wrong type of arg in " ^ to_string intrin_call };
+              ]
+        | _ ->
+            [
+              TypeError
+                { text = "Wrong amount of args in " ^ to_string intrin_call };
+            ]))
+
 let check_stmt_types (stmt : Program.stmt) (pt : Program.t) stmt_id block_id =
   let type_err fmt = type_err fmt stmt_id block_id in
   let expect_equal msg a b (s : type_error list) =
@@ -273,7 +318,6 @@ let check_stmt_types (stmt : Program.stmt) (pt : Program.t) stmt_id block_id =
   in
   let type_check = type_check stmt_id block_id in
   match stmt with
-  | Stmt.Instr_IntrinCall _ -> []
   | Stmt.Instr_Assign { al } ->
       al
       |> List.fold_left
@@ -386,6 +430,7 @@ let check_stmt_types (stmt : Program.stmt) (pt : Program.t) stmt_id block_id =
              output)
       in
       params_check
+  | Stmt.Instr_IntrinCall { name; lhs; args } -> check_intrin_call name lhs args
 
 let check_block prog (id, b) =
   Block.stmts_iter b
diff --git a/tree-sitter/grammar.bnfc.js b/tree-sitter/grammar.bnfc.js
index ea073da4..cce972fe 100644
--- a/tree-sitter/grammar.bnfc.js
+++ b/tree-sitter/grammar.bnfc.js
@@ -239,6 +239,8 @@ module.exports = ({
         seq(optional($.LVars), "call", $.token_ProcIdent, $.token_OpenParen, optional($.CallParams), $.token_CloseParen),
         // Stmt_IndirectCall. Stmt ::= "indirect" "call" Expr ;
         seq("indirect", "call", $.Expr),
+        // Stmt_IntrinCall. Stmt ::= LVars "call" IntrinCall OpenParen CallParams CloseParen ;
+        seq(optional($.LVars), "call", $.IntrinCall, $.token_OpenParen, optional($.CallParams), $.token_CloseParen),
         // Stmt_Assume. Stmt ::= "assume" Expr ;
         seq("assume", $.Expr),
         // Stmt_Guard. Stmt ::= "guard" Expr ;
@@ -351,6 +353,21 @@ module.exports = ({
         // CallParams_Named. CallParams ::= [NamedCallArg] ;
         $.list_NamedCallArg
       ),
+    IntrinCall: $ =>
+      choice(
+        // MallocCall. IntrinCall ::= "@_malloc" ;
+        "@_malloc",
+        // FreeCall. IntrinCall ::= "@_free" ;
+        "@_free",
+        // CallocCall. IntrinCall ::= "@_calloc" ;
+        "@_calloc",
+        // HavocCall. IntrinCall ::= "@_havoc" ;
+        "@_havoc",
+        // AllocaCall. IntrinCall ::= "@_alloca" ;
+        "@_alloca",
+        // FreeAllocaCall. IntrinCall ::= "@_free_alloca" ;
+        "@_free_alloca"
+      ),
     Jump: $ =>
       choice(
         // Jump_GoTo. Jump ::= "goto" OpenParen [BlockIdent] CloseParen ;

From 27df95d11f41cee6948ff0dc26b89f312b6d7acd Mon Sep 17 00:00:00 2001
From: JTrenerry <105094182+JTrenerry@users.noreply.github.com>
Date: Mon, 25 May 2026 12:11:52 +1000
Subject: [PATCH 03/10] parse test

---
 lib/lang/stmt.ml             | 4 ++--
 lib/transforms/type_check.ml | 2 +-
 test/cram/dune               | 1 +
 test/cram/roundtrip.sexp     | 3 +++
 test/cram/roundtrip.t        | 8 ++++++++
 5 files changed, 15 insertions(+), 3 deletions(-)

diff --git a/lib/lang/stmt.ml b/lib/lang/stmt.ml
index 7d42e191..fa555b33 100644
--- a/lib/lang/stmt.ml
+++ b/lib/lang/stmt.ml
@@ -23,7 +23,7 @@ module Intrinsic = struct
     | "@_malloc" -> Some Malloc
     | "@_calloc" -> Some Calloc
     | "@_free" -> Some Free
-    | "@_allcoa" -> Some AllocStack
+    | "@_alloca" -> Some AllocStack
     | "@_free_alloca" -> Some FreeStack
     | _ -> None
 
@@ -33,7 +33,7 @@ module Intrinsic = struct
     | Malloc -> "@_malloc"
     | Calloc -> "@_calloc"
     | Free -> "@_free"
-    | AllocStack -> "@_allcoa"
+    | AllocStack -> "@_alloca"
     | FreeStack -> "@_free_alloca"
 
   let pretty = Containers_pp.text % to_string
diff --git a/lib/transforms/type_check.ml b/lib/transforms/type_check.ml
index 3b4a4abe..3179159e 100644
--- a/lib/transforms/type_check.ml
+++ b/lib/transforms/type_check.ml
@@ -295,7 +295,7 @@ let check_intrin_call (intrin_call : Stmt.Intrinsic.t) args params =
             ])
     | Free | FreeStack -> (
         match (args, params) with
-        | [ ptr ], [] ->
+        | [ ptr ], [ err ] ->
             if Types.leq (Bitvector 64) (Var.typ ptr) then []
             else
               [
diff --git a/test/cram/dune b/test/cram/dune
index 398f1e65..75ef7a6a 100644
--- a/test/cram/dune
+++ b/test/cram/dune
@@ -18,6 +18,7 @@
   ssa-multi-deps.il
   memassign.il
   ptrrec1.il
+  intrin_before.il
   ../../examples/sqrt.il
   ../../examples/irreducible_loop_1.il
   ../../examples/cat.il
diff --git a/test/cram/roundtrip.sexp b/test/cram/roundtrip.sexp
index 545d40b3..de91f7a4 100644
--- a/test/cram/roundtrip.sexp
+++ b/test/cram/roundtrip.sexp
@@ -16,3 +16,6 @@
 (dump-il "ptrrec2.il")
 (load-il "ptrrec2.il")
 (dump-il "ptrrec3.il")
+
+(load-il "intrin_before.il")
+(dump-il "intrin_after.il")
diff --git a/test/cram/roundtrip.t b/test/cram/roundtrip.t
index d64b890b..8fdb2f95 100644
--- a/test/cram/roundtrip.t
+++ b/test/cram/roundtrip.t
@@ -16,6 +16,8 @@
   (dump-il ptrrec2.il)
   (load-il ptrrec2.il)
   (dump-il ptrrec3.il)
+  (load-il intrin_before.il)
+  (dump-il intrin_after.il)
 
 The serialise -> parse serialise loop should be idempotent
 
@@ -84,6 +86,12 @@ Record and Pointer
   [1]
   $ diff ptrrec2.il ptrrec3.il
 
+Intrin Calls
+
+  $ diff intrin_before.il intrin_after.il
+  6a7
+  >   
+  [1]
 
 Examples Directory
 

From 3632bb4f8afc0816ac78162e15b4bd9c78c48d40 Mon Sep 17 00:00:00 2001
From: JTrenerry <105094182+JTrenerry@users.noreply.github.com>
Date: Mon, 25 May 2026 14:43:43 +1000
Subject: [PATCH 04/10] does the transform

---
 lib/lang/stmt.ml                       |  10 +--
 lib/passes.ml                          |   8 ++
 lib/transforms/dune                    |   1 +
 lib/transforms/intrin_call.ml          | 102 +++++++++++++++++++++++++
 lib/transforms/memory_specification.ml |   7 +-
 lib/transforms/type_check.ml           |  10 +--
 6 files changed, 122 insertions(+), 16 deletions(-)
 create mode 100644 lib/transforms/intrin_call.ml

diff --git a/lib/lang/stmt.ml b/lib/lang/stmt.ml
index fa555b33..265d0d0f 100644
--- a/lib/lang/stmt.ml
+++ b/lib/lang/stmt.ml
@@ -19,11 +19,11 @@ module Intrinsic = struct
 
   let of_string e =
     match e with
-    | "@_havoc" -> Some Havoc
-    | "@_malloc" -> Some Malloc
-    | "@_calloc" -> Some Calloc
-    | "@_free" -> Some Free
-    | "@_alloca" -> Some AllocStack
+    | "@_havoc" | "@havoc" | "@#havoc" -> Some Havoc
+    | "@_malloc" | "@malloc" | "@#malloc" -> Some Malloc
+    | "@_calloc" | "@calloc" | "@zmalloc" -> Some Calloc
+    | "@_free" | "@free" | "@#free" -> Some Free
+    | "@_alloca" | "@alloca" -> Some AllocStack
     | "@_free_alloca" -> Some FreeStack
     | _ -> None
 
diff --git a/lib/passes.ml b/lib/passes.ml
index 02a12a9e..8666b980 100644
--- a/lib/passes.ml
+++ b/lib/passes.ml
@@ -290,6 +290,14 @@ module PassManager = struct
          cleaning stack address uses. Assumes SSA.";
     }
 
+  let intrin_call =
+    {
+      name = "intrin-call";
+      apply = Prog Transforms.Intrin_call.transform;
+      doc =
+        "Replaces special calls like malloc and free with intrin calls instead";
+    }
+
   let simp =
     {
       name = "simplify";
diff --git a/lib/transforms/dune b/lib/transforms/dune
index b0cd38a1..87a7e137 100644
--- a/lib/transforms/dune
+++ b/lib/transforms/dune
@@ -14,6 +14,7 @@
   memory_specification
   function_summaries
   boogie_prepass
+  intrin_call
   gamma_vars
   const_prop
   linear_copy)
diff --git a/lib/transforms/intrin_call.ml b/lib/transforms/intrin_call.ml
new file mode 100644
index 00000000..1761b8a0
--- /dev/null
+++ b/lib/transforms/intrin_call.ml
@@ -0,0 +1,102 @@
+open Bincaml_util.Common
+open Lang
+open Expr
+
+let transform_proc proc prog =
+  let replace_call (stmt : Program.stmt) : Program.stmt Iter.t =
+    match stmt with
+    | Stmt.Instr_Call { procid; lhs; args; attrib } -> (
+        match ID.name procid with
+        | ( "@malloc" | "@#malloc" | "@calloc" | "@alloca" | "@_malloc"
+          | "@_calloc" | "@_alloca" ) as name ->
+            let modifies =
+              List.filter
+                (fun var -> not @@ String.equal (Var.name var) "R0")
+                (Procedure.specification (Program.proc prog procid))
+                  .modifies_globs
+            in
+            let lhs =
+              StringMap.filter (fun name _ -> String.equal name "R0") lhs
+              |> StringMap.values |> List.of_iter
+            in
+            let args =
+              StringMap.filter (fun name _ -> String.equal name "R0") args
+              |> StringMap.values |> List.of_iter
+            in
+            Iter.doubleton
+              (Stmt.Instr_IntrinCall
+                 {
+                   name =
+                     Option.get_exn_or "Unreachable"
+                     @@ Stmt.Intrinsic.of_string name;
+                   lhs;
+                   args;
+                   attrib;
+                 })
+              (Stmt.Instr_IntrinCall
+                 {
+                   name = Stmt.Intrinsic.Havoc;
+                   lhs = modifies;
+                   args = [];
+                   attrib = Attrib.empty;
+                 })
+        | ("@#free" | "@free" | "@_free") as name ->
+            let modifies =
+              (Procedure.specification (Program.proc prog procid))
+                .modifies_globs
+            in
+            let lhs = StringMap.values lhs |> List.of_iter in
+            let args =
+              StringMap.filter (fun name _ -> String.equal name "R0") args
+              |> StringMap.values |> List.of_iter
+            in
+            Iter.doubleton
+              (Stmt.Instr_IntrinCall
+                 {
+                   name =
+                     Option.get_exn_or "Unreachable"
+                     @@ Stmt.Intrinsic.of_string name;
+                   lhs;
+                   args;
+                   attrib;
+                 })
+              (Stmt.Instr_IntrinCall
+                 {
+                   name = Stmt.Intrinsic.Havoc;
+                   lhs = modifies;
+                   args = [];
+                   attrib = Attrib.empty;
+                 })
+        | ("@#havoc" | "@havoc" | "@_havoc") as name ->
+            let modifies =
+              (Procedure.specification (Program.proc prog procid))
+                .modifies_globs
+            in
+            let lhs = StringMap.values lhs |> List.of_iter in
+            Iter.doubleton
+              (Stmt.Instr_IntrinCall
+                 {
+                   name =
+                     Option.get_exn_or "Unreachable"
+                     @@ Stmt.Intrinsic.of_string name;
+                   lhs;
+                   args = [];
+                   attrib;
+                 })
+              (Stmt.Instr_IntrinCall
+                 {
+                   name = Stmt.Intrinsic.Havoc;
+                   lhs = modifies;
+                   args = [];
+                   attrib = Attrib.empty;
+                 })
+        | _ -> Iter.singleton stmt)
+    | _ -> Iter.singleton stmt
+  in
+  let open BasilExpr in
+  Procedure.map_blocks_topo_fwd
+    (fun _ b -> Block.flat_map ~phi:id replace_call b)
+    proc
+
+let transform (prog : Program.t) =
+  Program.map_procedures (fun pid proc -> transform_proc proc prog) prog
diff --git a/lib/transforms/memory_specification.ml b/lib/transforms/memory_specification.ml
index 96d472f0..cafb9e31 100644
--- a/lib/transforms/memory_specification.ml
+++ b/lib/transforms/memory_specification.ml
@@ -168,11 +168,8 @@ let transform_proc entry _ (p : Program.proc) =
     match name with
     | "@main" -> transform_main p
     | e when String.equal entry e -> transform_main p
-    | "@malloc" -> transform_malloc p
-    | "@free" -> transform_free p
-    | "@#malloc" -> transform_malloc p
-    | "@zmalloc" -> transform_malloc p
-    | "@#free" -> transform_free p
+    | "@malloc" | "@#malloc" | "@zmalloc" -> transform_malloc p
+    | "@free" | "@#free" -> transform_free p
     | _ -> p
 
 let transform (p : Program.t) =
diff --git a/lib/transforms/type_check.ml b/lib/transforms/type_check.ml
index 3179159e..56cddd3d 100644
--- a/lib/transforms/type_check.ml
+++ b/lib/transforms/type_check.ml
@@ -266,12 +266,10 @@ let type_check stmt_id block_id expr =
 let check_intrin_call (intrin_call : Stmt.Intrinsic.t) args params =
   Stmt.Intrinsic.(
     match intrin_call with
-    | Havoc ->
-        List.fold_left2
-          (fun err lhs rhs ->
-            if Types.equal (Var.typ lhs) (BasilExpr.type_of rhs) then err
-            else TypeError { text = "Type of lhs != rhs in Havoc call" } :: err)
-          [] args params
+    | Havoc -> (
+        match params with
+        | [] -> []
+        | _ -> [ TypeError { text = "Havoc should not have args" } ])
     | Malloc | AllocStack | Calloc -> (
         match (args, params) with
         | [ size ], [ ptr ] ->

From 6954856530dc47aa341a96fc5425d1d67ca4350d Mon Sep 17 00:00:00 2001
From: JTrenerry <105094182+JTrenerry@users.noreply.github.com>
Date: Mon, 25 May 2026 15:18:59 +1000
Subject: [PATCH 05/10] minimal test

---
 lib/fe/AbsBasilIR.ml          |  9 -------
 lib/fe/BasilIR.cf             |  8 ------
 lib/fe/LexBasilIR.mll         |  6 ++---
 lib/fe/ParBasilIR.mly         | 25 +++----------------
 lib/fe/PrintBasilIR.ml        | 10 --------
 lib/fe/ShowBasilIR.ml         | 10 --------
 lib/fe/SkelBasilIR.ml         | 10 --------
 lib/lang/stmt.ml              | 10 ++++----
 lib/loadir.ml                 | 17 -------------
 lib/passes.ml                 |  1 +
 lib/transforms/intrin_call.ml | 47 ++++++++++++++---------------------
 test/cram/dune                |  2 ++
 test/cram/intrin_call.sexp    |  3 +++
 test/cram/intrin_call.t       |  2 ++
 tree-sitter/grammar.bnfc.js   | 17 -------------
 15 files changed, 38 insertions(+), 139 deletions(-)
 create mode 100644 test/cram/intrin_call.sexp
 create mode 100644 test/cram/intrin_call.t

diff --git a/lib/fe/AbsBasilIR.ml b/lib/fe/AbsBasilIR.ml
index 03e56438..7826cbd1 100644
--- a/lib/fe/AbsBasilIR.ml
+++ b/lib/fe/AbsBasilIR.ml
@@ -116,7 +116,6 @@ and stmt =
  | Stmt_Store of endian * globalIdent * expr * expr * intVal
  | Stmt_DirectCall of lVars * procIdent * openParen * callParams * closeParen
  | Stmt_IndirectCall of expr
- | Stmt_IntrinCall of lVars * intrinCall * openParen * callParams * closeParen
  | Stmt_Assume of expr
  | Stmt_Guard of expr
  | Stmt_Assert of expr
@@ -157,14 +156,6 @@ and callParams =
    CallParams_Exprs of expr list
  | CallParams_Named of namedCallArg list
 
-and intrinCall =
-   MallocCall
- | FreeCall
- | CallocCall
- | HavocCall
- | AllocaCall
- | FreeAllocaCall
-
 and jump =
    Jump_GoTo of openParen * blockIdent list * closeParen
  | Jump_Unreachable
diff --git a/lib/fe/BasilIR.cf b/lib/fe/BasilIR.cf
index 61c350ba..aa186959 100644
--- a/lib/fe/BasilIR.cf
+++ b/lib/fe/BasilIR.cf
@@ -166,14 +166,6 @@ CallParams_Named . CallParams ::= [NamedCallArg];
 
 Stmt_DirectCall   . Stmt ::= LVars "call" ProcIdent OpenParen CallParams CloseParen ;
 Stmt_IndirectCall . Stmt ::= "indirect" "call" Expr ;
-Stmt_IntrinCall   . Stmt ::= LVars "call" IntrinCall OpenParen CallParams CloseParen ;
-
-MallocCall     . IntrinCall ::= "@_malloc";
-FreeCall       . IntrinCall ::= "@_free";
-CallocCall     . IntrinCall ::= "@_calloc";
-HavocCall      . IntrinCall ::= "@_havoc";
-AllocaCall     . IntrinCall ::= "@_alloca";
-FreeAllocaCall . IntrinCall ::= "@_free_alloca";
 
 Stmt_Assume . Stmt ::= "assume" Expr ;
 Stmt_Guard . Stmt ::= "guard" Expr ;
diff --git a/lib/fe/LexBasilIR.mll b/lib/fe/LexBasilIR.mll
index 6620dfaa..c75cdd1a 100644
--- a/lib/fe/LexBasilIR.mll
+++ b/lib/fe/LexBasilIR.mll
@@ -7,9 +7,9 @@
 open ParBasilIR
 open Lexing
 
-let symbol_table = Hashtbl.create 16
+let symbol_table = Hashtbl.create 10
 let _ = List.iter (fun (kwd, tok) -> Hashtbl.add symbol_table kwd tok)
-                  [(";", SYMB1);(",", SYMB2);("->", SYMB3);("::", SYMB4);(":", SYMB5);("=", SYMB6);("|", SYMB7);(":=", SYMB8);("mem:=", SYMB9);("@_malloc", SYMB10);("@_free", SYMB11);("@_calloc", SYMB12);("@_havoc", SYMB13);("@_alloca", SYMB14);("@_free_alloca", SYMB15);("_", SYMB16)]
+                  [(";", SYMB1);(",", SYMB2);("->", SYMB3);("::", SYMB4);(":", SYMB5);("=", SYMB6);("|", SYMB7);(":=", SYMB8);("mem:=", SYMB9);("_", SYMB10)]
 
 let resword_table = Hashtbl.create 109
 let _ = List.iter (fun (kwd, tok) -> Hashtbl.add resword_table kwd tok)
@@ -53,7 +53,7 @@ let _idchar = _letter | _digit | ['_' '\'']         (*  identifier character *)
 let _universal = _                                  (* universal: any character *)
 
 (* reserved words consisting of special symbols *)
-let rsyms = ";" | "," | "->" | "::" | ":" | "=" | "|" | ":=" | "mem:=" | "@_malloc" | "@_free" | "@_calloc" | "@_havoc" | "@_alloca" | "@_free_alloca" | "_"
+let rsyms = ";" | "," | "->" | "::" | ":" | "=" | "|" | ":=" | "mem:=" | "_"
 
 (* user-defined token types *)
 let bVTYPE = "bv" _digit +
diff --git a/lib/fe/ParBasilIR.mly b/lib/fe/ParBasilIR.mly
index 6a0ca14f..d47dbb22 100644
--- a/lib/fe/ParBasilIR.mly
+++ b/lib/fe/ParBasilIR.mly
@@ -18,13 +18,7 @@ open Lexing
 %token SYMB7 /* | */
 %token SYMB8 /* := */
 %token SYMB9 /* mem:= */
-%token SYMB10 /* @_malloc */
-%token SYMB11 /* @_free */
-%token SYMB12 /* @_calloc */
-%token SYMB13 /* @_havoc */
-%token SYMB14 /* @_alloca */
-%token SYMB15 /* @_free_alloca */
-%token SYMB16 /* _ */
+%token SYMB10 /* _ */
 
 %token TOK_EOF
 %token <string> TOK_Ident
@@ -51,7 +45,7 @@ open Lexing
 %token <(int * int) * string> TOK_IntegerHex
 %token <(int * int) * string> TOK_IntegerDec
 
-%start pModuleT pDecl_list pBlockIdent_list pLambdaSep pVarModifiers pVarModifiers_list pDecl pTypeT_list pTypeAssign pTypeAssign_list pProcDef pField_list pField pIntType pBoolType pRecordType pPointerType pBVType pMapType pRecordField pRecordField_list pSumCase pSumCase_list pType1 pTypeT pIntVal pBVVal pFieldVal_list pFieldVal pEndian pAssignment pStmt pAssignment_list pLocalVar pLocalVar_list pGlobalVar pGlobalVar_list pVar pLocalVarParen pGlobalVarParen pLocalVarParen_list pNamedCallReturn pNamedCallReturn_list pLVars pNamedCallArg pNamedCallArg_list pCallParams pIntrinCall pJump pLVar pLVar_list pBlock_list pStmtWithAttrib pStmtWithAttrib_list pJumpWithAttrib pPhiExpr pPhiExpr_list pPhiAssign pPhiAssign_list pBlock pAttrKeyValue pAttrKeyValue_list pAttribSet pAttr_list pAttr pParams pParams_list pValue pExpr_list pExpr pExpr1 pExpr2 pLambdaDef pBinOp pUnOp pCase pCase_list pFieldAssign pFieldAssign_list pEqOp pBVUnOp pBVBinOp pBVLogicalBinOp pIntBinOp pIntLogicalBinOp pIntrinOp pPointerBinOp pRequireTok pEnsureTok pRelyTok pGuarTok pFunSpec pVarSpec pProgSpec pFunSpec_list pProgSpec_list
+%start pModuleT pDecl_list pBlockIdent_list pLambdaSep pVarModifiers pVarModifiers_list pDecl pTypeT_list pTypeAssign pTypeAssign_list pProcDef pField_list pField pIntType pBoolType pRecordType pPointerType pBVType pMapType pRecordField pRecordField_list pSumCase pSumCase_list pType1 pTypeT pIntVal pBVVal pFieldVal_list pFieldVal pEndian pAssignment pStmt pAssignment_list pLocalVar pLocalVar_list pGlobalVar pGlobalVar_list pVar pLocalVarParen pGlobalVarParen pLocalVarParen_list pNamedCallReturn pNamedCallReturn_list pLVars pNamedCallArg pNamedCallArg_list pCallParams pJump pLVar pLVar_list pBlock_list pStmtWithAttrib pStmtWithAttrib_list pJumpWithAttrib pPhiExpr pPhiExpr_list pPhiAssign pPhiAssign_list pBlock pAttrKeyValue pAttrKeyValue_list pAttribSet pAttr_list pAttr pParams pParams_list pValue pExpr_list pExpr pExpr1 pExpr2 pLambdaDef pBinOp pUnOp pCase pCase_list pFieldAssign pFieldAssign_list pEqOp pBVUnOp pBVBinOp pBVLogicalBinOp pIntBinOp pIntLogicalBinOp pIntrinOp pPointerBinOp pRequireTok pEnsureTok pRelyTok pGuarTok pFunSpec pVarSpec pProgSpec pFunSpec_list pProgSpec_list
 %type <AbsBasilIR.moduleT> pModuleT
 %type <AbsBasilIR.decl list> pDecl_list
 %type <AbsBasilIR.blockIdent list> pBlockIdent_list
@@ -99,7 +93,6 @@ open Lexing
 %type <AbsBasilIR.namedCallArg> pNamedCallArg
 %type <AbsBasilIR.namedCallArg list> pNamedCallArg_list
 %type <AbsBasilIR.callParams> pCallParams
-%type <AbsBasilIR.intrinCall> pIntrinCall
 %type <AbsBasilIR.jump> pJump
 %type <AbsBasilIR.lVar> pLVar
 %type <AbsBasilIR.lVar list> pLVar_list
@@ -196,7 +189,6 @@ open Lexing
 %type <AbsBasilIR.namedCallArg> namedCallArg
 %type <AbsBasilIR.namedCallArg list> namedCallArg_list
 %type <AbsBasilIR.callParams> callParams
-%type <AbsBasilIR.intrinCall> intrinCall
 %type <AbsBasilIR.jump> jump
 %type <AbsBasilIR.lVar> lVar
 %type <AbsBasilIR.lVar list> lVar_list
@@ -361,8 +353,6 @@ pNamedCallArg_list : namedCallArg_list TOK_EOF { $1 };
 
 pCallParams : callParams TOK_EOF { $1 };
 
-pIntrinCall : intrinCall TOK_EOF { $1 };
-
 pJump : jump TOK_EOF { $1 };
 
 pLVar : lVar TOK_EOF { $1 };
@@ -599,7 +589,6 @@ stmt : KW_nop { Stmt_Nop  }
   | KW_store endian globalIdent expr2 expr intVal { Stmt_Store ($2, $3, $4, $5, $6) }
   | lVars KW_call procIdent openParen callParams closeParen { Stmt_DirectCall ($1, $3, $4, $5, $6) }
   | KW_indirect KW_call expr { Stmt_IndirectCall $3 }
-  | lVars KW_call intrinCall openParen callParams closeParen { Stmt_IntrinCall ($1, $3, $4, $5, $6) }
   | KW_assume expr { Stmt_Assume $2 }
   | KW_guard expr { Stmt_Guard $2 }
   | KW_assert expr { Stmt_Assert $2 }
@@ -668,14 +657,6 @@ callParams : expr_list { CallParams_Exprs $1 }
   | namedCallArg_list { CallParams_Named $1 }
   ;
 
-intrinCall : SYMB10 { MallocCall  }
-  | SYMB11 { FreeCall  }
-  | SYMB12 { CallocCall  }
-  | SYMB13 { HavocCall  }
-  | SYMB14 { AllocaCall  }
-  | SYMB15 { FreeAllocaCall  }
-  ;
-
 jump : KW_goto openParen blockIdent_list closeParen { Jump_GoTo ($2, $3, $4) }
   | KW_unreachable { Jump_Unreachable  }
   | KW_return openParen expr_list closeParen { Jump_Return ($2, $3, $4) }
@@ -824,7 +805,7 @@ unOp : bVUnOp { UnOpBVUnOp $1 }
   ;
 
 case : expr SYMB3 expr { CaseCase ($1, $3) }
-  | SYMB16 SYMB3 expr { CaseDefault $3 }
+  | SYMB10 SYMB3 expr { CaseDefault $3 }
   ;
 
 case_list : /* empty */ { []  }
diff --git a/lib/fe/PrintBasilIR.ml b/lib/fe/PrintBasilIR.ml
index 67c6e14e..6aaf0f3c 100644
--- a/lib/fe/PrintBasilIR.ml
+++ b/lib/fe/PrintBasilIR.ml
@@ -283,7 +283,6 @@ and prtStmt (i:int) (e : AbsBasilIR.stmt) : doc = match e with
   |    AbsBasilIR.Stmt_Store (endian, globalident, expr1, expr2, intval) -> prPrec i 0 (concatD [render "store" ; prtEndian 0 endian ; prtGlobalIdent 0 globalident ; prtExpr 2 expr1 ; prtExpr 0 expr2 ; prtIntVal 0 intval])
   |    AbsBasilIR.Stmt_DirectCall (lvars, procident, openparen, callparams, closeparen) -> prPrec i 0 (concatD [prtLVars 0 lvars ; render "call" ; prtProcIdent 0 procident ; prtOpenParen 0 openparen ; prtCallParams 0 callparams ; prtCloseParen 0 closeparen])
   |    AbsBasilIR.Stmt_IndirectCall expr -> prPrec i 0 (concatD [render "indirect" ; render "call" ; prtExpr 0 expr])
-  |    AbsBasilIR.Stmt_IntrinCall (lvars, intrincall, openparen, callparams, closeparen) -> prPrec i 0 (concatD [prtLVars 0 lvars ; render "call" ; prtIntrinCall 0 intrincall ; prtOpenParen 0 openparen ; prtCallParams 0 callparams ; prtCloseParen 0 closeparen])
   |    AbsBasilIR.Stmt_Assume expr -> prPrec i 0 (concatD [render "assume" ; prtExpr 0 expr])
   |    AbsBasilIR.Stmt_Guard expr -> prPrec i 0 (concatD [render "guard" ; prtExpr 0 expr])
   |    AbsBasilIR.Stmt_Assert expr -> prPrec i 0 (concatD [render "assert" ; prtExpr 0 expr])
@@ -349,15 +348,6 @@ and prtCallParams (i:int) (e : AbsBasilIR.callParams) : doc = match e with
   |    AbsBasilIR.CallParams_Named namedcallargs -> prPrec i 0 (concatD [prtNamedCallArgListBNFC 0 namedcallargs])
 
 
-and prtIntrinCall (i:int) (e : AbsBasilIR.intrinCall) : doc = match e with
-       AbsBasilIR.MallocCall  -> prPrec i 0 (concatD [render "@_malloc"])
-  |    AbsBasilIR.FreeCall  -> prPrec i 0 (concatD [render "@_free"])
-  |    AbsBasilIR.CallocCall  -> prPrec i 0 (concatD [render "@_calloc"])
-  |    AbsBasilIR.HavocCall  -> prPrec i 0 (concatD [render "@_havoc"])
-  |    AbsBasilIR.AllocaCall  -> prPrec i 0 (concatD [render "@_alloca"])
-  |    AbsBasilIR.FreeAllocaCall  -> prPrec i 0 (concatD [render "@_free_alloca"])
-
-
 and prtJump (i:int) (e : AbsBasilIR.jump) : doc = match e with
        AbsBasilIR.Jump_GoTo (openparen, blockidents, closeparen) -> prPrec i 0 (concatD [render "goto" ; prtOpenParen 0 openparen ; prtBlockIdentListBNFC 0 blockidents ; prtCloseParen 0 closeparen])
   |    AbsBasilIR.Jump_Unreachable  -> prPrec i 0 (concatD [render "unreachable"])
diff --git a/lib/fe/ShowBasilIR.ml b/lib/fe/ShowBasilIR.ml
index 8e89d023..bb1dc1c6 100644
--- a/lib/fe/ShowBasilIR.ml
+++ b/lib/fe/ShowBasilIR.ml
@@ -176,7 +176,6 @@ and showStmt (e : AbsBasilIR.stmt) : showable = match e with
   |    AbsBasilIR.Stmt_Store (endian, globalident, expr0, expr, intval) -> s2s "Stmt_Store" >> c2s ' ' >> c2s '(' >> showEndian endian  >> s2s ", " >>  showGlobalIdent globalident  >> s2s ", " >>  showExpr expr0  >> s2s ", " >>  showExpr expr  >> s2s ", " >>  showIntVal intval >> c2s ')'
   |    AbsBasilIR.Stmt_DirectCall (lvars, procident, openparen, callparams, closeparen) -> s2s "Stmt_DirectCall" >> c2s ' ' >> c2s '(' >> showLVars lvars  >> s2s ", " >>  showProcIdent procident  >> s2s ", " >>  showOpenParen openparen  >> s2s ", " >>  showCallParams callparams  >> s2s ", " >>  showCloseParen closeparen >> c2s ')'
   |    AbsBasilIR.Stmt_IndirectCall expr -> s2s "Stmt_IndirectCall" >> c2s ' ' >> c2s '(' >> showExpr expr >> c2s ')'
-  |    AbsBasilIR.Stmt_IntrinCall (lvars, intrincall, openparen, callparams, closeparen) -> s2s "Stmt_IntrinCall" >> c2s ' ' >> c2s '(' >> showLVars lvars  >> s2s ", " >>  showIntrinCall intrincall  >> s2s ", " >>  showOpenParen openparen  >> s2s ", " >>  showCallParams callparams  >> s2s ", " >>  showCloseParen closeparen >> c2s ')'
   |    AbsBasilIR.Stmt_Assume expr -> s2s "Stmt_Assume" >> c2s ' ' >> c2s '(' >> showExpr expr >> c2s ')'
   |    AbsBasilIR.Stmt_Guard expr -> s2s "Stmt_Guard" >> c2s ' ' >> c2s '(' >> showExpr expr >> c2s ')'
   |    AbsBasilIR.Stmt_Assert expr -> s2s "Stmt_Assert" >> c2s ' ' >> c2s '(' >> showExpr expr >> c2s ')'
@@ -227,15 +226,6 @@ and showCallParams (e : AbsBasilIR.callParams) : showable = match e with
   |    AbsBasilIR.CallParams_Named namedcallargs -> s2s "CallParams_Named" >> c2s ' ' >> c2s '(' >> showList showNamedCallArg namedcallargs >> c2s ')'
 
 
-and showIntrinCall (e : AbsBasilIR.intrinCall) : showable = match e with
-       AbsBasilIR.MallocCall  -> s2s "MallocCall"
-  |    AbsBasilIR.FreeCall  -> s2s "FreeCall"
-  |    AbsBasilIR.CallocCall  -> s2s "CallocCall"
-  |    AbsBasilIR.HavocCall  -> s2s "HavocCall"
-  |    AbsBasilIR.AllocaCall  -> s2s "AllocaCall"
-  |    AbsBasilIR.FreeAllocaCall  -> s2s "FreeAllocaCall"
-
-
 and showJump (e : AbsBasilIR.jump) : showable = match e with
        AbsBasilIR.Jump_GoTo (openparen, blockidents, closeparen) -> s2s "Jump_GoTo" >> c2s ' ' >> c2s '(' >> showOpenParen openparen  >> s2s ", " >>  showList showBlockIdent blockidents  >> s2s ", " >>  showCloseParen closeparen >> c2s ')'
   |    AbsBasilIR.Jump_Unreachable  -> s2s "Jump_Unreachable"
diff --git a/lib/fe/SkelBasilIR.ml b/lib/fe/SkelBasilIR.ml
index a2a0adf6..d1012b4d 100644
--- a/lib/fe/SkelBasilIR.ml
+++ b/lib/fe/SkelBasilIR.ml
@@ -199,7 +199,6 @@ and transStmt (x : stmt) : result = match x with
   | Stmt_Store (endian, globalident, expr0, expr, intval) -> failure x
   | Stmt_DirectCall (lvars, procident, openparen, callparams, closeparen) -> failure x
   | Stmt_IndirectCall expr -> failure x
-  | Stmt_IntrinCall (lvars, intrincall, openparen, callparams, closeparen) -> failure x
   | Stmt_Assume expr -> failure x
   | Stmt_Guard expr -> failure x
   | Stmt_Assert expr -> failure x
@@ -250,15 +249,6 @@ and transCallParams (x : callParams) : result = match x with
   | CallParams_Named namedcallargs -> failure x
 
 
-and transIntrinCall (x : intrinCall) : result = match x with
-    MallocCall  -> failure x
-  | FreeCall  -> failure x
-  | CallocCall  -> failure x
-  | HavocCall  -> failure x
-  | AllocaCall  -> failure x
-  | FreeAllocaCall  -> failure x
-
-
 and transJump (x : jump) : result = match x with
     Jump_GoTo (openparen, blockidents, closeparen) -> failure x
   | Jump_Unreachable  -> failure x
diff --git a/lib/lang/stmt.ml b/lib/lang/stmt.ml
index 265d0d0f..fa555b33 100644
--- a/lib/lang/stmt.ml
+++ b/lib/lang/stmt.ml
@@ -19,11 +19,11 @@ module Intrinsic = struct
 
   let of_string e =
     match e with
-    | "@_havoc" | "@havoc" | "@#havoc" -> Some Havoc
-    | "@_malloc" | "@malloc" | "@#malloc" -> Some Malloc
-    | "@_calloc" | "@calloc" | "@zmalloc" -> Some Calloc
-    | "@_free" | "@free" | "@#free" -> Some Free
-    | "@_alloca" | "@alloca" -> Some AllocStack
+    | "@_havoc" -> Some Havoc
+    | "@_malloc" -> Some Malloc
+    | "@_calloc" -> Some Calloc
+    | "@_free" -> Some Free
+    | "@_alloca" -> Some AllocStack
     | "@_free_alloca" -> Some FreeStack
     | _ -> None
 
diff --git a/lib/loadir.ml b/lib/loadir.ml
index 8b3cdbc6..4d6a14b2 100644
--- a/lib/loadir.ml
+++ b/lib/loadir.ml
@@ -730,15 +730,6 @@ module BasilASTLoader = struct
           `Call
             (Instr_IndirectCall
                { target = trans_expr p_st expr; attrib = Attrib.empty }) )
-    | Stmt_IntrinCall (lvars, intrin_call, _, params, _) ->
-        let args = trans_intrin_call_rhs p_st params in
-        let p_st, lhs = trans_intrin_lhs p_st lvars in
-        let name = trans_intrin_call_name intrin_call in
-        (p_st,
-          `Call
-            (Instr_IntrinCall { attrib = Attrib.empty; lhs; name; args}
-            )
-        )
     | Stmt_Assume expr ->
         ( p_st,
           `Stmt
@@ -783,14 +774,6 @@ module BasilASTLoader = struct
     | CallParams_Named nl ->
       failwith "Named args in Intrin call"
 
-  and trans_intrin_call_name = Stmt.Intrinsic.(function
-    | MallocCall -> Malloc
-    | FreeCall -> Free
-    | CallocCall -> Calloc
-    | HavocCall -> Havoc
-    | AllocaCall -> AllocStack
-    | FreeAllocaCall -> FreeStack)
-
   and trans_intrin_lhs prog (x : lVars) : load_st * Var.t list =
     let vars : Var.t list =
       match x with
diff --git a/lib/passes.ml b/lib/passes.ml
index 8666b980..d00afa87 100644
--- a/lib/passes.ml
+++ b/lib/passes.ml
@@ -345,6 +345,7 @@ module PassManager = struct
       read_uninit false;
       read_uninit true;
       sssa;
+      intrin_call;
       sva;
       full_ssa;
       type_check;
diff --git a/lib/transforms/intrin_call.ml b/lib/transforms/intrin_call.ml
index 1761b8a0..6ad2dfcb 100644
--- a/lib/transforms/intrin_call.ml
+++ b/lib/transforms/intrin_call.ml
@@ -2,6 +2,15 @@ open Bincaml_util.Common
 open Lang
 open Expr
 
+let string_to_intrin =
+  Stmt.Intrinsic.(
+    function
+    | "@malloc" | "@#malloc" | "@_malloc" -> Malloc
+    | "@calloc" | "@_calloc" | "@zmalloc" -> Calloc
+    | "@alloca" | "@_alloca" -> AllocStack
+    | "@free" | "@#free" | "@_free" -> Free
+    | _ -> failwith "Unreachable")
+
 let transform_proc proc prog =
   let replace_call (stmt : Program.stmt) : Program.stmt Iter.t =
     match stmt with
@@ -11,28 +20,22 @@ let transform_proc proc prog =
           | "@_calloc" | "@_alloca" ) as name ->
             let modifies =
               List.filter
-                (fun var -> not @@ String.equal (Var.name var) "R0")
+                (fun var ->
+                  not @@ String.starts_with (Var.name var) ~prefix:"R0")
                 (Procedure.specification (Program.proc prog procid))
                   .modifies_globs
             in
             let lhs =
-              StringMap.filter (fun name _ -> String.equal name "R0") lhs
+              StringMap.filter (fun name _ -> String.starts_with name ~prefix:"R0") lhs
               |> StringMap.values |> List.of_iter
             in
             let args =
-              StringMap.filter (fun name _ -> String.equal name "R0") args
+              StringMap.filter (fun name _ -> String.starts_with name ~prefix:"R0") args
               |> StringMap.values |> List.of_iter
             in
             Iter.doubleton
               (Stmt.Instr_IntrinCall
-                 {
-                   name =
-                     Option.get_exn_or "Unreachable"
-                     @@ Stmt.Intrinsic.of_string name;
-                   lhs;
-                   args;
-                   attrib;
-                 })
+                 { name = string_to_intrin name; lhs; args; attrib })
               (Stmt.Instr_IntrinCall
                  {
                    name = Stmt.Intrinsic.Havoc;
@@ -47,19 +50,14 @@ let transform_proc proc prog =
             in
             let lhs = StringMap.values lhs |> List.of_iter in
             let args =
-              StringMap.filter (fun name _ -> String.equal name "R0") args
+              StringMap.filter
+                (fun name _ -> String.starts_with name ~prefix:"R0")
+                args
               |> StringMap.values |> List.of_iter
             in
             Iter.doubleton
               (Stmt.Instr_IntrinCall
-                 {
-                   name =
-                     Option.get_exn_or "Unreachable"
-                     @@ Stmt.Intrinsic.of_string name;
-                   lhs;
-                   args;
-                   attrib;
-                 })
+                 { name = string_to_intrin name; lhs; args; attrib })
               (Stmt.Instr_IntrinCall
                  {
                    name = Stmt.Intrinsic.Havoc;
@@ -75,14 +73,7 @@ let transform_proc proc prog =
             let lhs = StringMap.values lhs |> List.of_iter in
             Iter.doubleton
               (Stmt.Instr_IntrinCall
-                 {
-                   name =
-                     Option.get_exn_or "Unreachable"
-                     @@ Stmt.Intrinsic.of_string name;
-                   lhs;
-                   args = [];
-                   attrib;
-                 })
+                 { name = string_to_intrin name; lhs; args = []; attrib })
               (Stmt.Instr_IntrinCall
                  {
                    name = Stmt.Intrinsic.Havoc;
diff --git a/test/cram/dune b/test/cram/dune
index 75ef7a6a..c1071cdd 100644
--- a/test/cram/dune
+++ b/test/cram/dune
@@ -48,6 +48,8 @@
   ll_spec.sexp
   repeated_ssa.il
   repeated_ssa.sexp
+  intrin_call.sexp
+  ../../examples/memory/malloc_free.il
   ../../bin/main.exe))
 
 (cram
diff --git a/test/cram/intrin_call.sexp b/test/cram/intrin_call.sexp
new file mode 100644
index 00000000..62633236
--- /dev/null
+++ b/test/cram/intrin_call.sexp
@@ -0,0 +1,3 @@
+(load-il "../../examples/memory/malloc_free.il")
+(run-transforms "intrin-call")
+(dump-il "after.il")
diff --git a/test/cram/intrin_call.t b/test/cram/intrin_call.t
new file mode 100644
index 00000000..ac9f22a5
--- /dev/null
+++ b/test/cram/intrin_call.t
@@ -0,0 +1,2 @@
+  $ bincaml script intrin_call.sexp
+  $ cat after.il
diff --git a/tree-sitter/grammar.bnfc.js b/tree-sitter/grammar.bnfc.js
index cce972fe..ea073da4 100644
--- a/tree-sitter/grammar.bnfc.js
+++ b/tree-sitter/grammar.bnfc.js
@@ -239,8 +239,6 @@ module.exports = ({
         seq(optional($.LVars), "call", $.token_ProcIdent, $.token_OpenParen, optional($.CallParams), $.token_CloseParen),
         // Stmt_IndirectCall. Stmt ::= "indirect" "call" Expr ;
         seq("indirect", "call", $.Expr),
-        // Stmt_IntrinCall. Stmt ::= LVars "call" IntrinCall OpenParen CallParams CloseParen ;
-        seq(optional($.LVars), "call", $.IntrinCall, $.token_OpenParen, optional($.CallParams), $.token_CloseParen),
         // Stmt_Assume. Stmt ::= "assume" Expr ;
         seq("assume", $.Expr),
         // Stmt_Guard. Stmt ::= "guard" Expr ;
@@ -353,21 +351,6 @@ module.exports = ({
         // CallParams_Named. CallParams ::= [NamedCallArg] ;
         $.list_NamedCallArg
       ),
-    IntrinCall: $ =>
-      choice(
-        // MallocCall. IntrinCall ::= "@_malloc" ;
-        "@_malloc",
-        // FreeCall. IntrinCall ::= "@_free" ;
-        "@_free",
-        // CallocCall. IntrinCall ::= "@_calloc" ;
-        "@_calloc",
-        // HavocCall. IntrinCall ::= "@_havoc" ;
-        "@_havoc",
-        // AllocaCall. IntrinCall ::= "@_alloca" ;
-        "@_alloca",
-        // FreeAllocaCall. IntrinCall ::= "@_free_alloca" ;
-        "@_free_alloca"
-      ),
     Jump: $ =>
       choice(
         // Jump_GoTo. Jump ::= "goto" OpenParen [BlockIdent] CloseParen ;

From 161ed122282a9b8fdbd1da274eccefb4666d8b83 Mon Sep 17 00:00:00 2001
From: JTrenerry <105094182+JTrenerry@users.noreply.github.com>
Date: Mon, 25 May 2026 15:19:32 +1000
Subject: [PATCH 06/10] promo

---
 test/cram/intrin_call.t | 61 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 61 insertions(+)

diff --git a/test/cram/intrin_call.t b/test/cram/intrin_call.t
index ac9f22a5..26e932ef 100644
--- a/test/cram/intrin_call.t
+++ b/test/cram/intrin_call.t
@@ -1,2 +1,63 @@
   $ bincaml script intrin_call.sexp
+  (load-il ../../examples/memory/malloc_free.il)
+  (run-transforms intrin-call)
+  (dump-il after.il)
   $ cat after.il
+  var observable $mem:(bv64->bv8);
+  var $stack:(bv64->bv8);
+  proc @main_2276(R0_in:bv64, R16_in:bv64, R17_in:bv64, R1_in:bv64, R29_in:bv64,
+     R30_in:bv64, R31_in:bv64, _PC_in:bv64)
+     -> (R0_out:bv64, R17_out:bv64, R1_out:bv64, R29_out:bv64, R30_out:bv64) { .address = 2276;
+      .name = "main"; .returnBlock = "main_return" }
+    modifies $mem:(bv64->bv8), $stack:(bv64->bv8)
+    captures $mem:(bv64->bv8), $stack:(bv64->bv8)
+  
+  [
+     block %main_entry [
+       $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd(R31_in:bv64,
+        0xffffffffffffffe0:bv64) R29_in:bv64 64;
+       $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd(R31_in:bv64,
+        0xffffffffffffffe8:bv64) R30_in:bv64 64;
+       var Exp14__5_2_1:bv64 := load le $mem:(bv64->bv8) 0x20010:bv64 64;
+       assert true;
+       (var R0_3:bv64):= call @_malloc(0x1:bv64);
+       ($mem:(bv64->bv8), $stack:(bv64->bv8)):= call @_havoc();
+       goto (%phi_5);
+     ];
+     block %phi_5 [
+       $stack:(bv64->bv8) := store le $stack:(bv64->bv8) bvadd(R31_in:bv64,
+        0xfffffffffffffff8:bv64) R0_3:bv64 64;
+       var Exp14__5_21_1:bv64 := load le $stack:(bv64->bv8) bvadd(R31_in:bv64,
+        0xfffffffffffffff8:bv64) 64;
+       $mem:(bv64->bv8) := store le $mem:(bv64->bv8) Exp14__5_21_1:bv64 0x79:bv8 8;
+       var Exp14__5_22_1:bv64 := load le $stack:(bv64->bv8) bvadd(R31_in:bv64,
+        0xfffffffffffffff8:bv64) 64;
+       var Exp14__5_1_1:bv64 := load le $mem:(bv64->bv8) 0x20028:bv64 64;
+       assert true;
+       call @_free(Exp14__5_22_1:bv64);
+       ($mem:(bv64->bv8), $stack:(bv64->bv8)):= call @_havoc();
+       goto (%phi_6);
+     ];
+     block %phi_6 [
+       var Exp16__5_24_1:bv64 := load le $stack:(bv64->bv8) bvadd(R31_in:bv64,
+        0xffffffffffffffe0:bv64) 64;
+       var Exp18__5_25_1:bv64 := load le $stack:(bv64->bv8) bvadd(R31_in:bv64,
+        0xffffffffffffffe8:bv64) 64;
+       goto (%main_return);
+     ];
+     block %main_return [
+       (var R0_out:bv64 := 0x0:bv64, var R17_out:bv64 := Exp14__5_1_1:bv64,
+        var R1_out:bv64 := 0x79:bv64, var R29_out:bv64 := Exp16__5_24_1:bv64,
+        var R30_out:bv64 := Exp18__5_25_1:bv64);
+       return;
+     ]
+  ];
+  proc @malloc(R0_in:bv64)  -> (R0_out:bv64) { .name = "malloc" }
+    modifies $mem:(bv64->bv8), $stack:(bv64->bv8)
+    captures $mem:(bv64->bv8), $stack:(bv64->bv8)
+  ;
+  proc @#free(R0_in:bv64)  -> () { .name = "#free" }
+    modifies $mem:(bv64->bv8), $stack:(bv64->bv8)
+    captures $mem:(bv64->bv8), $stack:(bv64->bv8)
+  ;
+  prog entry @main_2276;

From 5d8e204d5f0af23ed4a4cd7bfbe5bde02334d9dd Mon Sep 17 00:00:00 2001
From: JTrenerry <105094182+JTrenerry@users.noreply.github.com>
Date: Mon, 25 May 2026 15:24:13 +1000
Subject: [PATCH 07/10] remove output of free

---
 lib/transforms/type_check.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/transforms/type_check.ml b/lib/transforms/type_check.ml
index 56cddd3d..2a6cd849 100644
--- a/lib/transforms/type_check.ml
+++ b/lib/transforms/type_check.ml
@@ -293,7 +293,7 @@ let check_intrin_call (intrin_call : Stmt.Intrinsic.t) args params =
             ])
     | Free | FreeStack -> (
         match (args, params) with
-        | [ ptr ], [ err ] ->
+        | [ ptr ], [ ] ->
             if Types.leq (Bitvector 64) (Var.typ ptr) then []
             else
               [

From 2ded50c83e5cd21f7b860e24fa786e5565dfcd86 Mon Sep 17 00:00:00 2001
From: JTrenerry <105094182+JTrenerry@users.noreply.github.com>
Date: Mon, 25 May 2026 15:25:32 +1000
Subject: [PATCH 08/10] remove unused func

---
 lib/loadir.ml | 8 --------
 1 file changed, 8 deletions(-)

diff --git a/lib/loadir.ml b/lib/loadir.ml
index 4d6a14b2..71d87083 100644
--- a/lib/loadir.ml
+++ b/lib/loadir.ml
@@ -766,14 +766,6 @@ module BasilASTLoader = struct
             (unsafe_unsigil (`Local li), trans_expr e))
         |> StringMap.of_list
     
-  and trans_intrin_call_rhs p_st (x : callParams) =
-    let trans_expr = trans_expr p_st in
-    match x with
-    | CallParams_Exprs exprs ->
-        List.map trans_expr exprs
-    | CallParams_Named nl ->
-      failwith "Named args in Intrin call"
-
   and trans_intrin_lhs prog (x : lVars) : load_st * Var.t list =
     let vars : Var.t list =
       match x with

From 13020d94d72af3212817361c327811f9486415ce Mon Sep 17 00:00:00 2001
From: JTrenerry <105094182+JTrenerry@users.noreply.github.com>
Date: Mon, 25 May 2026 15:29:56 +1000
Subject: [PATCH 09/10] was hidden by gitignore :(

---
 test/cram/intrin_before.il | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100644 test/cram/intrin_before.il

diff --git a/test/cram/intrin_before.il b/test/cram/intrin_before.il
new file mode 100644
index 00000000..4044cf86
--- /dev/null
+++ b/test/cram/intrin_before.il
@@ -0,0 +1,25 @@
+proc @main_4196164(R0_in:bv64, R10_in:bv64, R11_in:bv64, R12_in:bv64, R13_in:bv64,
+   R14_in:bv64, R15_in:bv64, R16_in:bv64, R17_in:bv64, R18_in:bv64, R1_in:bv64,
+   R29_in:bv64, R2_in:bv64, R30_in:bv64, R31_in:bv64, R3_in:bv64, R4_in:bv64,
+   R5_in:bv64, R6_in:bv64, R7_in:bv64, R8_in:bv64, R9_in:bv64, _PC_in:bv64)
+   -> (R0_out:bv64, R1_out:bv64) { .address = 4196164; .name = "main";
+    .returnBlock = "main_return" }
+
+[
+   block %main_entry [
+     var as:bv64 := 0x32:bv64;
+     (var x_2:bv64, var x_3:bv64, var addr:bv64):= call @_havoc();
+     (var ptr0:bv64):= call @_malloc(as:bv64);
+     (var ptr1:bv64):= call @_calloc(as:bv64);
+     call @_free(ptr0:bv64);
+     call @_free(ptr1:bv64);
+     (var stack_ptr:bv64):= call @_alloca(as:bv64);
+     call @_free_alloca(stack_ptr:bv64);
+     goto (%main_return);
+   ];
+   block %main_return [
+     (var R0_out:bv64 := 0x0:bv64, var R1_out:bv64 := 0x2a:bv64);
+     return;
+   ]
+];
+prog entry @main_4196164;
\ No newline at end of file

From 7e6da3715d190dc6954f356ad101c6e8dd0a06f3 Mon Sep 17 00:00:00 2001
From: JTrenerry <105094182+JTrenerry@users.noreply.github.com>
Date: Mon, 25 May 2026 15:36:19 +1000
Subject: [PATCH 10/10] fmt

---
 lib/loadir.ml                 | 2 +-
 lib/transforms/intrin_call.ml | 8 ++++++--
 lib/transforms/type_check.ml  | 2 +-
 3 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/lib/loadir.ml b/lib/loadir.ml
index 71d87083..339a0759 100644
--- a/lib/loadir.ml
+++ b/lib/loadir.ml
@@ -765,7 +765,7 @@ module BasilASTLoader = struct
         |> List.map (function NamedCallArg1 (li, e) ->
             (unsafe_unsigil (`Local li), trans_expr e))
         |> StringMap.of_list
-    
+
   and trans_intrin_lhs prog (x : lVars) : load_st * Var.t list =
     let vars : Var.t list =
       match x with
diff --git a/lib/transforms/intrin_call.ml b/lib/transforms/intrin_call.ml
index 6ad2dfcb..ae778787 100644
--- a/lib/transforms/intrin_call.ml
+++ b/lib/transforms/intrin_call.ml
@@ -26,11 +26,15 @@ let transform_proc proc prog =
                   .modifies_globs
             in
             let lhs =
-              StringMap.filter (fun name _ -> String.starts_with name ~prefix:"R0") lhs
+              StringMap.filter
+                (fun name _ -> String.starts_with name ~prefix:"R0")
+                lhs
               |> StringMap.values |> List.of_iter
             in
             let args =
-              StringMap.filter (fun name _ -> String.starts_with name ~prefix:"R0") args
+              StringMap.filter
+                (fun name _ -> String.starts_with name ~prefix:"R0")
+                args
               |> StringMap.values |> List.of_iter
             in
             Iter.doubleton
diff --git a/lib/transforms/type_check.ml b/lib/transforms/type_check.ml
index 2a6cd849..d849b7cc 100644
--- a/lib/transforms/type_check.ml
+++ b/lib/transforms/type_check.ml
@@ -293,7 +293,7 @@ let check_intrin_call (intrin_call : Stmt.Intrinsic.t) args params =
             ])
     | Free | FreeStack -> (
         match (args, params) with
-        | [ ptr ], [ ] ->
+        | [ ptr ], [] ->
             if Types.leq (Bitvector 64) (Var.typ ptr) then []
             else
               [