• For my implementation of eq.ml, it passes eq3.scm, but the output is of different order than scm.expected.

satisfiable
 (define-fun tgt_x () Int
   2)
-(define-fun src_x () Int
-  2)
 (define-fun src_y () Int
   1)
+(define-fun src_x () Int
+  2)

• Is this still a valid result?
• In general, will our solution only be graded getting the satisfiability correct, or will we also be checked on the produced model?

I'm working on the HW1 and stuck for a long time. I understanded eval function as evaluating the value of instruction and return it as Value.t type.
But I don't have any idea to go forward it. For ConstantInt type, I cannot find the proper function in LLVM OCaml binding document. The function type should be llvalue -> int or similar one I think.
For the Instruction type, I still don't understand how the instruction in eval and instruction in other functions are different, so the former should be interpreted as value and later should be interpreted as State-memory pair.
Can anyone give me hint for at least part of my question?

Hi all,
Homework 0-3 is graded.

We made a dummy homework named "Homework 0-3" at KLMS Week4 and uploaded your score there.
This score will be applied as a multiplication ratio to the final one.
For example, if your final score is 90, and the score of this is 3, you would get 92.7.

Thanks.

The instructions say that "Write in Korean if you are a native Korean speaker, in English otherwise."

Does that mean that I am forced to write Korean if I can, even if I prefer to write it in English?

I just wanted to double check because I haven't seen a course where writing in Korean was forced.

Thank you!

Hi,
Homework 2 is graded.

We made a dummy homework named "Homework 2" at KLMS Week7 and uploaded your score.
Note that this score reflects our late-submission policy.

We also pushed the hidden test cases used for grading to your homework repository.
You can test your code by pulling and running make test.

Have any questions, feel free to ask TA.

Thanks,
Sujin.

I have one question about today's lecture, regarding the definition of a "good state" in the sorting algorithm example.

In lecture03 slide 15, a property "Should return a sorted array (if terminated)" is a safety property.
Then, I wonder how we can define a "good state" and a "bad state" regarding this property.

If we define a "good property" as, "an array is sorted", the algorithm starts with a "bad state", where an input array is not sorted yet.
But we have learned that for safety property, a trace is initially in a good state and we try to prove that it never falls into a "bad state" in finite time.

Then, should we define a "good state" as, "ON RETURN, the array is sorted" in this situation?
And all states that are not return statements should be regarded as "good states"?

Thank you in advance :)

In the Sudoku Solver, I implemented all the codes that I need.
But when I run the test case ./sudoku test/sudoku1.scm, I have the result like below:

satisfiable Fatal error: exception Z3.Error("Conversion failed.")
But when I inserted the line Z3.Solver.to_string solver |> print_endline; in the solver function, I have the result

