Floating Point Support for Obliv-C #30
Conversation
…ange genData license
…blivc tests folder
@samee I've gone over the changes you've made and I believe that I've resolved the issues that were brought up either by you or by Jack on this thread. I've cherry-picked the latests commits from your float-support branch in order to absorb your changes into my PR, and on top of those I've made a few commits that fix the other issues. Please let me know how you want this rebased / modified before it can be merged into the main repo as I've tried rebasing it but it doesn't seem to come out cleanly. I'll be trying rebasing again after you get a chance to review these latest changes. Responses to the points you brought up:
You're right, that class is no longer necessary so I have removed it.
I believe that you're correct about the required change. I have changed the guard
That function is for my
I'm not sure why it's necessary but the reason that I have it is because all of the comparisons (the ones that were there before I started adding floating point support) have it. For example
I tried out that replacement and it doesn't seem to work. I actually tried out a few things before resorting to using the "union trick" but all of them did not work. What are you thoughts on this?
I'm not sure -- are we trying to support that kind of behavior? I can add in support for that but I hadn't because I didn't realize that we would want those kinds of conversions.
You're right, that has now been removed.
Things would have broken because of relative paths in the Makefile but I've fixed that and moved both
I've now included that file from a single place. Other Changessrc/ext/processObliv/processObliv.mlWhile I was testing out these changes at first compilation was not terminating on my test cases. I determined the cause to be the removal of
which was done during the changes in your rebase. Adding back that case allows compilation to terminate and the test cases to run successfully. What was the reason for the removal? src/ext/oblivc/obliv_bits.cMoved
As I mentioned earlier, I believe that this was the cause of issues when using the changes in this PR with other code. After this change, running:
no longer causes a segfault. Misc.The |
I can't really tell which commits you want me to cherry pick on top of E.g.:
Now you should have two branches, Let me know if this works. |
@samee I apologize for not being clear about that; what I meant is that I have already cherry-picked the last three commits from your float-support branch and integrated them with my branch. I was thinking we could do a merge-rebase of my branch into your repo. Would that work for you? (The reason that my commits won't play back properly on your branch is that my fp-support branch does not have a lot of the commits you included in float-support. I tried to be minimal with what I was including as part of the PR and thus did not include all of those commits. There should not be a difference/problem when it comes to merging though). |
Merging creates conflicts as well. The conflicts might be simple to solve, though. In any case, if I understand your intentions, you want me to include the following commits from your fp-support branch:
Is this what I should review now? |
@samee Actually, of those commits only the top three are needed. The bottom three were just to make my branch functionally equivalent to yours. So these three can be reviewed:
I should note that there were a few changes in this commit:
but as is shown in the commit message, these are fairly straightforward changes based on pervious discussion. You might want to approve the error messages I've added though. |
Again, Darion, please clean up diffs for commit before mailing them out, either here, or on some other open source project, or even in a company. In particular:
While every project is a little different, here is a reasonable guide to get you started: For example, I have split up your commit These things affect future maintainability of a project, specially when most of the code is no longer being contributed by a single developer. When cherry-picking $ git diff bc13208cf{^,} src/ext/processObliv/processObliv.ml
[...]
@@ -501,7 +498,6 @@ let setComparisonUS fnames dest s1 s2 loc =
let optype = typeOfLval s1 in
let fname = match unrollType optype with
| TInt(k,_) -> if isSigned k then snd fnames else fst fnames
- | TFloat(k,_) -> fst fnames
| _ -> E.s (E.error "Cannot operate on obliv values of type %a" d_type optype)
in
setComparison fname dest s1 s2 loc
[...]
@@ -685,10 +681,10 @@ let rec codegenUncondInstr (instr:instr) : instr = match instr with
| Shiftlt-> E.s (E.error "Shift operation on float invalid!\n")
| Ne -> setComparison "__obliv_c__setNotEqualF" v e1 e2 loc
| Eq -> setComparison "__obliv_c__setEqualToF" v e1 e2 loc
- | Lt -> setComparisonUS cmpLtFuncsF v e1 e2 loc
- | Gt -> setComparisonUS cmpLtFuncsF v e2 e1 loc
- | Le -> setComparisonUS cmpLeFuncsF v e1 e2 loc
- | Ge -> setComparisonUS cmpLeFuncsF v e2 e1 loc
+ | Lt -> setComparison "__obliv_c__setLessThanF" v e1 e2 loc
+ | Gt -> setComparison "__obliv_c__setLessThanF" v e2 e1 loc
+ | Le -> setComparison "__obliv_c__setLessThanEqF" v e1 e2 loc
+ | Ge -> setComparison "__obliv_c__setLessThanEqF" v e2 e1 loc Float-related code shouldn't need to use that function at all. So I'm a little surprised that line caused problems, since I don't think it is being invoked when processing floats. Maybe there's something I missed, but I'd like to know the underlying cause of the problem. |
@samee Thanks for reviewing my changes. I apologize for the messiness; I did not realize that you wanted to add my changes back to your float-support branch (I was under the impression that we would merge my fp-support branch) and as such I was not looking at the diffs against your branch. For any future changes I will just start at the HEAD of your branch as you suggest so that changes are easier to integrate. Sorry about that. With regards to the issue with:
The reason that I came to think it was an issue was that my floating point test suite,
which of course is the fall-through branch of the match statement that the removed line belongs to. Now that I consider it again though, this could just mean that I have some malformed code in my testFloatOps.oc file, however at the moment I don't see the issue. Let me know what you think. |
No problem. Regarding those So for the rest of darioncassel@c7d8bed, it seems you added a case for casts to float, but this doesn't seem to be solving everything. E.g., I tried making the following changes on top of darioncassel@e138867: $ git diff
diff --git a/test/oblivc/testFloat/testFloatOps.oc b/test/oblivc/testFloat/testFloatOps.oc
index 9ec8a407..f09a0efd 100644
--- a/test/oblivc/testFloat/testFloatOps.oc
+++ b/test/oblivc/testFloat/testFloatOps.oc
@@ -37,6 +37,14 @@ void floatOps(void* args)
printf("Y_r: %f\n", y_r);
printf("\n");
+ // Casts
+ obliv int i = obliv_x;
+ int i_r;
+ revealOblivInt(&i_r, i, 0);
+ printf("Casting to int test: expecting 1\n");
+ printf("Casting to int: %d\n", i_r);
+ printf("\n");
+
// Addition
obliv_z = obliv_x + obliv_y;
revealOblivFloat(&z, obliv_z, 0);
$ make
../../..//bin/oblivcc -DREMOTE_HOST=localhost -O3 -I . testFloatOps.oc testFloatOps.c ../common/util.c
testFloatOps.oc: In function ‘floatOps’:
testFloatOps.oc:41:3: error: conversion to non-scalar type requested
obliv int i = obliv_x;
^ We want to follow normal C semantics as closely as possible to avoid surprises. In C, we can convert a Or alternatively, you can leave it open as a bug for now, but at least have a clearer error message that says the feature is unimplemented. |
Btw, I like the way you keep input variables separate in |
Ok, I agree with what you said. To make sure we're on the same page, going forward are these the things that will be done?
If you're in agreement, I will go ahead and add the improved error message and then open an issue for the truncation circuit. |
Yes, that sounds quite reasonable. Please make sure we cover all combinations of float/int, float/float/ int/float, int/int combinations, even if it just says "unimplemented". We don't want an undefined behavior.
No, please remove it. My understanding if your previous message is that we cannot explain the purpose of those lines, in which case I don't want it in the code. Let me know if you have more questions. |
@samee I've been investigating the The reason why it seemed necessary was actually because of a bug in the logic of the The fix for this that I've implemented in
is to add an additional check to the A consequence of this fix is that I discovered that the
Those fixes are found in the two commits previous to My intention was to apply this commits on top of your |
Wow, I do appreciate you being thorough, but you are probably working too hard here! I was going through your code in darioncassel@3ae1c41, and you have added lots of code that are unreachable and unnecessary :) Let me explain.
First of all, great catch! Even I didn't notice it, and I should have. But this conversion is rare. The way CIL works is that it simplifies any C code into a sort of assembly-language-like version of simplified C, before Obliv-C even touches it. Here's a useful experiment you can do. Let us, for instance, try an input mixing ints with floats: float z = 5.0f + 10; You can see what CIL does to it using this command (put the line above in a function):
CIL's simplify plugin will translate it into this (along with other preprocessing cruft we don't care about): float z ;
float __cil_tmp2 ;
__cil_tmp2 = (float )10;
z = 5.0f + __cil_tmp2; And this is normal C code, with no hint of So I don't think line 671 of darioncassel@3ae1c41 will ever be executed. I tried a few tests with your | TInt(kind,a) when hasOblivAttr a ->
begin match unrollType (typeOf (Lval e1)) with
| TFloat(kind,a) when hasOblivAttr a ->
begin match unrollType (typeOf (Lval e2)) with
| TFloat(kind,a) when hasOblivAttr a -> into | TInt(IBool, a) when hasOblivAttr a &&
isOblivFloat (typeOf (Lval e1)) &&
isOblivFloat (typeOf (Lval e2)) ->
(* handle comparisons between floats *)
| TInt(kind,a) when hasOblivAttr a ->
(* leave obliv int binary operations unchanged *) Similarly, bitwise operations on floats: CIL already complains about it long before it gets to your code. You don't need those cases. The situation is similar for unary operators: you have a new Let me know if these make sense, or if I missed some case. You can play around with |
Thanks for going through that Samee! I agree with your analysis of the situation; those cases I added do seem unnecessary given the transformations you showed that CIL performs. I think that the simplification you have listed: | TInt(IBool, a) when hasOblivAttr a &&
isOblivFloat (typeOf (Lval e1)) &&
isOblivFloat (typeOf (Lval e2)) ->
(* handle comparisons between floats *)
| TInt(kind,a) when hasOblivAttr a ->
(* leave obliv int binary operations unchanged *) is valid. Please let me know if there is anything else you need me to do. |
processObliv.ml had many cases that would never have executed, specially regarding mixing float and ints in binary operator expressions. See the attached bug for details, but the summary is that many of these cases are taken care of by earlier stages in CIL. Details in comment: #30 (comment)
I found a bug in samee's float-support branch. See line obliv_bits.c, line 2069. This belongs in |
Sounds fair. See if this fixes it. |
Can confirm that it now works! |
Merge pushed. Obliv-C now has 'obliv float'. Thanks both of you for all the effort, specially Darion for implementing the whole thing! Closing out. |
Excellent! Thanks to all of you for your hard work on this. I much appreciate Samee's efforts to preserve quality and consistency in the code, all of Jack's contributions to make this work and go through the PRs, and Darion's work on this and patience in seeing things through. |
processObliv.ml had many cases that would never have executed, specially regarding mixing float and ints in binary operator expressions. See the attached bug for details, but the summary is that many of these cases are taken care of by earlier stages in CIL. Details in comment: samee#30 (comment)
Purpose
Floating point support has been added to Obliv-C as an "obliv float".
Changes Made
Nearly every file related to the Obliv-C CIL extension has been changed. The most important changes were to:
- src/ext/processObliv/processObliv.ml
- src/ext/processObliv/oblivUtils.ml
- src/cil.ml
- src/ext/oblivc/obliv_bits.c
- src/ext/oblivc/obliv_bits.h
- src/ext/oblivc/obliv_common.h
- src/ext/oblivc/obliv_bits.c
- src/ext/oblivc/obliv_types_internal.h
- src/ext/oblivc/obliv_types.h
- src/ext/oblivc/obliv.h
Documentation
Comments have been added throughout the additions where appropriate to explain the changes. A guide to extending the language has been added to the README.
Testing
The tests/testFloat folder contains tests for each standard function used with obliv floats (plus, minus, multiplication, etc). The tests/linreg folder contains an implementation of linear regression performed with the obliv float data type.