Skip to content

Commit

Permalink
[RefC] Object Immortalization and Pre-Generation of Constants (idris-…
Browse files Browse the repository at this point in the history
…lang#3242)

* [RefC] shrink value_header; object imortalized; stock well knwon values.

  * Shrink Value_Header to improve utilization of memory.
  * When refCounter reaches its maximum, the object is immortalized to
    avoid overflow. This immotalization is also used to represent
    statically allocated stock objects.
  * Prepare some commonly seen values and share it to improve memory usage.
  * Added debug code to dump memory stats.

* [RefC] Allocated constants statically; Predefined commonly seen values.

* Commonly seen values such as integers less than 100 are predefined and shared.
* Constant String, Int64, Bits64 and Double values are allocated statically as
  indestructible and shared.

* linter

* [RefC] make constants const.

* cleanup

* cleanup

* update CHANGELOG_NEXT

* [refc][test] revert debugging code

* Refactor constantName function in RefC.idr

Refactor constantName function to return Core String type
and handle unsupported types by throwing InternalError exception.

* lint

* fix typo in support/refc/memoryManagement.c

Co-authored-by: Mathew Polzin <matt.polzin@gmail.com>

* [RefC] erase runtime error of constantName

* [RefC] Fixed the missing case expression coverage.

---------

Co-authored-by: Mathew Polzin <matt.polzin@gmail.com>
  • Loading branch information
2 people authored and andrevidela committed Dec 17, 2024
1 parent 6364532 commit 95e4e0c
Show file tree
Hide file tree
Showing 10 changed files with 400 additions and 203 deletions.
11 changes: 11 additions & 0 deletions CHANGELOG_NEXT.md
Original file line number Diff line number Diff line change
Expand Up @@ -129,6 +129,17 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
* Switch calling conventions based on the number of arguments to avoid limits on
the number of arguments and to reduce stack usage.

* Values that reference counters reaching their maximum limit are immortalized to
prevent counter overflow. This can potentially cause memory leaks, but they
occur rarely and are a better choice than crashing. Since overflow is no longer
a concern, changing refCounter from int to uint16 reduces the size of 'Value_Header'.

* Values often found at runtime, such as integers less than 100 are generate
staticaly and share.

* Constant String, Int64, Bits64 and Double values are allocated statically as
imortal and shared.

#### Chez

* Fixed CSE soundness bug that caused delayed expressions to sometimes be eagerly
Expand Down
110 changes: 86 additions & 24 deletions src/Compiler/RefC/RefC.idr
Original file line number Diff line number Diff line change
Expand Up @@ -142,23 +142,6 @@ cPrimType CharType = "Char"
cPrimType DoubleType = "Double"
cPrimType WorldType = "void"

cConstant : Constant -> String
cConstant (I x) = "idris2_mkInt64("++ showIntMin x ++")"
cConstant (I8 x) = "idris2_mkInt8(INT8_C("++ show x ++"))"
cConstant (I16 x) = "idris2_mkInt16(INT16_C("++ show x ++"))"
cConstant (I32 x) = "idris2_mkInt32(INT32_C("++ show x ++"))"
cConstant (I64 x) = "idris2_mkInt64("++ showInt64Min x ++")"
cConstant (BI x) = "(Value*)idris2_mkIntegerLiteral(\""++ show x ++"\")"
cConstant (B8 x) = "idris2_mkBits8(UINT8_C("++ show x ++"))"
cConstant (B16 x) = "idris2_mkBits16(UINT16_C("++ show x ++"))"
cConstant (B32 x) = "idris2_mkBits32(UINT32_C("++ show x ++"))"
cConstant (B64 x) = "idris2_mkBits64(UINT64_C("++ show x ++"))"
cConstant (Db x) = "idris2_mkDouble("++ show x ++")"
cConstant (Ch x) = "idris2_mkChar("++ escapeChar x ++")"
cConstant (Str x) = "(Value*)idris2_mkString("++ cStringQuoted x ++")"
cConstant (PrT t) = cPrimType t
cConstant WorldVal = "(Value*)NULL"

||| Generate scheme for a primitive function.
cOp : {0 arity : Nat} -> PrimFn arity -> Vect arity String -> String
cOp (Neg ty) [x] = "idris2_negate_" ++ cPrimType ty ++ "(" ++ x ++ ")"
Expand Down Expand Up @@ -211,6 +194,20 @@ data EnvTracker : Type where
data FunctionDefinitions : Type where
data IndentLevel : Type where
data HeaderFiles : Type where
data ConstDef
= CDI64 String
| CDB64 String
| CDDb String
| CDStr String

constantName : ConstDef -> String
constantName = \case
CDI64 x => go "Int64" x
CDB64 x => go "Bits64" x
CDDb x => go "Double" x
CDStr x => go "String" x
where go : String -> String -> String
go x y = "idris2_constant_\{x}_\{y}"

ReuseMap = SortedMap Name String
Owned = SortedSet AVar
Expand Down Expand Up @@ -457,6 +454,7 @@ mutual
-> {auto e : Ref EnvTracker Env}
-> {auto oft : Ref OutfileText Output}
-> {auto il : Ref IndentLevel Nat}
-> {auto _ : Ref ConstDef (SortedMap Constant ConstDef)}
-> Env
-> String -> String -> List Int -> ANF -> TailPositionStatus
-> Core ()
Expand All @@ -479,6 +477,7 @@ mutual
-> {auto oft : Ref OutfileText Output}
-> {auto il : Ref IndentLevel Nat}
-> {auto e : Ref EnvTracker Env}
-> {auto _ : Ref ConstDef (SortedMap Constant ConstDef)}
-> ANF
-> TailPositionStatus
-> Core String
Expand Down Expand Up @@ -557,8 +556,8 @@ mutual
"prim__void", "prim__os", "prim__codegen", "prim__onCollect", "prim__onCollectAny" ]
case p of
NS _ (UN (Basic pn)) =>
unless (elem pn prims) $ throw $ InternalError $ "INTERNAL ERROR: Unknown primitive: " ++ cName p
_ => throw $ InternalError $ "INTERNAL ERROR: Unknown primitive: " ++ cName p
unless (elem pn prims) $ throw $ InternalError $ "[refc] Unknown primitive: " ++ cName p
_ => throw $ InternalError $ "[refc] Unknown primitive: " ++ cName p
emit fc $ "// call to external primitive " ++ cName p
pure $ "idris2_\{cName p}("++ showSep ", " (map varName args) ++")"