... (not (= x63 x85)) (not (= x63 8)) (not (= x63 x83)) (not (= x63 9)) (not (= x63 1)) (not (= x63 4)) (not (= x63 x65)) (not (= x63 x64)) (not (= 7 9)) (not (= x86 9)) (not (= x86 7)) (not (= 5 9)) (not (= 5 7)) (not (= 5 x86)) (not (= x77 9)) (not (= x77 7)) (not (= x77 x86)) (not (= x77 5)) (not (= x76 9)) (not (= x76 7)) (not (= x76 x86)) (not (= x76 5)) (not (= x76 x77)) (not (= x68 9)) (not (= x68 7)) (not (= x68 x86)) (not (= x68 5)) (not (= x68 x77)) (not (= x68 x76)) (not (= 8 9)) (not (= 8 7)) (not (= 8 x86)) (not (= 8 5)) (not (= 8 x77)) (not (= 8 x76)) (not (= 8 x68)) (not (= 2 9)) (not (= 2 7)) (not (= 2 x86)) (not (= 2 5)) (not (= 2 x77)) (not (= 2 x76)) (not (= 2 x68)) (not (= 2 8)))) (model-add x71 () Int 8) (model-add x11 () Int 7) (model-add x85 () Int 6) (model-add x23 () Int 3) (model-add x55 () Int 4) (model-add x76 () Int 6) (model-add x63 () Int 5) (model-add x16 () Int 3) (model-add x26 () Int 5) (model-add x53 () Int 9) (model-add x41 () Int 2) (model-add x56 () Int 8) (model-add x62 () Int 1) (model-add x65 () Int 7) (model-add x33 () Int 7) (model-add x35 () Int 1) (model-add x57 () Int 5) (model-add x46 () Int 7) (model-add x24 () Int 4) (model-add x31 () Int 5) (model-add x86 () Int 1) (model-add x72 () Int 7) (model-add x03 () Int 6) (model-add x51 () Int 1) (model-add x83 () Int 2) (model-add x18 () Int 8) (model-add x52 () Int 3) (model-add x20 () Int 1) (model-add x25 () Int 2) (model-add x37 () Int 2) (model-add x32 () Int 9) (model-add x44 () Int 5) (model-add x05 () Int 8) (model-add x77 () Int 3) (model-add x81 () Int 4) (model-add x82 () Int 5) (model-add x42 () Int 6) (model-add x64 () Int 3) (model-add x70 () Int 2) (model-add x36 () Int 4) (model-add x02 () Int 4) (model-add x12 () Int 2) (model-add x47 () Int 9) (model-add x60 () Int 9) (model-add x17 () Int 4) (model-add x68 () Int 4) (model-add x28 () Int 7) (model-add x80 () Int 3) (model-add x08 () Int 2) (model-add x06 () Int 9) (model-add x07 () Int 1) ...

Which coincides with the solution of the Sudoku.
If the Sudoku is unsatisfiable, the result has no problem since it does not have to print any Sudoku board. I cannot find out why this kind of problem occurs. Is it a problem from my code? I think my code gives a proper FOL formula to represent the Sudoku, and I think solver is finding the right solution - but it has a trouble in just printing the solution.

Thank you.

Hi all, this is an announcement about homework 1.

Homework 1 is a programming assignment requiring you to implement the SmaLLVM interpreter.

Here is the GitHub classroom link for this homework:
https://classroom.github.com/a/_uCtpq_X

Due is 9.18(Sun) 23:59:59, and late submission is available until 9.20(Tue) 23:59:59.

Thanks.

Hi.
Here is another gift for you. This homework is optional. (similar to HW 0-3)

Read the three articles about the future of programming on the course webpage:

• Wired
• IEEE Spectrum
• CACM

and think about the followings:

• What is the future of programming?
• What are the limitations of current AI-based programming?
• How can we overcome the above challenges?

Provide your opinion and write an essay. The same (syntactic and semantic) evaluation criteria will be applied as before.

Due: Nov 11 23:59:59 (no late submission allowed)

TAs, please add the invitation link below.

Hello, now I'm trying to understand 'incompleteness' concept and apply this to programming languages.

From my understanding, if a simple language containing basic arithmetic operations is given, there should be a statement that is true but cannot be proven by Gödel's incompleteness theorems.
Then, this statement $S$ must not be written by both of big-step and small-step operational semantics.

Am I right? Is there really such a case in reality?

Hello, I found some possible typos in lecture0 slides.

1. higher-order function
   In slide 18, there's an example about higher-order functions.
   

It says its final result will be 17, but I think it should be 18 since ((10 + 1) + 5) + 2 is 18. So I thought it was a typo, but I cannot sure because I'm totally new to OCaml.. Am I right? Or, was there any mistake in my logic?

2. "function" keyword
   In slide 21, a recursive function("fact") is simplified using "function" keyword.
   

But it doesn't work and shows an error message "Error: Unbound value n".
So I think there should be "n" right after the function name, like

# let rec fact n = function
| 0 -> 1
| _ -> n * fact(n-1)

and this works fine, at least for me. Is this right?

Well I'm sorry for somewhat trivial questions, but I want to be sure about OCaml :)
Thank you for reading!

Hi all, this is an announcement about homework 2.

Homework 2 is a programming assignment requiring you to implement logical reasoning tools using the Z3 SMT solver.

Here is the GitHub classroom link for this homework:
https://classroom.github.com/a/iojoMyS0

Due is 10.7(Fri) 23:59:59, and late submission is available until 10.9(Sun) 23:59:59.

