implementation restriction: pre- and postconditions for fields are ignored (interpreter) or cause broken code (JVM/C backend)

[fridis]

This example uses an effect to selectively cause a precondition or postcondition failure:

test_field_post =>

  x(pre_ok, post_ok bool) : simple_effect is

  f i32
    pre
      x.env.pre_ok
    post
      x.env.post_ok
   := 42

  (x true true).go ()->
    say f

  failPre := envir.args.count > 1
  failPost := envir.args.count <= 1
  if failPre
    say "should fail on postcondition"
  if failPost
    say "should fail on precondition"

  (x failPre failPost).go ()->
    say f

but it does not fail as expected when using the interpreter

 > ./build/bin/fz -interpreter test_field_post.fz  
42
should fail on precondition
42
 > ./build/bin/fz -interpreter test_field_post.fz  a
42
should fail on postcondition
42

Using the JVM backend, this results in a NoClassDefFoundError

 > ./build/bin/fz test_field_post.fz  

error 1: java.lang.NoClassDefFoundError: fzC_test_field_post__f
	at fzC_test_field_post__INTERN_fun0__call.fzRoutine(/home/fridi/fuzion/clean/fuzion.1/test_field_post.fz:13)
	at fzC_test_field_post__INTERN_fun0.fzD_1921_call(/home/fridi/fuzion/clean/fuzion.1/test_field_post.fz:207)
	at fzC_test_field_post__2x__1go_unit__INTERN_fun3__call.fzRoutine($MODULE/effect.fz:207)
	at fzC_test_field_post__2x__1Effect_Call_unit__call.fzRoutine($MODULE/effect.fz:153)
	at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
	at java.base/java.lang.reflect.Method.invoke(Method.java:580)
	at dev.flang.be.jvm.runtime.Runtime.effect_abortable(Runtime.java:612)
	at fzC_test_field_post__2x__1go_unit.fzRoutine($MODULE/effect.fz:207)
	at fzC_test_field_post.fzRoutine(/home/fridi/fuzion/clean/fuzion.1/test_field_post.fz:12)
	at fzC_universe.fzRoutine(--builtin--:25)
	at fzC_universe.fz_run(--builtin--)
	at dev.flang.be.jvm.runtime.FuzionThread.lambda$new$1(FuzionThread.java:97)
	at dev.flang.util.Errors.runAndExit(Errors.java:935)
	at dev.flang.be.jvm.runtime.FuzionThread.lambda$new$2(FuzionThread.java:106)
	at java.base/java.lang.Thread.run(Thread.java:1583)


*** fatal errors encountered, stopping.

while the C backend generates C compilation errors:

 > ./build/bin/fz -c test_field_post.fz  
/tmp/fuzion_universe_12248286956057100336.c:43137:3: error: use of undeclared identifier 'fzT_test_u_field_u_post__f'; did you mean 'fzP_test_u_field_u_post__f'?
  fzT_test_u_field_u_post__f* fzCur;
  ^~~~~~~~~~~~~~~~~~~~~~~~~~
  fzP_test_u_field_u_post__f
/tmp/fuzion_universe_12248286956057100336.c:43134:6: note: 'fzP_test_u_field_u_post__f' declared here
void fzP_test_u_field_u_post__f()
     ^
/tmp/fuzion_universe_12248286956057100336.c:43137:31: error: use of undeclared identifier 'fzCur'
  fzT_test_u_field_u_post__f* fzCur;
                              ^
/tmp/fuzion_universe_12248286956057100336.c:43138:3: error: use of undeclared identifier 'fzCur'
  fzCur = fzE_malloc_safe(sizeof(fzT_test_u_field_u_post__f));
  ^
/tmp/fuzion_universe_12248286956057100336.c:43138:34: error: use of undeclared identifier 'fzT_test_u_field_u_post__f'; did you mean 'fzP_test_u_field_u_post__f'?
  fzCur = fzE_malloc_safe(sizeof(fzT_test_u_field_u_post__f));
                                 ^~~~~~~~~~~~~~~~~~~~~~~~~~
                                 fzP_test_u_field_u_post__f
/tmp/fuzion_universe_12248286956057100336.c:43134:6: note: 'fzP_test_u_field_u_post__f' declared here
void fzP_test_u_field_u_post__f()
     ^
4 errors generated.

error 1: C backend: C compiler failed
C compiler call 'clang --target=x86_64-pc-linux-gnu -Wall -Werror -Wno-trigraphs -Wno-gnu-empty-struct -Wno-unused-variable -Wno-unused-label -Wno-unused-function -Wno-pointer-to-int-cast -Wno-infinite-recursion -Wno-unused-but-set-variable -O3 -lgc -DGC_THREADS -DGC_PTHREADS -DPTW32_STATIC_LIB -DGC_WIN32_PTHREADS -fno-trigraphs -fno-omit-frame-pointer -mno-omit-leaf-frame-pointer -std=c11 -o universe /home/fridi/fuzion/clean/fuzion.1/build/include/shared.c /home/fridi/fuzion/clean/fuzion.1/build/include/posix.c /tmp/fuzion_universe_12248286956057100336.c' failed with exit code '1'

one error.

Change the field to a routine

test_routine_post =>

  x(pre_ok, post_ok bool) : simple_effect is

  f i32
    pre
      x.env.pre_ok
    post
      x.env.post_ok
  => 42

  (x true true).go ()->
    say f

  failPre := envir.args.count > 1
  failPost := envir.args.count <= 1
  if failPre
    say "should fail on postcondition"
  if failPost
    say "should fail on precondition"

  (x failPre failPost).go ()->
    say f

fixes this all:

 > ./build/bin/fz test_routine_post.fz
42
should fail on precondition

error 1: CONTRACT FAILED: pre-condition on call to 'test_routine_post.f'
Call stack:
precondition of test_routine_post__f
test_routine_post__INTERN_fun1__call
test_routine_post__2x__1go_unit__INTERN_fun3__call
test_routine_post__2x__1Effect_Call_unit__call
test_routine_post__2x__1go_unit
test_routine_post
universe

*** fatal errors encountered, stopping.

and

 > ./build/bin/fz test_routine_post.fz a
42
should fail on postcondition

error 1: CONTRACT FAILED: post-condition on call to 'test_routine_post.f'
Call stack:
test_routine_post__f
test_routine_post__INTERN_fun1__call
test_routine_post__2x__1go_unit__INTERN_fun3__call
test_routine_post__2x__1Effect_Call_unit__call
test_routine_post__2x__1go_unit
test_routine_post
universe

*** fatal errors encountered, stopping.

[michaellilltokiwa]

currently:

/home/not_synced/fuzion (skip_native_value)1$ cat ~/playground/test.fz
ex is

  a i32
  pre true
  post true
  := 2

/home/not_synced/fuzion (skip_native_value)$ make no-java && fz ~/playground/test.fz

/home/sam/playground/test.fz:4:3: error 1: Implementation restriction: pre-condition for Field not supported yet.
  pre true



/home/sam/playground/test.fz:5:3: error 2: Implementation restriction: post-condition for Field not supported yet.
  post true


2 errors.
/home/not_synced/fuzion (skip_native_value)1$