-
Notifications
You must be signed in to change notification settings - Fork 19
Closed
Description
Hi everyone,
If you have not generated your repository yet, then you can ignore this since I have updated the template.
However, If you have already generated your own Homework 5 repository, please check the followings.
We extend the due dates by 2 days because of this update.
Updated Due: 11. 9 (Thu.) 23:59:59 ---> 11. 11 (Sat.) 23:59:59
Updated Late Due: 11. 11 (Sat.) 23:59:59 ---> 11. 13 (Mon.) 23:59:59 (late submission penalty).
Sorry for the inconvenience.
Patches
There were missing instructions in the template. You should consider two additional instructions to complete the analyzer.
--- a/src/semantics.ml
+++ b/src/semantics.ml
@@ -58,6 +58,8 @@ module Make (Memory : D.INSTRUMENTED_MEMORY_DOMAIN) : S = struct
(callgraph, [ (next, memory) ])
| Llvm.Opcode.Alloca -> failwith "Not implemented"
| Llvm.Opcode.Ret -> failwith "Not implemented"
+ | Llvm.Opcode.ZExt -> failwith "Not implemented"
+ | Llvm.Opcode.BitCast -> failwith "Not implemented"
| Llvm.Opcode.PHI -> failwith "Not implemented"
| Llvm.Opcode.Add -> failwith "Not implemented"
| Llvm.Opcode.Sub -> failwith "Not implemented"Their semantics are not stated in the homework document. You can consider them as identity functions.
--- a/README.md
+++ b/README.md
@@ -129,6 +129,9 @@ and the abstract transition relations defined in the [document](doc/homework.pdf
some utility functions like `Llvmutils.entry_point` and `Llvmutils.get_function` in [Llvmutils](https://prosyslab-classroom.github.io/llvmutils/llvmutils/Llvmutils/index.html) to get the first instruction
of a function and the function where an instruction belongs.
+There are two instructions not apeared in the [document](doc/homework.pdf): `ZExt` and `Bitcast`.
+You can consider them as identity functions.
+
Students should design a proper memory update strategy. A naive implementation will always apply weak update
because the analysis is context-insensitive (i.e., potentially have multiple instances of local variables and
stack memory cells). However, a precise update strategy is possible even with the context-insensitive abstraction,Metadata
Metadata
Assignees
Labels
No labels