Thanks.

In class, while proving the validity of
$F: a[i] = e \rightarrow \forall j. a \langle i \triangleleft e \rangle [j] = a[j]$,
we reached
$(1) \ I \vDash a[i] = e$, $(2) \ I' \nvDash a \langle i \triangleleft e \rangle [j] = a[j]$ and $(3) \ I' \vDash i = j$ where $I' = I \triangleleft \{ j \mapsto v \}$.
This is enough if we can say
$(1)$ implies $(4) \ I' \vDash a[i] = e$,
since $(3)$ and $(4)$ implies $(5) \ I' \vDash a \langle i \triangleleft e \rangle [j] = a[j]$ which is contradictory to $(2)$.

The only problem is that I couldn't find a rule that implies $(4)$ from $(1)$.
Here are the alternative answers I found:
a) Add a new rule.
$I \vDash F$ implies $I' \vDash F$ where $I'$ is a $x$-variant of $I$ and $x$ is free in $F$.

b) Move $\forall j.$ to the outmost. That is, replace $F$ by
$F': \forall j.(a[i] = e \rightarrow a \langle i \triangleleft e \rangle [j] = a[j])$.
Then we are happy since we will get $(4)$ instead of $(1)$ from the beginning of the proof.

c) There is a rule but I just couldn't find.

So what would be the correct way?

In the first line of hw0-2 readme.md, 'running your code' section, isn't it OCaml REPL, not REFL?

Hi, I have a question about homework 1.

Why there is no definition of input function in domain.ml?

In the module VALUE, there is definition of function "print" (val print : t -> unit).
But I can't find the definition of function "input".

Can I just use input_line in the semantics.ml(in the Llvm.Opcode.Call when Llvmutils.is_input instr)?

I found that given match cases in eval function cannot support undef value of LLVM IR.
(I have no idea why compiler creates such code even j is properly initialized at the point it should be)
Is this kind of IR considered as syntactically invalid? Should I add support for undef value, such as initializing with zero?

By README, it seems HW3, LLVM verifer is planned to be out before midterm exam.

Can you announce when is out and due for planning after midterm?

Thank you.

In the LLVM docs, i1 is a single-bit integer.
Since Bool type of interpreter is matched with i1 type, should we allow arithmetic & comparison operations for boolean operands?

Hi,

Let me clarify one thing regarding the question from Sanga (상아) during the lecture today.
The proof of the safety property of an algorithm can be done as follows.

For simplicity, let us consider a search algorithm rather than a sorting algorithm. Consider a linear search algorithm: given an array a, lower bound index l, upper bound index u, and target e, the following function checks whether there exists e in the array within the boundaries:

bool LinearSearch(int []a, int l, int u, int e) {
  int i = l;
  while (i <= u) {
    if (a[i] == e) return true;
    i = i + 1;
  }
  return false;
}

To show the safety property "the algorithm returns true if there exists e", it is enough to show the following is a loop invariant:

l <= i /\ (forall  j. l <= j < i  -> a[j] != e)

This is the "good" state we want our program remains in during the execution of the loop.
Why? If it is proven to be a loop invariant, it is fairly easy to prove the correctness afterward. I recommend you prove it by yourself as an exercise.

We will revisit this example in a few weeks.

I'm new to this github-classroom, so I'm not sure whether I submitted successfully.

Is it successfully submitted if I can see the green check marker in the action tap of my homework repository? And is it intentional that I cannot check any score? (or is it bug?)

Thank you!

For now, execute_instr seems to return only mutated memory.
But to implement semantics, I think it should return next label(i.e. instruction) as well.
Can I change the signature of function? Or am I missing something?

What is difference between (Z3.Arithmetic.Integer.mk_numeral_i v) and (Z3.Arithmetic.Integer.mk_constant z3ctx ((Z3.Symbol.mk_int z3ctx v)))?

I think each produces different result while executing sudoku.ml..

If they are different, what function should I use?

And I always have this error when I execute sudoku

satisfiable 
Fatal error: exception Z3.Error("Conversion failed.")

Is it related to this problem?

Thank you

Hi, I have one question regarding the grading method of eq in our homework assignment.

