Interpreter.dcl 5.88 KB
Newer Older
1 2
definition module ABC.Interpreter

3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25
/**
 * This module defines types and functions to use an interpreter for the ABC
 * language for cross-platform (de)serialization of lazy expressions.
 *
 * Currently, functionality is limited to 64-bit platforms, because ABC code
 * generated for 32-bit platforms is different.
 *
 * You need to set certain project options to use this library.
 *
 * When using cpm, set the following in your project file:
 *  - ByteCode: path for the main bytecode file (e.g. {Project}*app.bc)
 *  - CodeGen/GenerateByteCode: True
 *  - CodeGen/OptimiseABC: True (unless you suspect a bug in the ABC optimiser)
 *  - Link/StripByteCode: False (because we need symbols in the bytecode)
 *  - Link/GenerateSymbolTable: True (because we need symbols in the executable)
 *
 * In the Clean IDE, you can set these options in two panes:
 *  - Project options > Linker (GenerateSymbolTable)
 *  - Project options > Bytecode (all other options)
 *
 * There is currently no support for bytecode generation in clm.
 */

Camil Staps's avatar
Camil Staps committed
26
from StdMaybe import :: Maybe
27

28 29 30 31
/**
 * This type describes settings used by the interpreter to deserialize
 * expressions. You may also use {{`defaultDeserializationSettings`}}.
 */
32
:: DeserializationSettings =
33 34
	{ heap_size  :: !Int //* Heap size for the interpreter, in bytes (default: 2M)
	, stack_size :: !Int //* Stack size for the interpreter, in bytes (default: 1M in total; 500k for A and 500k for BC stack)
35 36 37 38
	}

defaultDeserializationSettings :: DeserializationSettings

39 40 41 42 43 44
/**
 * A serialized expression.
 * Use {{`graphToString`}} and {{`graphFromString`}} to convert this to and
 * from strings, or use {{`graphToFile`}} and {{`graphFromFile`}} to read/write
 * this from/to files.
 */
45
:: *SerializedGraph
46

47 48 49
/**
 * This is an internal type.
 */
50
:: InterpretedExpression
51 52 53 54

/**
 * This is an internal type.
 */
55 56
:: *InterpretationEnvironment

57 58 59 60 61 62 63 64 65
/**
 * Serialize an expression for interpretation.
 *
 * @param The value to serialize.
 * @param The path to the executable's bytecode (set by the `ByteCode` option in the project file).
 * @result The result may be `Nothing` if the bytecode could not be parsed.
 */
serialize :: a !String !*World -> *(!Maybe SerializedGraph, !*World)

66
/**
Camil Staps's avatar
Camil Staps committed
67
 * Serialize an expression for prelinked interpretation. This is a mode of
68 69 70 71 72
 * interpretation where the code and data addresses are fixed. It is useful for
 * the WebAssembly interpreter where memory always starts at index 0.
 *
 * @param The value to serialize.
 * @param The path to the executable's bytecode (set by the `ByteCode` option in the project file).
Camil Staps's avatar
Camil Staps committed
73
 * @param The path to the executable itself.
74 75
 * @result The result may be `Nothing` if the bytecode could not be parsed.
 */
Camil Staps's avatar
Camil Staps committed
76
serialize_for_prelinked_interpretation :: a !String !String !*World -> *(!Maybe String, !*World)
77

78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96
/**
 * Deserialize an expression using the ABC interpreter.
 * This version copies nodes as soon as they are in head normal form.
 * Therefore, the result is only `Nothing` when pre-interpretation validation
 * has failed (e.g., when the bytecode could not be parsed). If an
 * interpretation error occurs this will most likely crash the host program.
 * For more safety, see {{`deserialize_strict`}}.
 *
 * @param Settings for the interpreter.
 * @param The graph to deserialize. Should be obtained using {{`serialize`}}.
 * @param The path to the current executable (needed to resolve symbols when copying the result).
 * @result The result may be `Nothing` when pre-interpretation validation has failed.
 */
deserialize :: !DeserializationSettings !SerializedGraph !String !*World -> *(!Maybe a, !*World)

/**
 * This type represents several different run-time errors that may occur when
 * deserializing an expression in strict mode (see {{`deserialize_strict`}}).
 */
97 98
:: DeserializedValue a
	= DV_ParseError
99
		//* The bytecode or serialized graph could not be parsed.
100

101
	| DV_HeapFull
102 103 104 105
		//* The interpreter had not enough heap to evaluate the expression.
	| DV_StackOverflow
		//* The interpreter had not enough stack to evaluate the expression.
		//* NB: on Windows, not all stack overflows can be caught.
106
	| DV_Halt
107
		//* The ABC instruction `halt` was encountered.
108
	| DV_IllegalInstruction
109
		//* A forbidden (ccall, etc.) or unknown ABC instruction was encountered.
110
	| DV_HostHeapFull
111
		//* The heap of the host application has not enough space to copy the result.
112

113
	| DV_Ok !a
114
		//* Deserialization succeeded.
115

116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138
/**
 * Deserialize an expression using the ABC interpreter.
 * This version evaluates the node to a normal form (unlike {{`deserialize`}},
 * which copies the result as soon as it is in head normal form). This allows
 * the interpreter to catch run-time errors (signaled in the
 * {{`DeserializedValue`}} type), so you can use this function for sandboxing.
 *
 * @param Settings for the interpreter.
 * @param The graph to deserialize. Should be obtained using {{`serialize`}}.
 * @param The path to the current executable (needed to resolve symbols when copying the result).
 */
deserialize_strict :: !DeserializationSettings !SerializedGraph !String !*World -> *(!DeserializedValue a, !*World)

/**
 * Deserialize the `Start` rule of a Clean application in bytecode format.
 * This is essentially the same as {{`deserialize`}}, but it always interprets
 * the start rule instead of a custom serialized graph.
 *
 * @param Settings for the interpreter.
 * @param The path to the bytecode file to run (set by the `ByteCode` option in the project file).
 * @param The path to the current executable (needed to resolve symbols when copying the result).
 * @result The result may be `Nothing` when the bytecode cannot be parsed.
 */
139
get_start_rule_as_expression :: !DeserializationSettings !String !String !*World -> *(Maybe a, !*World)
140

141 142
graph_to_string :: !*SerializedGraph -> *(!.String, !*SerializedGraph)
graph_from_string :: !String -> Maybe *SerializedGraph
Camil Staps's avatar
Camil Staps committed
143

144 145
graph_to_file :: !*SerializedGraph !*File -> *(!*SerializedGraph, !*File)
graph_from_file :: !*File -> *(!Maybe *SerializedGraph, !*File)