Expand Down Expand Up @@ -635,7 +634,44 @@ mutual
emit emptyFC "}"
pure switchReturnVar

cStatementsFromANF (APrimVal fc c) _ = pure $ cConstant c
cStatementsFromANF (APrimVal fc (I x)) tailPosition = cStatementsFromANF (APrimVal fc (I64 $ cast x)) tailPosition
cStatementsFromANF (APrimVal fc c) _ = do
constdefs <- get ConstDef
case lookup c constdefs of
Just cdef => pure "((Value*)&\{constantName cdef})" -- the constant already booked.
Nothing => dyngen
where
orStagen : ConstDef -> Core String
orStagen cdef = do -- booking the constant to generate later
constdefs <- get ConstDef
put ConstDef $ insert c cdef constdefs
pure "((Value*)&\{constantName cdef})" -- the constant already booked.
dyngen : Core String
dyngen = case c of
I x => if x >= 0 && x < 100
then pure "(Value*)(&idris2_predefined_Int64[\{show x}])"
else orStagen $ CDI64 $ cCleanString $ show x
I8 x => pure "idris2_mkInt8(INT8_C(\{show x}))"
I16 x => pure "idris2_mkInt16(INT16_C(\{show x}))"
I32 x => pure "idris2_mkInt32(INT32_C(\{show x}))"
I64 x => if x >= 0 && x < 100
then pure "(Value*)(&idris2_predefined_Int64[\{show x}])"
else orStagen $ CDI64 $ cCleanString $ show x
BI x => if x >= 0 && x < 100
then pure "idris2_getPredefinedInteger(\{show x})"
else pure "idris2_mkIntegerLiteral(\"\{show x}\")"
B8 x => pure "idris2_mkBits8(UINT8_C(\{show x}))"
B16 x => pure "idris2_mkBits16(UINT16_C(\{show x}))"
B32 x => pure "idris2_mkBits32(UINT32_C(\{show x}))"
B64 x => if x >= 0 && x < 100
then pure "(Value*)(&idris2_predefined_Bits64[\{show x}])"
else orStagen $ CDB64 $ show x
Db x => orStagen $ CDDb $ cCleanString $ show x
Ch x => pure "idris2_mkChar(\{escapeChar x})"
Str _ => orStagen $ CDStr !(getNextCounter)
PrT t => pure $ cPrimType t
WorldVal => pure "(NULL /* World */)"

cStatementsFromANF (AErased fc) _ = pure "NULL"
cStatementsFromANF (ACrash fc x) _ = pure "(NULL /* CRASH */)"