When two programs, src and tgt are not functionally equivalent, our program should print satisfiable, with a counterexample. (Counterexample that makes the two programs return different output for the same input)

I wonder if the homework grader will take into account that there may be multiple counterexamples for satisfiable case.

To illustrate, for test/eq3.scm,

; f(x) = let y = 1 in if (x = y) then 1 else y
(let y 1 (if (= x y) 1 1))
; f(x) = x
x

the expected output in the given repository is,

satisfiable
(define-fun tgt_x () Int
  2)
(define-fun src_x () Int
  2)
(define-fun src_y () Int
  1)

But my program gives,

satisfiable
(define-fun src_y () Int
  1)
(define-fun tgt_x () Int
  0)
(define-fun src_x () Int
  0)

So the CI workflow in my homework repository fails. However, I believe my output is also acceptable.
There can be many counterexamples, and I wonder if the grader of this assignment will take this into consideration.

Thank you in advance :)

Hello.

I have been implementing the solvers for Hw2.
I believe I have correctly implemented the program equivalence checker, in that I think it prints "satisfiable" along with a model when the programs are not equivalent, and "unsatisfiable" when they are equivalent.

However, for some reason, when printing a model in which the programs give different results, my implementation prints the variables in a different order than was provided on Github.

Below is a picture of my testing with the eq3.scm file.
Instead of printing in tgt_x -> src_x -> src_y order,
it does in tgt_x -> src_y -> src_x order.
Moreover, when testing with make test, this is registered as a wrong output.

My question is, does the order of printing a satisfying model matter?
Should I modify my code so that it correctly prints in the designated order?

Thank you.

I have several questions on implementing program equivalence checker part.

• Can a function return the value from Eq operation? For instance, is this function definition ok? f(x) = (x = x) If so, then should we treat result of Eq operation as having a boolean type (which is different from integer type)?
• From the definition of exp, we know type exp ::= ... | If exp * exp * exp | .... In this case, can we assume first argument of If case should be Eq? Otherwise, if the first argument evaluates to an integer value in runtime, then how do we decide which branch to take?
• Is it guaranteed that every variable and function parameter x have integer type?
• Can we assume that every given program never incurs any error in runtime (such as use of free variables)?
• I read the template code, and found that if Z3 solver says given formula is satisfiable, then our program prints the model. In this situation, it seems it also prints out the name of the variables that we used when constructing the formula. So, should we follow the naming convention provided in the problem description? (e.g., src_x, src_y, tgt_x)

Many of my questions are related to type system of the language, and it would be helpful if you clarify on these questions. Thank you in advance.

To implement the transfer of case print, I want to know the argument of function call instruction instr which calls print. But I couldn't find a way to reach it. How can I?

This semester, students will use OCaml and several tools for programming assignments.

To help you set up the programming environment, we provide a pre-built docker image and KCLOUD VMs.

For detailed information, please see the instructions.

According to homework.pdf, semantics of expression are defined as above.
Can I assume that E1 and E2 are limited to pure values (n / true / false) or labels?
As far as I understand, LLVM never generates nested instructions.

p.s. I am asking this question in case of nested instruction exists and LLVM considers it as 'integer' or 'boolean' as label do)

Hello.
I'm just confusing when the online lecture will turn into the offline classes.
Especially, I'm wondering whether there will be an offline class tomorrow.. because the incoming typhoon is forecasted to affect Daejeon from today late-night to tomorrow morning accroding to KMA.

Thank you for replying in advance!

Hi.
In the page 48, there is a comment (about fold_left).

(* val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list *)

But I think it should be like this.

(* val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a *)

Thank you

Hi all,
this is an announcement about homework 3.

Homework 3 is a programming assignment requiring you to implement a program verifier that automatically checks non-trivial semantic properties of SmaLLVM programs.

Here is the GitHub classroom link for this homework:
https://classroom.github.com/a/9y0vacVC

Due is 10.27(Thu.) 23:59:59, and late submission is available until 10.29(Sat.) 23:59:59.

Thanks.

Hi everyone.

Welcome to CS492. I am looking forward to meeting you in class.
Here are some things you should set up for this course. The details will be introduced in the first lecture.

