-
Notifications
You must be signed in to change notification settings - Fork 2
Serialization
The serialization will be into LLVM meta data. This structure can only be flat (LLVM restriction). These meta data will be bounded with every instruction (see http://llvm.org/docs/LangRef.html#metadata). The meta data will represent domain returned as the result of instruction. The constants created inside of the instruction need not to be saved, since they can always be computed given the parameters available (and the result will always be the same).
Saved meta data will have the following format:
!"Class:Arguments:Version", data1, data2...
with number of data arguments will be the same as given in descriptor. This overcomes the problem with flat structure (you can save class's data inside of other class's data and the descriptor will tell you how many arguments should be given to class to deserialize from).
For memory, if the instruction creates new object on stack or heap, this information has to be dumped as well. (Memory object is stored as place -> data, so only data will be saved). This object is given a unique number. If pointer pointing to this memory object is serialized, the target will be this unique number.
Serialization and deserialization will work on the whole LLVM module. For every instruction from the state, serialized value of returned value will be created and saved into LLVM module. If new memory object is created in this instruction (e.g. alloca instruction), this object is dumped along with returned value. This modified module along with meta data will then be saved into separate file.
During deserialization, new state will be created from the LLVM module. For every variable in this state, the value is loaded from the meta data saved in the module. For pointers, target location must be created before the pointer itself is created; therefore, topological ordering or two phase creation (firstly locations only, secondly pointers) needs to be used.
TODO: Global constants and variables.
Comparison will work on two states and will compare variables between them. Since the states may have different structure (given different .s files), it is necessary to provide pairing function, which will say which variables from state A will be compared with which variables from state B. Also, it has to provide location translator, which can compare locations in between states (where every state has different LLVM module loaded, so pointers to those objects will be different). This can be achieved via absolute representation of location in program, like:
[ function name, basic block id, instruction id, [opcode id...] ]
Every domain will provide four new methods - canDeserialize, deserialize, serialize, compareWith. There is no need to dump type info into meta data - it is already provided from the LLVM bytecode.
This method reads the meta data and returns TRUE if it can deserialize them. Note that type must be the same (e.g. bit width).
This method modifies object to represent data loaded from meta data nodes.
This method creates new meta data nodes that represent serialized version of itself.
This method provides inclusion testing for domains from other state. For domains which represent values, this may be the same as inclusion test, but it can be relaxed (e.g. structure of domains in ReduceProduct may not be the same). For memory representing domains, this has to take into account different locations of objects from LLVM module; for that, LocationTranslator is provided, which translates locations from the LLVM module between states, so that they can be compared as values.