Expand Down Expand Up @@ -760,6 +796,7 @@ additionalFFIStub name argTypes retType =

createCFunctions : {auto c : Ref Ctxt Defs}
-> {auto a : Ref ArgCounter Nat}
-> {auto _ : Ref ConstDef (SortedMap Constant ConstDef)}
-> {auto f : Ref FunctionDefinitions (List String)}
-> {auto oft : Ref OutfileText Output}
-> {auto il : Ref IndentLevel Nat}
Expand Down Expand Up @@ -856,17 +893,19 @@ createCFunctions n (MkAForeign ccs fargs ret) = do

decreaseIndentation
emit EmptyFC "}"
_ => assert_total $ idris_crash ("INTERNAL ERROR: FFI not found for " ++ cName n)
_ => throw $ InternalError "[refc] FFI not found for \{cName n}"
-- not really total but this way this internal error does not contaminate everything else

createCFunctions n (MkAError exp) = assert_total $ idris_crash ("INTERNAL ERROR: Error with expression: " ++ show exp)
createCFunctions n (MkAError exp) = throw $ InternalError "[refc] Error with expression: \{show exp}"
-- not really total but this way this internal error does not contaminate everything else


header : {auto c : Ref Ctxt Defs}
-> {auto f : Ref FunctionDefinitions (List String)}
-> {auto o : Ref OutfileText Output}
-> {auto il : Ref IndentLevel Nat}
-> {auto h : Ref HeaderFiles (SortedSet String)}
-> {auto _ : Ref ConstDef (SortedMap Constant ConstDef)}
-> Core ()
header = do
let initLines = """
Expand All @@ -875,9 +914,31 @@ header = do
"""
let headerFiles = SortedSet.toList !(get HeaderFiles)
let headerLines = map (\h => "#include <" ++ h ++ ">\n") headerFiles
fns <- get FunctionDefinitions
update OutfileText (appendL ([initLines] ++ headerLines ++ ["\n// function definitions"] ++ fns))
update OutfileText $ appendL $
[initLines] ++
map (\h => "#include <\{h}>\n") headerFiles ++
["\n// function definitions"] ++
fns ++
["\n// constant value definitions"] ++
map (uncurry genConstant) (SortedMap.toList !(get ConstDef))
where
go : ConstDef -> String -> String -> String -> String
go cdef ty tag v =
"static Value_\{ty} const \{constantName cdef}"
++ " = { IDRIS2_STOCKVAL(\{tag}_TAG), \{v} };"
genConstant : Constant -> ConstDef -> String
genConstant c cdef = case c of
I x => go cdef "Int64" "INT64" (showIntMin x)
I64 x => go cdef "Int64" "INT64" (showInt64Min x)
B64 x => go cdef "Bits64" "BITS64" "UINT64_C(\{show x})"
Db x => go cdef "Double" "DOUBLE" (show x)
Str x => go cdef "String" "STRING" (cStringQuoted x)
_ => "/* bad constant */"





footer : {auto il : Ref IndentLevel Nat}
-> {auto f : Ref OutfileText Output}
Expand Down Expand Up @@ -908,6 +969,7 @@ generateCSourceFile : {auto c : Ref Ctxt Defs}
generateCSourceFile defs outn =
do _ <- newRef ArgCounter 0
_ <- newRef FunctionDefinitions []
_ <- newRef ConstDef Data.SortedMap.empty
_ <- newRef OutfileText DList.Nil
_ <- newRef HeaderFiles empty
_ <- newRef IndentLevel 0
Expand Down
13 changes: 11 additions & 2 deletions support/refc/_datatypes.h
Original file line number Diff line number Diff line change
Expand Up @@ -31,9 +31,16 @@
#define CONDITION_TAG 31

typedef struct {
int refCounter;
int tag;
// Objects that reach the maximum reference count will be immortalized.
// This 'immortalization' feature is also utilized to prevent statically
// allocated objects from being destroyed.
#define IDRIS2_VP_REFCOUNTER_MAX UINT16_MAX
uint16_t refCounter;
uint8_t tag;
uint8_t reserved;
} Value_header;
#define IDRIS2_STOCKVAL(t) \
{ IDRIS2_VP_REFCOUNTER_MAX, t, 0 }

typedef struct {
Value_header header;
Expand Down Expand Up @@ -182,3 +189,5 @@ typedef struct {
Value_header header;
pthread_cond_t *cond;
} Value_Condition;

void idris2_dumpMemoryStats(void);
Loading

0 comments on commit 95e4e0c

Please sign in to comment.