• Submit your account via the google form. (TAs will give the link below.)
• Join the Gradescope. The Entry code is V58RX4

Hope you enjoy the class!

I understand from the LLVM Primer slides that most things in LLVM IR are represented as llvalue instances.
I also found in the OCaml Llvm module API that the functions num_operands and operand can be used to access the operands of the instruction if the input llvalue instance is in fact an instruction.

However, I seem to be having little luck in finding how the operands are placed and interpreted.
For example, suppose that Llvm.instr_opcode instr returned Llvm.Opcode.Add.
How many operands should this instruction normally have?
If this was interpreted as the addition arithmetic expression, then I would guess 2.
But if this addition instruction also implied an assignment command implicitly, then I think 3 operands (2 sources, 1 destination) should be provided.

Is there documentation that explains such internal structures of instructions?

Thank you.

Announcement

Hi all, this is an announcement of homework 0.

This homework includes two programming exercises and one writing.

Here are the GitHub classroom links for each assignment:

• Homework 0-1: https://classroom.github.com/a/Fiyo7xH9
• Homework 0-2: https://classroom.github.com/a/I26NZsHx
• Homework 0-3: https://classroom.github.com/a/-s2pJdij

Description

Homework 0-1 & 0-2

Homework 0-1 and 0-2 are programming exercises for those unfamiliar with OCaml and Git.

Feel free to skip these assignments if you are already used to both.

We won't grade them, so there are no deadlines.

Homework 0-3

Homework 0-3 is a writing assignment.

Watch the video(KR, EN) explaining undecidability, and write a critique about it.

You should submit it at Gradescope in PDF format.

Due is 9.16(Fri), and late submission is available until 9.18(Sun).

If you have any questions, feel free to ask TA.

Thanks.

In satTest.ml file, sample answer for solve (And (Or (Z, Not Y), Or (Not X, Not Z))) is SAT (false, false, false).
However, SAT (true, false, false) also makes sense.
Is there specific reason that the answer should be (false, false, false)?

Hi all,
We regrade the score of homework1 due to the ambiguity about the boolean comparison.

Initially, we expected you to implement the Eq and Ne operations between boolean values.
However, we also decided to accept the "Invalid Argument exceptions" as a correct answer since we guessed it would have been confusing to make such a decision.

We have updated the new scores in KLMS.
So please recheck your score.

Thanks,
Seungwan.

In transfer function in semantics.ml, when dealing with print operation, do we need to automatically print newline character after printing value on the screen? Or do we just need to print only the value?
(I checked if we don't print newline character then make test fails, but I wonder if it is the case even for hidden test cases.)

• In class on 9/29/2022, we learned about the theory of arrays and the key axioms.
• One thing I noticed but forgot to mention is that there does not seem to be any check that indexes are inbounds. Does this mean that the theory is for unbounded arrays?
• In the case that we add a restriction for bounded arrays, would we need to be careful to not assert anything about out-of-bounds access, or will it be OK to say it is None?
• Another impression I got was that we implicitly assumed array was "initialized". Would a theory where a read on a index was only possible after a write was done make sense?

Is it possible to use the techniques we have used to prove the correctness of recursive functions?
For example, the following function is recursive:

@pre: n >= 0
@post: isNthFibonacciNumber(ret, n)
let rec fibo = function
    | 0 -> 0
    | 1 -> 1
    | n -> (fibo (n - 1)) + (fibo (n - 2))

To prove the correctness of this function, my instinct is to use induction on n, which might work for this particular case since it is a simple function with only one integer input.

However, for more complex functions like merge sort:

@pre: 0 <= l, r < length(a)
@post: forall i, j. l <= i <= j < r -> a[i] <= a[j]
let rec mergeSort a l r =
    if l >= r then return;
    let mid = (l + r) / 2 in
    (Something something)
    let _ = mergeSort a l mid in
    let _ = mergeSort a mid r in
    (Something something)

such simple mathematical induction seems inapplicable.
It feels like we need to know how mergeSort functions in order to reason about its function, let alone its correctness.
I attempted to say that if mergeSort correctly sorts the left half and it correctly sorts the right half, then it satisfies the postcondition.
However, this argument begs the question, i.e., it assumes the postcondition that I am trying to prove, making it vacuous.

In short, how do we prove the partial correctness of recursive functions?

Thanks.

(Forgive me for the trivial questions... I am new to LLVM...)

I originally thought that Variable.t should represent the name of the variable, collected from the instruction object with the Llvm.value_name function.
For example, when the object instr encodes the instruction
%x = add nsw i32 10 20
then the result of the add instruction is saved in the %x variable.
I had thought that the %x should be used for the Value.t somehow, and that %x should be parsed from Llvm.value_name instr command.
However, it seems that Variable.t takes the data type of Llvm.llvalue.
Then, how should I interpret what Variable.t means? How is it encoded in the instruction?

Thank you.

Is there a way to create a distinct Z3.Arithmetic.Integer term similar to Z3.Boolean.mk_distinct.

I tried using Z3.Boolean.mk_distinct, but unfortunately they are incompatible.

I'm using a provided docker image to do homework.
According to the Makefile in the 'test' directory, opt-10 is used to apply mem2reg optimization. However,opt-10 is not installed in the pre-built docker image.
Is it okay to edit the Makefile to use opt-13 instead? HW1 also used opt-13 instead of opt-10.

make: opt-10: Command not found
make: *** [Makefile:12: example5.ll] Error 127

Hi,

We would like to organize some confusing things about the output of Z3 model. (please refer to #47)

The result of your Z3 model and the result of *.expected file do not have to match perfectly.

• Okay: The order of the variables that the Z3 model outputs is different from the expected file.

e.g.

satisfiable
 (define-fun tgt_x () Int
   2)
-(define-fun src_x () Int
-  2)
 (define-fun src_y () Int
   1)
+(define-fun src_x () Int
+  2)

• Okay: The value of the variable is reasonable, but different from the expected file.

e.g.

// result of expected file

satisfiable
(define-fun tgt_x () Int
  2)
(define-fun src_x () Int
  2)
(define-fun src_y () Int
  1)

// assume your result

satisfiable
(define-fun src_y () Int
  1)
(define-fun tgt_x () Int
  0)
(define-fun src_x () Int
  0)

If you want to check whether actually passed through test case, you need to modify some things.

1. please modify your src/test/dune according to the following format. (except for sudoku)

// original

(rule
 (deps pl1.scm)
 (targets pl1.output)
 (action
  (with-stdout-to
   %{targets}
   (run ../pl %{deps}))))

(rule
 (alias runtest)
 (action
  (diff pl1.expected pl1.output)))

// modified

(rule
 (deps pl1.scm)
 (targets pl1.output)
 (action
  (with-stdout-to
   %{targets}
   (pipe-stdout
   (run ../pl %{deps})
   (run head -n 1)))))

(rule
 (alias runtest)
 (action
  (diff pl1.expected pl1.output)))

2. Please modify your dune-project.

// original
(lang dune 2.3)

// modified
(lang dune 2.7)

3. Please leave only the first line of all expected file. (except for sudoku)

// original

satisfiable
(define-fun x () Int
  2)
(define-fun src_y () Int
  1)

// modified

satisfiable

Sorry for the confusion.

Hi all,
Homework 1 is graded.

We made a dummy homework named "Homework 1" at KLMS Week4 and uploaded your score.
Note that this score reflects our late-submission policy.

We also pushed the hidden test cases used for grading to your homework repository.
You can test your code by pulling and running make test.

Have any questions, feel free to ask TA.

Thanks,
Seungwan.

• Can functions return boolean, or do we consider only those that return integers?
• Can it be the case that in the two branches of If, one is integer, and other is bool?

Hi, I have a question on the wlp of while command.

In the page 29 of lecture 7, it says that the wlp of while command is as follows:

wlp(while E do S, Q) = I /\ (E /\ I -> wlp(S, I)) /\ (!E /\ I -> Q)

with assumption that an inductive invariant I is provided.

And I got confused when I applied this to the example in page 31.

while i > 1 {
  i := i - 2;
}
assert(i = 1);

For the above program, I used inductive invariant as i >= 0 instead of i >= 0 /\ odd(i).
(I think it is also inductive invariant because wlp(i := i - 2, i >= 0) = (i >= 2) and i > 1 => i >= 2 is true.)

So in the above notation, E is i > 1, S is i := i - 2, Q is i = 1 and I is i >= 0.

  I
= i >= 0

  E /\ I -> wlp(S, I)
= (i > 1) /\ (i >= 0) -> wlp(i := i - 2, i >= 0)
= (i > 1) /\ (i >= 0) -> (i - 2 >= 0)
= i > 1 -> i >= 2
= true

  !E /\ I -> Q
= !(i > 1) /\ (i >= 0) -> i = 1
= 0 <= i <= 1 -> i = 1
= !(0 <= i <= 1) \/ (i = 1)
= (i < 0 \/ i > 1) \/ (i = 1)
= i < 0 \/ i >= 1

  wlp(while E do S, Q)
= I /\ (E /\ I -> wlp(S, I)) /\ (!E /\ I -> Q)
= i >= 0 /\ true /\ (i < 0 \/ i >= 1)
= i >= 1

Therefore, wlp(while i > 1 do i := i - 2, i = 1) is i >= 1 and so { i = 4 } while i > 1 do i := i - 2 { i = 1 } is true because i = 4 => i >= 1 is true. However, I think this is not true because the assertion fails when the initial value of i is 4. Is there anything I'm thinking wrong?

+) I searched for other references and found that there is a definition as follows (Reference)

wlp(while E do S, Q) = I /\ (forall x1,...,xk (((E /\ I) -> wlp(S, I)) /\ ((!E /\ I) -> Q))[xi/wi])

where w1,...,wk is the set of assigned variables in statement S and x1,...,xk are fresh logic variables.

1. Is it an undefined behavior to put boolean operands for arithmetic/comparison operators? The doc(homework.pdf) says

The semantics of ⊕ and < follows the standard definition of arithmetic and comparison operators of LLVM

but I cannot find the specification of implicit conversion nor explicit error from LLVM Language Reference.

From what I understood, LLVM IR is motivated from assembly, so it sounds plausible if we support implicit conversion such as
add %rax, %rax, %ebx

2. Why do unsigned comparison operators(e.g. Ugt, Uge, Ult, Ule) exist in Llvm.Icmp although doc(homework.pdf) says

However, the interpreter will not take into account the sign of operators.

3. Are there extra test cases for grading?

Hello. This is a duplicated question. Copyright: #51.

I have been implementing the solvers for Hw2.
I believe I have correctly implemented the program equivalence checker, in that I think it prints "satisfiable" along with a model when the programs are not equivalent, and "unsatisfiable" when they are equivalent.

[Small change]

However, for some reason, when printing a model in which the programs give different results, my implementation prints the variables in a different order than was provided on Github.

[Small change]

Below is a picture of my testing with the eq3.scm file.
Instead of printing in tgt_x -> src_x -> src_y order,
it does in tgt_x -> src_y -> src_x order.

My question is, does the order of printing a satisfying model matter?

Thank you.

===
Sorry for unnecessary notification emails.

Hi.

I tried to connect the KCLOUD VM via ssh (the host "CS492H-20" in the sheet), but the server did not respond. The ssh command ends with the following error message. (erased out the IP address due to security reasons)

ssh: connect to host ***.***.***.*** port 22: Operation timed out

I tried to connect with and without the KVPN, but both tries failed in the same way. (btw, I'm using the KAIST internal network)

I guess there is a certain way to connect to the KCLOUD?

I hope students can successfully use the VM in short time.

According to answer of #26, my submission throws Invalid Argument error for suite:17:cmp_ne_bool and suite:14:cmp_eq_bool, failing some of test cases.

I thought the interpretation of "integer" referenced in comparison should be applied on ALL comparison operators, include equal and not equal.

Is there any chance for claim?

Could you provide an example of valid C code to generate such comparison of boolean operands in LLVM given test condition?

This is what I thought:
README limits test cases of all values to be i32 or i1, but as far as I know there is no way to define i1 in C.
So i1 value can be only generated from comparison.
Therefore there can be no comparison of boolean operands.